![]() |
![]() |
University of Birmingham > Talks@bham > Theoretical computer science seminar > Two extensions of Reynolds' Relational Parametricity: Classical Mechanics and Dependent Types
Two extensions of Reynolds' Relational Parametricity: Classical Mechanics and Dependent TypesAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Paul Levy. Reynolds’ theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds’ original work exploited the typing discipline of the polymorphically typed λ-calculus System F, but there is now considerable interest in extending relational parametricity to type systems that are richer and more expressive than that of System F. In this talk I’ll cover two recent extensions of Reynolds’ theory of parametricity that I have worked on. Firstly, I link Reynolds’ relational parametricity with Noether’s theorem for deriving conservation laws of classical mechanical systems. I propose an extension of System Fω with new kinds, types and term constants for writing programs that describe classical mechanical systems in terms of their Lagrangians. We show, by constructing a relationally parametric model of an extension of Fω, that relational parametricity is enough to satisfy the hypotheses of Noether’s theorem, and so to derive conserved quantities for free, directly from the polymorphic types of Lagrangians expressed in our system. Secondly, I will present a relationally parametric denotational model of dependent type theory. This model uniformly interprets all types as reflexive graphs, thereby building in the relational interpretation of all types. A sample application of this model is to show that all indexed functors expressible in the calculus have initial algebras via a Church encoding. This portion of the talk is joint work with Neil Ghani and Patricia Johann. 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 listsCargo Theoretical Physics Journal Club and Group Meeting Featured talksOther talksModelling uncertainty in image analysis. Geometry of alternating projections in metric spaces with bounded curvature Provably Convergent Plug-and-Play Quasi-Newton Methods for Imaging Inverse Problems Quantum simulations using ultra cold ytterbium Metamaterials for light-matter interaction studies Ultrafast, all-optical, and highly efficient imaging of molecular chirality |