## 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 listsSeminars on Advanced Materials Mathematics Colloquium Type the title of a new list here## Other talksLarge Cantor sets as non-Lebesgue sets of Fourier transforms Hydrodynamics and Chaos in Quantum Matter Physics at van der Waals interfaces: Twists, incommensurability and emergent phenomena An attack on ECDSA using lattice techniques The Small Mathieu Groups Rage against the dying of the light: Type Ia supernovae at 1000 days and beyond |