Tech Talk: Constructing A Universal Domain for Reasoning About Haskell Datatypes

October 6th, 2009 by Levent Erkok

The October 13th Galois Tech Talk will be delivered by Brian Huffman, titled “Constructing a Universal Domain for Reasoning About Haskell Datatypes.”

• Date: Tuesday, October 13th, 2009
• Time: 10:30am – 11:30am
• Location: Galois, Inc.
  421 SW 6th Ave. Suite 300
  (3rd floor of the Commonwealth Building)
  Portland, OR 97204

Abstract: Existing theorem prover tools do not adequately support reasoning about general recursive datatypes. Better support for such datatypes would facilitate reasoning about a wide variety of real-world programs, including those written in continuation-passing style, that are beyond the scope of current tools.

This paper introduces a new formalization of a universal domain that is suitable for modeling general recursive datatypes. The construction is purely definitional, introducing no new axioms. Defining recursive types in terms of this universal domain will allow a theorem prover to derive strong reasoning principles, with soundness ensured by construction.

Bio: Brian Huffman is a PhD student in Computer Science at Portland State University, working with advisor John Matthews. He studies formal reasoning with the Isabelle theorem prover, specializing in formalized mathematics and semantics of functional languages. He is currently the maintainer of Isabelle/HOLCF, a logic for domain theory.

---

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities. The talks are open and free. An RSVP is not required, but feel free to contact the organizer with questions and comments.

Leave a Reply

Name

Email address (will not be published)

Website (optional)

Comments