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:DAYLIGHT
DTSTART:20140309T020000
RDATE:20140309T020000
TZOFFSETFROM:-0800
TZOFFSETTO:-0700
TZNAME:PDT
END:DAYLIGHT
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20140728T185801Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140801T120000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20140801T110000
DTSTAMP;VALUE=DATE-TIME:20140728T185801Z
LAST-MODIFIED;VALUE=DATE-TIME:20140728T185801Z
UID:http://calagator.org/events/1250466723
DESCRIPTION:Abstract:&#13\;\nRecords in Haskell are notoriously difficult
  to compose\; many solutions have been proposed. Vinyl lies in the space
  of library-level approaches\, and addresses polymorphism\, extensibilit
 y\, effects and strictness. I describe how Vinyl approaches record famil
 ies over arbitrary key spaces using a Tarski universe construction\, as 
 well as a method for immersing each field of a record in a chosen effect
  modality. Moreover\, I give a characterization of records as sheaves of
  types\, which provides a clear motivation for the safety of subtyping a
 nd coercion of records\, and a path toward records with non-trivial topo
 logies on their key spaces. Lastly\, I describe an interpretation of Vin
 yl-style records into Type Theory as finite products over containers\, l
 eading to many possible and interesting extensions\, such as composition
 al universes of polymorphic variants\, as well as inductive and coinduct
 ive types.&#13\;\n&#13\;\nBio:&#13\;\nI'm an amateur type theorist who s
 tudied Historical Linguistics during my undergraduate at UC Berkeley\, s
 pecializing in Ancient Greek\, Sumerian\, Akkadian and Anglo-Saxon. I'm 
 particularly interested in type-theoretic syntax and semantics for natur
 al language\, and am presently exploring the use of multi-modal combinat
 ory categorial grammar for interpreting the hyperbaton-rich syntax of an
 cient Indo-European languages. In addition to my interest in linguistics
 \, I have become obsessed with extensionality\, realizability and PER se
 mantics for Martin-Löf Type Theory\, and am currently trying to come up 
 with an extension to Observational Type Theory which internalizes furthe
 r extensional concepts\, such as union\, intersection\, image and PER ty
 pes whilst retaining decidability of type checking.&#13\;\n\n\nTags: Gal
 ois tech talk\n\nImported from: http://calagator.org/events/1250466723
URL:http://galois.com/blog/2014/07/tech-talk-vinyl-records-haskell-type-t
 heory/
SUMMARY:Galois tech talk: Vinyl: Records in Haskell & Type Theory
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:1
END:VEVENT
END:VCALENDAR