## GADTs and the Girard/Schroeder-Heister EqualityAdd 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
- Computer Science Departmental Series
- Computer Science Distinguished Seminars
- Lab Lunch
- Theoretical computer science seminar
Note that ex-directory lists are not shown. |
## Other listsTheoretical Physics Seminars Computer Science Lunch Time Talk Series Lab Lunch## Other talks |