Building a Correct-by-Construction Type Checker for a Dependently Typed Core Language
Abstract elided by the publisher.
Related papers
- Typing Algorithm in Type Theory with Inheritance POPL 1997
- Self-certification: bootstrapping certified typecheckers in F* with Coq POPL 2012
- Algebra of programming in Agda: Dependent types for relational program derivation JFP 2009
- SteelCore: an extensible concurrent separation logic for effectful dependently typed programs ICFP 2020
- Scope States: Guarding Safety of Name Resolution in Parallel Type Checkers ECOOP 2021
- Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications OOPSLA 2020
- Localizing Type Errors for Syntactic Sugar by Lifting OOPSLA 2026
- A Typing Discipline for Hardware Interfaces ECOOP 2019