![]() |
![]() |
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 listsTheoretical Physics Seminars Molecular and Medical Physics Seminar Series Aerospace Seminar SeriesOther talksWave turbulence in the Schrödinger-Helmholtz equation TBA Hunt for an Earth-twin TBA Quantum Sensing in Space Control variates for computing transport coefficients |