Brian Huffman

I am a recent PhD graduate from the Department of Computer Science at Portland State University (previously at the OGI School of Science & Engineering at OHSU). I work with the theorem prover Isabelle.

Current Research Interests

Domain Theory

I am currently the maintainer of HOLCF, a library of domain theory for the Isabelle theorem prover.

My thesis project involves the development of tools for defining recursive functions and recursive datatypes in HOLCF. Read more about it in my PhD thesis.

My Stuff

Isabelle Theories

Type Constructor Classes and Monad Transformers

June 2012. These theories contain a formalization of first class type constructors and axiomatic constructor classes for HOLCF. This work is described in detail in the ICFP 2012 paper Formal Verification of Monad Transformers by the author. The formalization is a revised and updated version of earlier joint work with Matthews and White. Based on the hierarchy of type classes in Haskell, we define classes for functors, monads, monad-plus, etc. Each one includes all the standard laws as axioms. We also provide a new user command, tycondef, for defining new type constructors in HOLCF. Using tycondef, we instantiate the type class hierarchy with various monads and monad transformers.

Free Boolean Algebra

March 2010. This theory defines a type constructor representing the free boolean algebra over a set of generators. Values of type (α)formula represent propositional formulas with uninterpreted variables from type α, ordered by implication. In addition to all the standard boolean algebra operations, the library also provides a function for building homomorphisms to any other boolean algebra type.

Stream Fusion

April 2009. Stream Fusion is a system for removing intermediate list structures from Haskell programs; it consists of a Haskell library along with several compiler rewrite rules. (The library is available online.) These theories contain a formalization of much of the Stream Fusion library in HOLCF. Lazy list and stream types are defined, along with coercions between the two types, as well as an equivalence relation for streams that generate the same list. List and stream versions of map, filter, foldr, enumFromTo, append, zipWith, and concatMap are defined, and the stream versions are shown to respect stream equivalence.

Countable Ordinals

November 2005. This development defines a well-ordered type of countable ordinals. It includes notions of continuous and normal functions, recursively defined functions over ordinals, least fixed-points, and derivatives. Much of ordinal arithmetic is formalized, including exponentials and logarithms. The development concludes with formalizations of Cantor Normal Form and Veblen hierarchies over normal functions.

Papers

Formal Verification of Monad Transformers

International Conference on Functional Programming (ICFP'12), Copenhagen, Denmark, September, 2012. Publication pending.

HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs

PhD thesis, Portland State University, 2012. (pdf)

Proof Pearl: A New Foundation for Nominal Isabelle

Brian Huffman and Christian Urban. In Matt Kaufmann and Lawrence C. Paulson, editors, Interactive Theorem Proving - 1st International Conference (LNCS 6172), pages 35-50, Springer, 2010. (pdf)

A Purely Definitional Universal Domain

22nd International Conference on Theorem Proving in Higher Order Logics, Munich, Germany, August, 2009. (pdf)

Reasoning with Powerdomains in Isabelle/HOLCF

21st International Conference on Theorem Proving in Higher Order Logics (Emerging Trends), Montreal, Quebec, Canada, August, 2008. (pdf)

Transfer Principle Proof Tactic for Nonstandard Analysis

NETCA 2005, August 2005. (pdf) (slides)

Axiomatic Constructor Classes in Isabelle/HOLCF

Brian Huffman, John Matthews and Peter White. In Joe Hurd, Edward Smith, and Ashish Darbari, editors, Theorem Proving in Higher Order Logics - 18th International Conference, TPHOLs 2005, Oxford, UK, August 2005, Proceedings, pages 147-162, Oxford, UK, August 2005. (pdf) (slides)

Semantics for ML Polymorphism in Isabelle/HOL

Research Proficiency Exam (RPE), OGI School of Science and Engineering at OHSU, May 2004. (pdf) (slides)

Talks

HOLCF '11: A Definitional Domain Theory for Verifying Functional Programs

PhD Thesis Defense, Portland State University, July 13, 2011. (pdf)

Verifying Stream Fusion with Isabelle/HOLCF

Galois Technical Seminar, June 30, 2009. (pdf)

Deflation Chains and Induction Rules for Haskell Types

Presented at Portland State University, November 7, 2008. (pdf)

A Deflation Model for Haskell Types

Presented at Portland State University, October 10, 2008. (pdf)

Powerdomains in Isabelle/HOLCF

Galois Technical Seminar, February 26, 2008. (pdf)
Earlier version presented at PSU, February 8, 2008. (pdf)

A Framework for Embedding Functional languages in Isabelle

Presented at Portland State University, August 9, 2007. (pdf)

Embedding GHC-Core in Isabelle

Presented at Galois, March 6, 2007. (pdf)

Semantics for ML Polymorphism in Isabelle/HOL

Research Proficiency Exam (RPE), Portland State University, October 12, 2006. (pdf)

Bringing Isabelle/HOLCF Closer to Haskell

Pattern matching combinators for Isabelle/HOLCF. Presented at Portland State University, November 16, 2005. (pdf)
Earlier version, presented October 28, 2005. (pdf)

Last Updated: July 9, 2012