Union, intersection and dependent types in an explicitly typed lambda-calculus
DMIF, University of Udine
16/10/2020 ore 14:00
Sala Riunioni, DMIF
We introduce a lambda-calculus decorated with types, enhanced with intersection types, union types, and dependent types. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the “proofs-as-lambda-terms / formulae-as-types” Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. We then discuss the design decisions which have led us to the formulation of these calculi, and provide some examples of applications; and we finally present a software implementation of the Delta-framework, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants.