Subtyping with singleton types

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

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.
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
Pages1-15
Number of pages15
Volume933
ISBN (Electronic)978-3-540-49404-1
ISBN (Print)978-3-540-60017-6
DOIs
Publication statusPublished - 1995

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume933

Fingerprint

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

Cite this