BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:STANDARD
DTSTART:20121104T020000
RDATE:20121104T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20130301T020956Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130305T113000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20130305T103000
DTSTAMP;VALUE=DATE-TIME:20130301T020956Z
LAST-MODIFIED;VALUE=DATE-TIME:20130301T020956Z
UID:http://calagator.org/events/1250463749
DESCRIPTION:Presented by Brian Huffman.
\;\n
\;\nA polymorphic func
tion may be instantiated at many different types\; if the function is pa
rametrically polymorphic\, then all of its instances must behave uniform
ly. Reynolds' parametricity theorem expresses this precisely\, in terms
of binary relations derived from types. One application of the parametri
city 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).
\;\n
\;\nIn 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 correspondin
g propositions about quotient types and their representation types are l
ogically equivalent. This design is implemented as the Transfer package
in the Isabelle theorem prover\, where it is used to automate many proof
s about quotient types.\n\nTags: galois\, formal methods\, tech talk\n\n
Imported from: http://calagator.org/events/1250463749
URL:https://corp.galois.com/blog/2013/2/28/tech-talk-parametricity-quotie
nt-types-and-theorem-transfer.html
SUMMARY:Galois Tech Talk: Parametricity\, Quotient types\, and Theorem tr
ansfer
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR