abstract:
The Curry-Howard Isomorphism motivates the well known proofs-as-programs 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 epsilon-monads to be able to strengthen the function type. Epsilon-monads are monads that support a membership predicate. Epsilon-monads enabled the development of a bind-induction 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.