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.)
Please note the unusual time for this talk.
It is on Thursday at 11am.
title:
Formal Verification of Monad Transformers
speaker:
Brian Huffman
time:
Thursday, 30 August 2012, 11:00am
location:
Galois Inc.
421 SW 6th Ave. Suite 300,
Portland, OR, USA
(3rd floor of the Commonwealth building)
abstract:
We present techniques for reasoning about constructor classes that (like the monad class) fix polymorphic operations and assert polymorphic axioms. We do not require a logic with first-class type constructors, first-class polymorphism, or type quantification; instead, we rely on a domain-theoretic model of the type system in a universal domain to provide these features. These ideas are implemented in the Tycon library for the Isabelle theorem prover, which builds on the HOLCF library of domain theory. The Tycon library provides various axiomatic type constructor classes, including functors and monads. It also provides automation for instantiating those classes, and for defining further subclasses. We use the Tycon library to formalize three Haskell monad transformers: the error transformer, the writer transformer, and the resumption transformer. The error and writer transformers do not universally preserve the monad laws; however, we establish datatype invariants for each, showing that they are valid monads when viewed as abstract datatypes.
bio:
Brian Huffman is a recent PhD graduate from the Department
of Computer Science at Portland State University, now working as a postdoc at
the Technical University of Munich. He has been an avid Haskell programmer
since 2001, and has contributed to the development of the Isabelle interactive
theorem prover since 2005, with an emphasis on tools for verifying lazy
functional programs. Several of Brian’s formalizations can be found online at
the Archive of Formal Proofs.