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 Types

Add 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.