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