Viewing 0 current events matching “curryhoward isomorphism” by Location.
Sort By: Date  Event Name, Location , Default 

No events were found. 
Viewing 1 past event matching “curryhoward isomorphism” by Location.
Sort By: Date  Event Name, Location , Default 

Friday
Mar 18, 2016

Galois Tech talk: Toward Extracting Monadic Programs from Proofs – Galois, Inc abstract: The CurryHoward Isomorphism motivates the well known proofsasprograms interpretation. Under that interpretation, sufficiently different proofs yield different programs. This work is a step toward extracting monadic programs from proofs. In working with the list monad as a motivating example, we discovered that the standard type bind (M a > (a > M b) > M b) does not contain 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 epsilonmonads to be able to strengthen the function type. Epsilonmonads are monads that support a membership predicate. Epsilonmonads enabled the development of a bindinduction proof rule which allows the extraction of monadic programs using the bind operator. Also, epsilon monads allow for extensional specifications of monadic programs. We used the Coq theorem prover to formalize the definitions and to prove many properties of the formalization. This is joint work with Hadi Shafe’i. bio: James Caldwell is Professor and Head of the Computer Science Department at the University of Wyoming. 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 center. He moved to NASA from the Electric Corporate R&D center in Schenectady, 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. 