Tech talk: Toward Extracting Monadic Programs from Proofs

  • Date Friday, March 18, 2016  Time 10:30 AM
  • Speaker James Caldwell
  • Location Galois Inc, 421 SW 6th Ave. Suite 300, Portland, OR, USA, (3rd floor of the Commonwealth building)
  • Galois is pleased to host the following tech talk.
    These talks are open to the interested public--please join us!
    (There is no need to pre-register for the talk.)

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.

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.