Code underlying the publication: Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language
Datacite citation style:
Liesnikov, Bohdan; Cockx, Jesper (2024): Code underlying the publication: Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language. Version 1. 4TU.ResearchData. software. https://doi.org/10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f.v1
Other citation styles (APA, Harvard, MLA, Vancouver, Chicago, IEEE) available at Datacite
Software
choose version:
version 2 - 2024-10-31 (latest)
version 1 - 2024-08-16
licence
CC0
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.
history
- 2024-08-16 first online, published, posted
publisher
4TU.ResearchData
format
Agda project, built using nix
funding
- A trustworthy and extensible core language for Agda (grant code VI.Veni.202.216 ) [more info...] NWO
organizations
TU Delft, Faculty of Electrical Engineering, Mathematics and Computer Science, Department of Software Technology
DATA
To access the source code, use the following command:
git clone https://data.4tu.nl/v3/datasets/0ae22b64-3ab6-466d-a419-66e12c866a6e.git "agda-core"
