Seminario: “Union, intersection and dependent types in an explicitly typed lambda-calculus”
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.
Chiudendo questo banner, scorrendo questa pagina, cliccando su un link o proseguendo la navigazione in altra maniera, acconsenti all’uso dei cookie. OK
Privacy & Cookies Policy
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.