Two extensions of Reynolds' Relational Parametricity: Classical Mechanics and Dependent Types

Add to your list(s) Download to your calendar using vCal

• Bob Atkey
• Friday 08 November 2013, 16:00-17:00
• UG10 Learning Centre.

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:

• Computer Science Departmental Series
• Computer Science Distinguished Seminars
• Theoretical computer science seminar
• UG10 Learning Centre
• computer sience

Note that ex-directory lists are not shown.