Brian Huffman
I am a PhD student in the
Department of Computer Science at Portland State University (formerly 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 Stuff
Isabelle Theories
- VectorCalculus
- Inner product spaces, gradient derivatives, vectors and square matrices.
(browse source)
(download)
- Bits
- A formalization of modular arithmetic and bitwise operators.
Type constructors for integers mod n and n-bit words are defined.
(browse source)
(download)
- Ordinal
- A theory of countable ordinals in Isabelle/HOL, available online at the
Archive of Formal Proofs.
- Transfer
- A formalization of the transfer principle of nonstandard analysis,
as presented at NETCA 2005. It has since been integrated into the
HOL-Complex theory of Isabelle 2005.
(browse source)
(download)
- HOL-Constructor
- A formalization of axiomatic constructor classes (HOL version).
(browse source)
(download)
Papers
- A Purely Definitional Universal Domain
- Submitted to TPHOLs 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
- 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: March 16, 2009