APLAS 2024
Tue 22 - Fri 25 October 2024 Kyoto

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 typechecker 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 typechecker. We provide guidelines for making design decisions for certified core typecheckers and evaluate trade-offs.

Wed 23 Oct

Displayed time zone: Osaka, Sapporo, Tokyo change

10:30 - 12:00
Type theory and Semantic Frameworks IIResearch Papers at Yamauchi Hall
Chair(s): Pierre-Evariste Dagand IRIF / CNRS
10:30
30m
Talk
Building A Correct-By-Construction Type Checker for a Dependently Typed Core Language
Research Papers
Bohdan Liesnikov Delft University of Technology, Jesper Cockx Delft University of Technology
11:00
30m
Talk
Extending the Quantitative Pattern-Matching Paradigm
Research Papers
Sandra Alves University of Porto, Delia Kesner Université Paris Cité - CNRS - IRIF; Institut Universitaire de France, Miguel Ramos Universidade do Porto, LIACC; Université Paris Cité, IRIF, CNRS
11:30
30m
Talk
On Computational Indistinguishability and Logical Relations
Research Papers
Ugo Dal Lago University of Bologna & INRIA Sophia Antipolis, Zeinab Galal University of Bologna, Giulia Giusti ENS Lyon
:
:
:
: