BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.bham.ac.uk//v3//EN
BEGIN:VEVENT
CATEGORIES:Theoretical computer science seminar
SUMMARY:Two extensions of Reynolds' Relational Parametrici
ty: Classical Mechanics and Dependent Types - Bob
Atkey
DTSTART:20131108T160000Z
DTEND:20131108T170000Z
UID:TALK1234AT
URL:/talk/index/1234
DESCRIPTION:Reynolds’ theory of relational parametricity captu
res the invariance\nof polymorphically typed progr
ams under change of data\nrepresentation. Reynolds
’ original work exploited the typing\ndiscipline o
f the polymorphically typed λ-calculus System F\,
but there\nis now considerable interest in extendi
ng relational parametricity to\ntype systems that
are richer and more expressive than that of System
\nF.\n\nIn this talk I'll cover two recent extensi
ons of Reynolds' theory of\nparametricity that I h
ave worked on.\n\nFirstly\, I link Reynolds’ relat
ional parametricity with Noether’s\ntheorem for de
riving conservation laws of classical mechanical\n
systems. I propose an extension of System Fω with
new kinds\, types and\nterm constants for writing
programs that describe classical mechanical\nsyste
ms in terms of their Lagrangians. We show\, by con
structing a\nrelationally parametric model of an e
xtension of Fω\, that relational\nparametricity is
enough to satisfy the hypotheses of Noether’s\nth
eorem\, and so to derive conserved quantities for
free\, directly from\nthe polymorphic types of Lag
rangians expressed in our system.\n\nSecondly\, I
will present a relationally parametric denotationa
l model\nof dependent type theory. This model unif
ormly interprets all types as\nreflexive graphs\,
thereby building in the relational interpretation
of\nall types. A sample application of this model
is to show that all\nindexed functors expressible
in the calculus have initial algebras via\na Churc
h encoding. This portion of the talk is joint work
with Neil\nGhani and Patricia Johann.
LOCATION:UG10 Learning Centre
CONTACT:Paul Levy
END:VEVENT
END:VCALENDAR