@inproceedings{343219691d8d4ba7a1e9ac8f7ac938f6,

title = "Subtyping with singleton types",

abstract = "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.",

author = "David Aspinall",

year = "1995",

doi = "10.1007/BFb0022243",

language = "English",

isbn = "978-3-540-60017-6",

volume = "933",

series = "Lecture Notes in Computer Science",

publisher = "Springer Berlin Heidelberg",

pages = "1--15",

editor = "Leszek Pacholski and Jerzy Tiuryn",

booktitle = "Computer Science Logic",

}