![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > FreshMLTT: Dependent Type Theory with Names and Name-Abstraction
FreshMLTT: Dependent Type Theory with Names and Name-AbstractionAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Neel Krishnaswami. The aim of this work is to develop a constructive version of nominal logic as a dependent type theory. The motivation for such an aim, from a programming point of view, is the desire to combine FreshML style meta-programming for syntax with binding operations with Agda/Coq style theorem-proving (particularly inductively defined indexed families of types and dependent pattern-matching). Achieving this aim requires a constructive treatment of the nominal sets notion of freshness. In this talk I will describe one such treatment as an extension of Martin-L\”of type theory. This is joint work with Justus Matthiesen and Jasper Derikx. This talk is part of the Theoretical computer science seminar series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsMolecular and Medical Physics Seminar Series Aerospace Seminar Series School of Metallurgy and Materials ColloquiaOther talksTBA Ultrafast Spectroscopy and Microscopy as probes of Energy Materials Quantum Sensing in Space Counting cycles in planar graphs Wave turbulence in the Schrödinger-Helmholtz equation Hunt for an Earth-twin |