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.