The doi above is for this specific version of this dataset, which is currently the latest. Newer versions may be published in the future. For a link that will always point to the latest version, please use
doi: 10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f

Liesnikov, Bohdan; Cockx, Jesper (2024): Code underlying the publication: Building a Correct-By-Construction Type Checker for a Dependently Typed Core Language. Version 2. 4TU.ResearchData. software. https://doi.org/10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f.v2

Software

x choose version: version 1 - 2024-08-16

• Computer Software
• Information and Computing Sciences

core language, dependent types, type theory, type-checking, typechecking

CC0

RefWorks, BibTeX, Reference Manager, Endnote, DataCite, NLM, DC, CFF

by Bohdan Liesnikov , Jesper Cockx

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.

• 2024-08-16 first online

• 2024-10-31 published, posted

4TU.ResearchData

git repository cotaining an Agda project, built using nix

Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language

• https://conf.researchr.org/details/aplas-2024/aplas-2024-research-papers/13/Building-A-Correct-By-Construction-Type-Checker-for-a-Dependently-Typed-Core-Language

https://github.com/jespercockx/agda-core/

https://github.com/jespercockx/agda-core/tree/aplas-2024

• A trustworthy and extensible core language for Agda (grant code VI.Veni.202.216 ) [more info...] NWO

TU Delft, Faculty of Electrical Engineering, Mathematics and Computer Science, Department of Software Technology