cff-version: 1.2.0
abstract: "<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>"
authors:
  - family-names: Liesnikov
    given-names: Bohdan
    orcid: "https://orcid.org/0009-0000-2216-8830"
  - family-names: Cockx
    given-names: Jesper
title: "Code underlying the publication: Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language"
keywords:
version: 1
identifiers:
  - type: doi
    value: 10.4121/6f239149-2526-42a0-8d07-d0e9d6714f7f.v1
license: CC0
date-released: 2024-08-16