publications

2024

1. PLDI

   Space-Efficient Polymorphic Gradual Typing, Mostly Parametric

   Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, and Yudai Tanabe

   Proceedings of the ACM on Programming Languages (PACMPL), 2024

   PACMPL Abs

   Since the arrival of gradual typing, which allows partially typed code in a single program, efficient implementations of gradual typing have been an active research topic. In this paper, we study the space-efficiency problem of gradual typing in the presence of parametric polymorphism. Based on the existing work that showed the impossibility of a space-efficient implementation that supports fully parametric polymorphism, this paper will show that a space-efficient implementation is, in principle, possible by slightly relaxing parametricity. We first develop \lambdaC^\F_mp, which is a coercion calculus with mostly parametric polymorphism, and show its relaxed parametricity. Then, we present \lambdaS^\F_mp, a space-efficient version of \lambdaC^\F_mp, and prove that \lambdaS^\F_mp programs can be executed in a space-efficient manner and that translation from \lambdaC^\F_mp to \lambdaS^\F_mp is type- and semantics-preserving.

2023

1. 

   COP 2023: Proceedings of the 15th ACM International Workshop on Context-Oriented Programming and Advanced Modularity

   Edited by Yudai Tanabe, Lars Schütze, Robert Hirschfeld, Atsushi Igarashi, and Hidehiko Masuhara

   2023

   ACM DL Abs

   Contextual information plays an ever-increasing role in our information-centric world. Current-day software systems adapt continuously to changing execution and usage contexts, even while running. Unfortunately, mainstream programming languages and development environments still do not support this kind of dynamicity very well, leading developers to implement complex designs to anticipate various dimensions of variability.

2. APLAS

   Compilation Semantics for a Programming Language with Versions

   Yudai Tanabe, Luthfan Anshar Lubis, Tomoyuki Aotani, and Hidehiko Masuhara

   In Programming Languages and Systems, 2023

   Springer arXiv Abs

   Programming with versions is a paradigm that allows a program to use multiple versions of a module so that the programmer can selectively use functions from both older and newer versions of a single module. Previous work formalized \{}lambda _{}textrm{VL}}\\λVL, a core calculus for programming with versions, but it has not been integrated into practical programming languages. In this paper, we propose VL, a Haskell-subset surface language for \{}lambda _{}textrm{VL}}\\λVLalong with its compilation method. We formally describe the core part of the VL compiler, which translates from the surface language to the core language by leveraging Girard’s translation, soundly infers the consistent version of expressions along with their types, and generates a multi-version interface by bundling specific-version interfaces. We conduct a case study to show how VL supports practical software evolution scenarios and discuss the method’s scalability.

2022

1. 

   COP ’22: Proceedings of the 14th ACM International Workshop on Context-Oriented Programming and Advanced Modularity

   Edited by Yudai Tanabe, Jens Lincke, Robert Hirschfeld, Atsushi Igarashi, and Hidehiko Masuhara

   2022

   ACM DL
2. SLE

   BatakJava: An Object-Oriented Programming Language with Versions

   Luthfan Anshar Lubis, Yudai Tanabe, Tomoyuki Aotani, and Hidehiko Masuhara

   In Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, Dec 2022

   ACM DL Abs

   Programming with versions is a recent proposal that supports multiple versions of software components in a program. Though it would provide greater freedom for the programmer, the concept is only realized as a simple core calculus, called λVL, where a value consists of λ-terms with multiple versions. We explore a design space of programming with versions in the presence of data structures and module systems, and propose BatakJava, an object-oriented programming language in which multiple versions of a class can be used in a program. This paper presents BatakJava’s language design, its core semantics with subject reduction, an implementation as a source-to-Java translator, and a case study to understand how we can exploit multiple versions in BatakJava for developing an application program with an evolving library.

3. COP

   A Step toward Programming with Versions in Real-World Functional Languages

   Yudai Tanabe, Luthfan Anshar Lubis, Tomoyuki Aotani, and Hidehiko Masuhara

   In Proceedings of the 14th ACM International Workshop on Context-Oriented Programming and Advanced Modularity, Dec 2022

   ACM DL Abs

   λVL is a core calculus based on the concept of programming with versions that supports multiple versions of program definitions and values inherently in the semantics of a language. However, since λVL was not designed as a surface language, its complex syntax and semantics only provide primitive constructs to manipulate versioned values. In order to realize the programming with versions concept in a real-world language, we propose a compilation method for functional languages through λVL and discuss how real-world programs can be written in a Haskell-like functional language with versions.

2021

1. ‹Programming›

   A Functional Programming Language with Versions

   Yudai Tanabe, Luthfan Anshar Lubis, Tomoyuki Aotani, and Hidehiko Masuhara

   The Art, Science, and Engineering of Programming, Jul 2021

   J. Prog. Abs

   While modern software development heavily uses versioned packages, programming languages rarely support the concept of versions in their semantics, which makes software updates more bulky and unsafe. This paper proposes a programming language that intrinsically supports versions. The main goals are to design core language features to support multiple versions in one program and establish a proper notion of type safety with those features. The proposed core calculus, called Lambda VL, has versioned values, each containing different values under different versions. We show the construction of the type system as an extension of coeffect calculus by mapping versions to computational resources. The type system guarantees the existence of a valid combination of versions for a program. The calculus enables programming languages to use multiple versions of a package within a program. It will serve as a basis for designing advanced language features like module systems and semantic versioning.

2018

1. COP

   A Context-Oriented Programming Approach to Dependency Hell

   Yudai Tanabe, Tomoyuki Aotani, and Hidehiko Masuhara

   In Proceedings of the 10th ACM International Workshop on Context-Oriented Programming: Advanced Modularity for Run-time Composition, Jul 2018

   ACM DL Abs

   Two or more incompatible versions of a library are sometimes needed in one software artifact, which is so-called dependency hell. One likely faces the problem if he or she uses two or more libraries that depend on the same library. In this paper, we propose versioned values to solve the problem. They allow us to have multiple versions of functions in a binary file. This gets rid of requiring two or more incompatible binaries. We develop a calculus λVL to discuss type safety in the case where definitions are available only in specific versions, which is a common and important nature of versioned programs.