In Programming up to Congruence, Sjöberg and Weirich handle potentially nonterminating terms by taking the somewhat radical step of designing a dependently typed language not equipped with automatic β-reduction at all, instead using casts along explicitly specified equalities. To recover the “usual” experience of dependently typed programming, the authors then describe a surface language that elaborates into the explicitly annotated core language, with appropriate equalities automatically inferred via congruence closure. In this work, we propose a generalization of this method applicable to various existing type systems: given a variant of the (dependently-typed) lambda calculus satisfying some basic properties, we may construct a modified calculus in which we compare and type-check terms within an “equivalence context” of equalities, sans any notion of automatic reduction or normalization. We then provide an algorithm that, given a term in the original calculus, produces a term in the modified calculus and a set of equality constraints that are satisfied if and only if the original term type-checks. Hence, we may implement the original calculus “under the hood” by lowering to the modified calculus, with little to no changes to the original type theory or semantics, preserving compatibility with programs in the original language. We have used this method to develop an experimental congruence-based implementation of the Calculus of Inductive Constructions written in Rust, “isotope,” which we hope to demonstrate. We believe that this method can significantly improve the speed with which sizeable proof developments can be type-checked, while at the same time having applications in the design of novel type systems to handle problems such as non-terminating (or even non-confluent) sets of rewrite rules, and semantic versioning of dependently typed programs.
PhD student at the Department of Computer Science and Technology in the University of Cambridge, supervised by Neel Krishnaswami.
Sat 22 JanDisplayed time zone: Eastern Time (US & Canada) change
15:05 - 16:20
Session 4WITS at Salon III
Chair(s): Jesper Cockx TU Delft, Richard A. Eisenberg Tweag
|mitten: A Flexible Multimodal Proof AssistantRemote|
Philipp Stassen Aarhus University, Daniel Gratzer Aarhus University, Lars Birkedal Aarhus University
|Understandable and Useful Error Messages for Liquid TypesRemote|
Alcides Fonseca LASIGE, Faculdade de Ciências da Universidade de Lisboa, Catarina Gamboa LASIGE, Faculdade de Ciências da Universidade de Lisboa, João David LASIGE, Faculdade de Ciências da Universidade de Lisboa, Guilherme Espada LASIGE, Faculdade de Ciências da Universidade de Lisboa, Paulo Canelas LASIGE, Faculdade de Ciências da Universidade de Lisboa
|Deciding type equivalence with simple grammarsIn-Person|
Bernardo Almeida LASIGE, Faculty of Sciences, University of Lisbon, Andreia Mordido Lasige / Faculty of Sciences, Universidade de Lisboa, Vasco T. Vasconcelos LASIGE, Faculty of Sciences, University of Lisbon
|Typechecking up to CongruenceIn-Person|
Jad Elkhaleq Ghalayini University of Cambridge
|À bas l’η — Coq’s troublesome η-conversionRemote|
Meven Lennon-Bertrand Inria – LS2N, Université de Nantes