APAL
2005
13 years 11 months ago
2005
Systems of explicit mathematics provide an axiomatic framework to represent programs and to prove properties of them. We introduce such a system with a new form of power types usi...
CSL
2000
Springer
14 years 3 months ago
2000
Springer
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...