![]() |
![]() |
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 listsNuclear physics seminars Type the title of a new list here What's on in Physics?Other talksQuantum simulations using ultra cold ytterbium Modelling uncertainty in image analysis. Geometry of alternating projections in metric spaces with bounded curvature Metamaterials for light-matter interaction studies Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Disorder relevance for non-convex random gradient Gibbs measures in d=2 |