[Club2] Talk by Brian Huffman -- Wed. Nov. 9, 2PM, room: "Alan Turing"

[Andrei Popescu]

Dear All, 

On Wednesday, Brian will present HOLCF-'11 and applications.  

Best regards, 
  Andrei 

Brian Huffman 
HOLCF-'11: A Definitional Domain Theory for Verifying
Functional Programs
====================================================
Wed. Nov. 9, 14:00, MI 00.09.055 ("Alan Turing")

(Note: This is a reprise of the author's PhD thesis defense talk,
originally presented on July 13, 2011 at Portland State University.)

HOLCF is an interactive theorem proving system that uses the
mathematics of domain theory to reason about programs written in
functional programming languages. This thesis introduces HOLCF-'11, a
thoroughly revised and extended version of HOLCF that advances the
state of the art in program verification: HOLCF-'11 can reason about
many program definitions that are beyond the scope of other formal
proof tools, while providing a high degree of proof automation. The
soundness of the system is ensured by adhering to a definitional
approach: New constants and types are defined in terms of previous
concepts, without introducing new axioms.

Major features of HOLCF-'11 include two high-level definition
packages: the Fixrec package for defining recursive functions, and the
Domain package for defining recursive datatypes. Each of these uses
the domain-theoretic concept of least fixed points to translate
user-supplied recursive specifications into safe low-level
definitions. Together, these tools make it easy for users to translate
a wide variety of functional programs into the formalism of HOLCF.
Theorems generated by the tools also make it easy for users to reason
about their programs, with a very high level of confidence in the
soundness of the results.

As a case study, we present a fully mechanized verification of a model
of concurrency based on powerdomains. The formalization depends on
many features unique to HOLCF-'11, and is the first verification of
such a model in a formal proof tool.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/club2/attachments/20111105/46fd6bd4/attachment.html>