- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- ANF preserves dependent types up to extensional equality
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
ANF preserves dependent types up to extensional equality Koronkevich, Paulette
Abstract
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 no guarantees after compiling, nor when linking after compilation. Type-preserving compilers preserve guarantees encoded in types, then use type checking to verify compiled code and ensure safe linking with external code. Unfortunately, standard compiler passes do not preserve the dependent typing of commonly used (intensional) type theories. This is because assumptions valid in simpler type systems no longer hold, and intensional dependent type systems are highly sensitive to syntactic changes, including compilation. We develop an A-normal form (ANF) translation with join-point optimization, a standard translation for making control flow explicit in functional languages, from the Extended Calculus of Constructions (ECC) with dependent elimination of booleans and natural numbers (a representative subset of Coq). Our dependently typed target language has equality reflection, allowing the type system to encode semantic equality of terms. This is key to proving type preservation and correctness of separate compilation for this translation. This is the first ANF translation for dependent types. Unlike related translations, it supports the universe hierarchy, and does not rely on parametricity or impredicativity.
Item Metadata
Title |
ANF preserves dependent types up to extensional equality
|
Creator | |
Supervisor | |
Publisher |
University of British Columbia
|
Date Issued |
2021
|
Description |
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 no
guarantees after compiling, nor when linking after compilation.
Type-preserving compilers preserve guarantees encoded
in types, then use type checking to verify compiled code and ensure
safe linking with external code.
Unfortunately, standard compiler passes do not preserve the
dependent typing of commonly used (intensional) type theories.
This is because assumptions valid in simpler type systems no longer hold,
and intensional dependent type systems are highly sensitive to
syntactic changes, including compilation.
We develop an A-normal form (ANF) translation with
join-point optimization, a standard translation for making control flow explicit
in functional languages, from the Extended Calculus of Constructions (ECC)
with dependent elimination of booleans and natural numbers
(a representative subset of Coq).
Our dependently typed target language has equality reflection,
allowing the type system to encode semantic equality of terms.
This is key to proving type preservation and correctness of separate compilation
for this translation.
This is the first ANF translation for dependent types.
Unlike related translations, it supports the universe hierarchy,
and does not rely on parametricity or impredicativity.
|
Genre | |
Type | |
Language |
eng
|
Date Available |
2021-08-17
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
Attribution-NonCommercial-NoDerivatives 4.0 International
|
DOI |
10.14288/1.0401431
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
2021-11
|
Campus | |
Scholarly Level |
Graduate
|
Rights URI | |
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivatives 4.0 International