TY - DATA
T1 - Code underlying the publication: Building a Correct-By-Construction Type Checker for a Dependently Typed Core Language
PY - 2024/10/31
AU - Bohdan Liesnikov
AU - Jesper Cockx
UR - 
DO - 10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f.v2
KW - dependent types
KW - core language
KW - type theory
KW - typechecking
KW - type-checking
N2 - <p>This repository contains source code for the paper. We develop a correct-by-construction typechecker for a subset of Agda's internal language. This code assumes that the input has already been scope-checked and is presented to the core in a well-scoped form. The typechecker uses erasure extensively and doesn't develop any meta-theory, relying on the typing rules as the source of truth. The implementation was developed by the authors of the paper through 2023 and 2024.</p>
ER -