Tech Talk: Verifying Stream Fusion with Isabelle/HOLCF

June 23rd, 2009 by Levent Erkok

The June 30th Galois Tech Talk will be delivered by Brian Huffman, titled “Verifying Stream Fusion with Isabelle/HOLCF”

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

Slides from the talk.

Abstract: Stream fusion is a system for removing intermediate data structures from Haskell programs that manipulate lists.  Formal verification of such libraries requires very precise modeling in a theorem prover, to avoid strictness-related bugs.

In this talk I will present a formalization of the stream fusion library in Isabelle/HOLCF, a theorem proving environment designed especially for reasoning about functional programs.  I will show how to prove the correctness of various stream functions using “fixed-point induction”, a powerful reasoning principle for general recursive functions.

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