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

Bohdan Liesnikov; Jesper Cockx

doi:10.1007/978-981-97-8943-6_4

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

^*Corresponding author for this work

Programming Languages

Research output: Chapter in Book/Conference proceedings/Edited volume › Conference contribution › Scientific › peer-review

Abstract

Dependently typed languages allow us to state a program’s expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? The goal of this paper is to develop a lightweight technique to improve their trustworthiness by giving a formal specification of the typing rules and intrinsically verifying the type checker with respect to these rules. Concretely, we apply this technique to a subset of Agda’s internal language, implemented in Agda. Our development relies on erasure annotations to separate the specification from the runtime of the type checker. We provide guidelines for making design decisions for certified core type checkers and evaluate trade-offs.

Original language	English
Title of host publication	Programming Languages and Systems
Subtitle of host publication	22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings
Editors	Oleg Kiselyov
Place of Publication	Singapore
Publisher	Springer
Pages	63-83
Number of pages	21
ISBN (Electronic)	978-981-97-8943-6
ISBN (Print)	978-981-97-8942-9
DOIs	https://doi.org/10.1007/978-981-97-8943-6_4
Publication status	Published - 2025
Event	22nd Asian Symposium on Programming Languages and Systems - Kyoto, Japan Duration: 22 Oct 2024 → 24 Oct 2024 Conference number: 22

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer
Volume	15194 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	22nd Asian Symposium on Programming Languages and Systems
Abbreviated title	APLAS 2024
Country/Territory	Japan
City	Kyoto
Period	22/10/24 → 24/10/24

Bibliographical note

Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care
Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.

Keywords

Agda
Correct-by-Construction Programming
Dependent types

Access to Document

10.1007/978-981-97-8943-6_4

Cite this

Liesnikov, B., & Cockx, J. (2025). Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. In O. Kiselyov (Ed.), Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings (pp. 63-83). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15194 LNCS). Springer. https://doi.org/10.1007/978-981-97-8943-6_4

Liesnikov, Bohdan ; Cockx, Jesper. / Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. editor / Oleg Kiselyov. Singapore : Springer, 2025. pp. 63-83 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{e194d108d23247ce8904232061af3f7f,

title = "Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language",

abstract = "Dependently typed languages allow us to state a program{\textquoteright}s expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? The goal of this paper is to develop a lightweight technique to improve their trustworthiness by giving a formal specification of the typing rules and intrinsically verifying the type checker with respect to these rules. Concretely, we apply this technique to a subset of Agda{\textquoteright}s internal language, implemented in Agda. Our development relies on erasure annotations to separate the specification from the runtime of the type checker. We provide guidelines for making design decisions for certified core type checkers and evaluate trade-offs.",

keywords = "Agda, Correct-by-Construction Programming, Dependent types",

author = "Bohdan Liesnikov and Jesper Cockx",

note = "Green Open Access added to TU Delft Institutional Repository 'You share, we take care!' - Taverne project https://www.openaccess.nl/en/you-share-we-take-care Otherwise as indicated in the copyright section: the publisher is the copyright holder of this work and the author uses the Dutch legislation to make this work public.; 22nd Asian Symposium on Programming Languages and Systems, APLAS 2024 ; Conference date: 22-10-2024 Through 24-10-2024",

year = "2025",

doi = "10.1007/978-981-97-8943-6_4",

language = "English",

isbn = "978-981-97-8942-9",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "63--83",

editor = "Oleg Kiselyov",

booktitle = "Programming Languages and Systems",

}

Liesnikov, B & Cockx, J 2025, Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. in O Kiselyov (ed.), Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 15194 LNCS, Springer, Singapore, pp. 63-83, 22nd Asian Symposium on Programming Languages and Systems, Kyoto, Japan, 22/10/24. https://doi.org/10.1007/978-981-97-8943-6_4

Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. / Liesnikov, Bohdan ; Cockx, Jesper.
Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. ed. / Oleg Kiselyov. Singapore: Springer, 2025. p. 63-83 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 15194 LNCS).

Research output: Chapter in Book/Conference proceedings/Edited volume › Conference contribution › Scientific › peer-review

TY - GEN

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

AU - Liesnikov, Bohdan

AU - Cockx, Jesper

N1 - Conference code: 22

PY - 2025

Y1 - 2025

N2 - Dependently typed languages allow us to state a program’s expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? The goal of this paper is to develop a lightweight technique to improve their trustworthiness by giving a formal specification of the typing rules and intrinsically verifying the type checker with respect to these rules. Concretely, we apply this technique to a subset of Agda’s internal language, implemented in Agda. Our development relies on erasure annotations to separate the specification from the runtime of the type checker. We provide guidelines for making design decisions for certified core type checkers and evaluate trade-offs.

AB - Dependently typed languages allow us to state a program’s expected properties and automatically check that they are satisfied at compile time. Yet the implementations of these languages are themselves just software, so can we really trust them? The goal of this paper is to develop a lightweight technique to improve their trustworthiness by giving a formal specification of the typing rules and intrinsically verifying the type checker with respect to these rules. Concretely, we apply this technique to a subset of Agda’s internal language, implemented in Agda. Our development relies on erasure annotations to separate the specification from the runtime of the type checker. We provide guidelines for making design decisions for certified core type checkers and evaluate trade-offs.

KW - Agda

KW - Correct-by-Construction Programming

KW - Dependent types

UR - http://www.scopus.com/inward/record.url?scp=85209802908&partnerID=8YFLogxK

U2 - 10.1007/978-981-97-8943-6_4

DO - 10.1007/978-981-97-8943-6_4

M3 - Conference contribution

AN - SCOPUS:85209802908

SN - 978-981-97-8942-9

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 63

EP - 83

BT - Programming Languages and Systems

A2 - Kiselyov, Oleg

PB - Springer

CY - Singapore

T2 - 22nd Asian Symposium on Programming Languages and Systems

Y2 - 22 October 2024 through 24 October 2024

ER -

Liesnikov B , Cockx J. Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language. In Kiselyov O, editor, Programming Languages and Systems: 22nd Asian Symposium, APLAS 2024, Kyoto, Japan, October 22-24, 2024, Proceedings. Singapore: Springer. 2025. p. 63-83. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-981-97-8943-6_4

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

Abstract

Publication series

Conference

Bibliographical note

Keywords

Access to Document

Other files and links

Embargoed Document

Fingerprint

Cite this