# Typed closure conversion for the calculus of constructions

@article{Bowman2018TypedCC, title={Typed closure conversion for the calculus of constructions}, author={William J. Bowman and Amal Ahmed}, journal={Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation}, year={2018} }

Dependently typed languages such as Coq are used to specify and verify the full functional correctness of source programs. Type-preserving compilation can be used to preserve these specifications and proofs of correctness through compilation into the generated target-language programs. Unfortunately, type-preserving compilation of dependent types is hard. In essence, the problem is that dependent type systems are designed around high-level compositional abstractions to decide type checking, but… Expand

#### 7 Citations

Compiling Dependent Types Without Continuations

- 2019

Programmers rely on dependently typed languages, such as Coq, to machine-verify high-assurance software, but get no guarantees after compiling or when linking after compilation. We could provide… Expand

TWAM: A Certifying Abstract Machine for Logic Programs

- Computer Science
- VSTTE
- 2018

A soundness metatheorem is presented which constitutes a partial correctness guarantee: well-typed programs implement the logic program specified by their type, which justifies the design and implementation of a certifying compiler from T-Prolog to TWAM. Expand

Strictly capturing non-strict closures

- Computer Science
- PEPM@POPL
- 2021

The logical relation techniques used to prove compiler correctness for call-by-value languages, to apply to non-strict languages too, are extended and some important properties for reasoning about memoization with a heap are identified. Expand

The Dynamic Practice and Static Theory of Gradual Typing

- Computer Science
- SNAPL
- 2019

We can tease apart the research on gradual types into two `lineages': a pragmatic, implementation-oriented dynamic-first lineage and a formal, type-theoretic, static-first lineage. The dynamic-first… Expand

3rd Summit on Advances in Programming Languages, SNAPL 2019, May 16-17, 2019, Providence, RI, USA

- Computer Science
- SNAPL
- 2019

It is argued that the gap between available precision and that that is required for either Software 1.0 or Software 2.0 is a fundamental aspect of software design that illustrates the balance between software designed for general-purposes and domain-adapted solutions. Expand

ANF preserves dependent types up to extensional equality

- Mathematics
- 2021

A growing number of programmers use dependently typed languages such as Coq to machine-verify important properties of high-assurance software. However, existing compilers for these languages provide… Expand

Solving the Funarg Problem with Static Types

- Computer Science
- ArXiv
- 2021

This work presents a simple extension to the prenex fragment of System F that allows closures to be stack-allocated and demonstrates a concrete implementation of this system in the Juniper functional reactive programming language, which is designed to run on extremely resource limited Arduino devices. Expand

#### References

SHOWING 1-10 OF 47 REFERENCES

Typed closure conversion

- Computer Science
- POPL '96
- 1996

This work presents closure conversion as a type-directed, and type-preserving translation for both the simply-typed and the polymorphic ¿-calculus, and exploits a variant of the Harper-Lillibridge "translucent type" formalism to characterize the types of polymorphic closures. Expand

Typed Closure Conversion for Recursively-Defined Functions

- Computer Science
- Electron. Notes Theor. Comput. Sci.
- 1997

Three main approaches are considered in the treatment of simply-typed closure conversion for compiler transformation to account for recursively-defined functions such as are found in ML, one based on a recursive code construct, oneBased on a self-referential data structure, and onebased on recursive types. Expand

Type-preserving CPS translation of Σ and Π types is not not possible

- Computer Science, Mathematics
- Proc. ACM Program. Lang.
- 2018

This paper develops both call-by-name and call- by-value CPS translations from the Calculus of Constructions with both Π and Σ types to a dependently typed target language, and proves type preservation and compiler correctness of each translation. Expand

A type-preserving compiler from system f to typed assembly language

- Computer Science
- 2009

This thesis presents a compiler from a polymorphic higher-order functional language to typed assembly language, whose main property is that type preservation is verified statically, through type annotations on the compiler’s code. Expand

The Implicit Calculus of Constructions as a Programming Language with Dependent Types

- Computer Science
- FoSSaCS
- 2008

This paper shows how Miquel's Implicit Calculus of Constructions can be used as a programming language featuring dependent types and introduces a more verbose variant, called ICC* which fixes the issue of an undecidable type-checking. Expand

Typed closure conversion preserves observational equivalence

- Computer Science
- ICFP
- 2008

It is proved that typed closure conversion for the polymorphic »-calculus with existential and recursive types is fully abstract, i.e., compilation that both preserves and reflects observational equivalence. Expand

Type-preserving compilation of end-to-end verification of security enforcement

- Computer Science
- PLDI '10
- 2010

A type-preserving compiler that translates programs written in FINE, a source-level functional language with dependent refinements and affine types, to DCIL, a new extension of the .NET Common Intermediate Language, to reduce the proof burden on source programmers. Expand

Verifying an Open Compiler Using Multi-language Semantics

- Computer Science
- ESOP
- 2014

A new methodology for verifying correct compilation of program components, while formally allowing linking with target code of arbitrary provenance is presented, and a two-pass type-preserving open compiler is presented and it is proved that compilation preserves semantics. Expand

On Strong Normalization of the Calculus of Constructions with Type-Based Termination

- 2018

Termination of recursive functions is an important property in proof assistants based on dependent type theories; it implies consistency and decidability of type checking. Type-based termination is a… Expand