Subtyping with singleton types

We give syntax and a PER-model semantics for a typed λ-calculus with subtypes and singleton types. The calculus may be seen as a minimal calculus of subtyping with a simple form of dependent types. The aim is to study singleton types and to take a canny step towards more complex dependent subtyping systems. Singleton types have applications in the use of type systems for specification and program extraction: given a program P we can form the very tight specification {P} which is met uniquely by P. Singletons integrate abbreviational definitions into a type system: the hypothesis x: {M} asserts x=M. The addition of singleton types is a non-conservative extension of familiar subtyping theories. In our system, more terms are typable and previously typable terms have more (non-dependent) types.