Strong Normalization with Singleton Types

Abstract

This paper presents a new lambda-calculus with singleton types, called λ≤{}βδ. The main novelty of λ≤{}βδ is the introduction of a new reduction, the δ-reduction, replacing any variable declared of singleton type by its value, and the definition of equality as the syntactic equality of βδ-normal forms. The δ-reduction has a very odd behavior on untyped terms, which renders its metatheoretical study difficult since the usual proof method for subject-reduction and Church-Rosser property are inapplicable. Nevertheless, these properties can be proved simultaneously with strong normalization on typed terms using a proof method à la Coquand-Gallier, borrowing ideas to Goguen. In spite of its complex metatheory, our calculus enjoys a simple, sound and complete type-inference algorithm.