A predicative type system with power types is introduced and studied, based on a reformulated fragment of Cardelli's 1988 system. It allows better logical encodings than in LF or LF with subtyping (LambdaPsub), and can express higher-order subtyping without needing special rules for operators. A particular novelty is the auxiliary system for "rough typing", which assigns simple types to terms of the calculus. This allows a model definition to be given which uses a set-theoretic containment semantics without recourse to a universal domain.David Aspinall.
Click here to return to my papers page.