Dependent Merges and First-Class Environments (Artifact)

Authors Jinhao Tan, Bruno C. d. S. Oliveira

Thumbnail PDF

Artifact Description

  • Filesize: 446 kB
  • 3 pages

Document Identifiers

Author Details

Jinhao Tan
  • The University of Hong Kong, China
Bruno C. d. S. Oliveira
  • The University of Hong Kong, China


We thank the anonymous reviewers for their helpful comments.

Cite AsGet BibTex

Jinhao Tan and Bruno C. d. S. Oliveira. Dependent Merges and First-Class Environments (Artifact). In Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023). Dagstuhl Artifacts Series (DARTS), Volume 9, Issue 2, pp. 2:1-2:3, Schloss Dagstuhl – Leibniz-Zentrum fΓΌr Informatik (2023)


Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2023 Call for Artifacts and the ACM Artifact Review and Badging Policy


This artifact contains the mechanical formalization of the calculi associated with the paper Dependent Merges and First-Class Environments. All of the metatheory has been formalized in Coq theorem prover. The paper studies a statically typed calculus, called 𝖀_i, with first-class environments. The main novelty of the 𝖀_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them.

Subject Classification

ACM Subject Classification
  • Theory of computation β†’ Type theory
  • First-class Environments
  • Disjointness
  • Intersection Types


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads