|
Change #19643
2013-02-28
18:09:56
|
create
Calagator::Event
1250463749
Galois Tech Talk: Parametricity, Quotient types, and Theorem transfer
Roll back
| description |
nil |
→ |
Presented by Brian Huffman.
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. |
| end_time |
nil |
→ |
2013-03-05 11:30:00 -0800 |
| id |
nil |
→ |
1250463749 |
| start_time |
nil |
→ |
2013-03-05 10:30:00 -0800 |
| title |
nil |
→ |
Galois Tech Talk: Parametricity, Quotient types, and Theorem transfer |
| url |
nil |
→ |
https://corp.galois.com/blog/2013/2/28/tech-talk-parametricity-quotient-types-and-theorem-transfer.html |
| venue_id |
nil |
→ |
202390439 |
|