Ctrl K

agda-core

Code underlying the publication: Building a Correct-By-Construction Type Checker for a Dependently Typed Core Language

1
mention
2
contributors

Description

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.

Logo of agda-core
Keywords
core language
Dependent Types
type-checking
typechecking
Type Theory
Programming languages
License
  • CC0-1.0
</>Source code
Packages

Reference papers

Mentions

Contributors

BL
JC
Jesper Cockx

Member of community

4TU