## 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:Note that ex-directory lists are not shown. |
## Other listsPostgraduate Algebra Seminar Featured lists Computer Security Seminars## Other talksGeometry of alternating projections in metric spaces with bounded curvature TBC Modelling uncertainty in image analysis. When less is more - reduced physics simulations of the solar wind Hodge Theory: Connecting Algebra and Analysis The development of an optically pumped magnetometer based MEG system |