Programming up to Congruence

8 years 4 days ago
Programming up to Congruence
This paper presents the design of ZOMBIE, a dependently-typed programming language that uses an adaptation of a congruence closure algorithm for proof and type inference. This algorithm allows the type checker to automatically use equality assumptions from the context when reasoning about equality. Most dependentlytyped languages automatically use equalities that follow from βreduction during type checking; however, such reasoning is incompatible with congruence closure. In contrast, ZOMBIE does not use automatic β-reduction because types may contain potentially diverging terms. Therefore ZOMBIE provides a unique opportunity to explore an alternative definition of equivalence in dependentlytyped language design. Our work includes the specification of the language via a bidirectional type system, which works “up-to-congruence,” and an algorithm for elaborating expressions in this language to an explicitly typed core language. We prove that our elaboration algorithm is complete ...
Vilhelm Sjöberg, Stephanie Weirich
Added 16 Apr 2016
Updated 16 Apr 2016
Type Journal
Year 2015
Where POPL
Authors Vilhelm Sjöberg, Stephanie Weirich
Comments (0)