Galois is pleased to host the following tech talk.
These talks are open to the interested public–please join us!
(There is no need to pre-register for the talk.)
title:
Parametricity, Quotient types, and Theorem transfer
speaker:
Brian Huffman
time:
Tuesday, 05 March 2013, 10:30am.
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
A polymorphic function may be instantiated at many different types; if
the function is parametrically polymorphic, then all of its instances
must behave uniformly. Reynolds’ parametricity theorem expresses this
precisely, in terms of binary relations derived from types. One
application of the parametricity theorem is to derive Wadler-style
“free theorems” about a polymorphic function from its type;
e.g. rev :: [a] -> [a] must satisfy
map f (rev xs) = rev (map f xs).
In this talk, I will show how to apply many of the ideas behind
parametricity and free theorems in a new setting: formal reasoning
about quotient types. Using types-as-binary-relations, we can
automatically prove that corresponding propositions about quotient
types and their representation types are logically equivalent. This
design is implemented as the Transfer package in the Isabelle theorem
prover, where it is used to automate many proofs about quotient types.
bio:
Brian Huffman is a recent PhD graduate from the Department of Computer
Science at Portland State University, now at Galois after completing a
postdoc at the Technical University of Munich. He has been an avid
Haskell programmer since 2001, and has contributed to the development
of the Isabelle interactive theorem prover since 2005, with an
emphasis on tools for verifying lazy functional programs. Several of
Brian’s formalizations can be found online at the Archive of Formal Proofs.