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:20160313T020000 RDATE:20160313T020000 TZOFFSETFROM:-0800 TZOFFSETTO:-0700 TZNAME:PDT END:DAYLIGHT END:VTIMEZONE BEGIN:VEVENT CREATED;VALUE=DATE-TIME:20160314T224157Z DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20160318T113000 DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20160318T103000 DTSTAMP;VALUE=DATE-TIME:20160314T224157Z LAST-MODIFIED;VALUE=DATE-TIME:20160314T224157Z UID:http://calagator.org/events/1250469962 DESCRIPTION:abstract: \;\n \;\nThe Curry-Howard Isomorphism motivat es the well known proofs-as-programs interpretation. Under that interpre tation\, sufficiently different proofs yield different programs. This wo rk is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example\, we discovered that the sta ndard type bind \;\n(M a ->\; (a ->\; M b) ->\; M b) does not c ontain enough information to allow many proofs to go through. For lists\ , an implicit assumption on the function of type ( a ->\; M b) is that the input of type a is an element of the list of type M b. We developed an new typeclass of epsilon-monads to be able to strengthen the functio n type. Epsilon-monads are monads that support a membership predicate. E psilon-monads enabled the development of a bind-induction proof rule whi ch allows the extraction of monadic programs using the bind operator. Al so\, epsilon monads allow for extensional specifications of monadic prog rams. We used the Coq theorem prover to formalize the definitions and to prove many properties of the formalization. This is joint work with Had i Shafe’i. \;\n \;\nbio: \;\n \;\nJames Caldwell is Professo r and Head of the Computer Science Department at the University of Wyomi ng. He earned his PhD from Cornell in the Nuprl group advised by Robert Constable. Before moving to the University of Wyoming in 1998\, he was a researcher in the formal methods group at the NASA Langley Research cen ter. He moved to NASA from the Electric Corporate R&\;D center in Sch enectady\, NY where he was first exposed to formal verification. He has MS and BS degrees in computer science from SUNY Albany. Before coming to computer science he studied painting and sculpture at the School of the Museum of Fine Arts\, Boston. \;\n\n\nTags: Galois tech talk\, curry -howard isomorphism\, proofs\n\nImported from: http://calagator.org/even ts/1250469962 URL:http://galois.com/blog/2016/03/tech-talk-toward-extracting-monadic-pr ograms-from-proofs/ SUMMARY:Galois Tech talk: Toward Extracting Monadic Programs from Proofs LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US SEQUENCE:1 END:VEVENT END:VCALENDAR