Subtyping with Power Types

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

Abstract / Description of output

This paper introduces a typed λ-calculus called λPower, a predicative reformulation of part of Cardelli’s power type system. Power types integrate subtyping into the typing judgement, allowing bounded abstraction and bounded quantification over both types and terms. This gives a powerful and concise system of dependent types, but leads to difficulty in the meta-theory and semantics which has impeded the application of power types so far. Basic properties of λPower are proved here, and it is given a model definition using a form of applicative structures. A particular novelty is the auxiliary system for rough typing, which assigns simple types to terms in λPower. These “rough” types are used to prove strong normalization of the calculus and to structure models, allowing a novel form of containment semantics without a universal domain.
Original languageEnglish
Title of host publicationComputer Science Logic
Subtitle of host publication14th Annual Conference of the EACSL, Fischbachau, Germany, August 21-26, 2000, Proceedings
PublisherSpringer
Pages156-171
Number of pages16
ISBN (Electronic)978-3-540-44622-4
ISBN (Print)978-3-540-67895-3
DOIs
Publication statusPublished - 2000

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume1862
ISSN (Print)0302-9743

Fingerprint

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

Cite this