Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compilation Semantics for a Programming Language with Versions

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

TL;DR

This work addresses the rigidity of single-version dependencies by introducing VL, a surface language for λ_VL that enables simultaneous use of multiple module versions. The VL compiler translates programs to a version-label-free core, VLMini, via Girard's translation, and then applies algorithmic type and version inference to assign consistent versions and generate a multi-version interface through bundling. The approach delivers a formal pathway from surface language to core semantics, with proofs of inference soundness, and demonstrates practicality through implementation and a case study on authentic software evolution scenarios. The resulting framework supports scalable handling of evolving libraries, enabling robust software maintenance in multi-version ecosystems.

Abstract

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 $λ_{\mathrm{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 $λ_{\mathrm{VL}}$ along 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.

Compilation Semantics for a Programming Language with Versions

TL;DR

This work addresses the rigidity of single-version dependencies by introducing VL, a surface language for λ_VL that enables simultaneous use of multiple module versions. The VL compiler translates programs to a version-label-free core, VLMini, via Girard's translation, and then applies algorithmic type and version inference to assign consistent versions and generate a multi-version interface through bundling. The approach delivers a formal pathway from surface language to core semantics, with proofs of inference soundness, and demonstrates practicality through implementation and a case study on authentic software evolution scenarios. The resulting framework supports scalable handling of evolving libraries, enabling robust software maintenance in multi-version ecosystems.

Abstract

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 , 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 along 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.
Paper Structure (16 sections, 18 equations, 5 figures)

This paper contains 16 sections, 18 equations, 5 figures.

Table of Contents

  1. Introduction
  2. Paper Organization.
  3. Overview
  4. Motivating Example
  5. $\lambda_{\mathrm{VL}}$
  6. Version Labels
  7. Syntax of $\lambda_{\mathrm{VL}}$
  8. Type of Versioned Values
  9. Programming with Versions in VL
  10. Compilation
  11. An Intermediate Language, VLMini
  12. Syntax of VLMini
  13. Constraints
  14. Girard's Translation for VLMini
  15. Bundling
  16. ...and 1 more sections

Figures (5)

  • Figure 1: Minimal module configuration before and after the dependency update causing an error due to inconsistency expected to the dependent package.
  • Figure 2: The syntax of $\lambda_{\mathrm{VL}}$.
  • Figure 3: The programs in Figure \ref{['fig2-1']} in VL.
  • Figure 4: The translation phases for a single module with multiple versions.
  • Figure 5: The syntax of VLMini.