University of Birmingham > Talks@bham > Lab Lunch > GADTs and the Girard/Schroeder-Heister Equality

GADTs and the Girard/Schroeder-Heister Equality

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Neel Krishnaswami.

GAD Ts, or “generalized algebraic data types”, are a feature found in functional languages like Ocaml and Haskell. Essentially, they permit indexing data types with additional information, so that (for instance) lists may be indexed with their length, or term syntaxes with the type they will evaluate to.

In this talk, I’ll show how these types have a logical interpretation, in terms of a type-theoretic equality type originally introduced by Jean-Yves Girard and Peter Schroeder-Heister to model equality in first-order logic. This equality has a different (and stronger) elimination form than the equality type of Martin-Loef type theory, and leads to a different proof theory.

Time permitting, I’ll also sketch how this view leads to some new type inference algorithms for GAD Ts.

This talk is part of the Lab Lunch series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.