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