Subtyping with Power Types

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 t, 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. 1 Introducing Power Types Power types were introduced in a seminal paper by Cardelli [9]. The notion is that Power(A) is a type “whose elements a...

• Type: Conference
• Year: 2000
• Where: CSL
• Authors: David Aspinall
• Keywords: Automated Reasoning, Cardelli’s Power Type, CSL 2000, Dependent Types, Power Types