GADTs and the Girard/Schroeder-Heister Equality

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

• Neel Krishnaswami (University of Birmingham)
• Friday 07 February 2014, 13:00-14:00
• CS 245.

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.

This talk is included in these lists:

• CS 245
• Lab Lunch

Note that ex-directory lists are not shown.