Subtyping with singleton types

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

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.
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication8th Workshop, CSL '94 Kazimierz, Poland, September 25–30, 1994 Selected Papers
EditorsLeszek Pacholski, Jerzy Tiuryn
PublisherSpringer Berlin Heidelberg
Number of pages15
ISBN (Electronic)978-3-540-49404-1
ISBN (Print)978-3-540-60017-6
Publication statusPublished - 1995

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg


Dive into the research topics of 'Subtyping with singleton types'. Together they form a unique fingerprint.

Cite this