[Club2] Update: move time to 2:15 pm -- Re: Room correction: "von Neumann" instead of "Turing" -- Talk by Brian Huffman

[Brian Huffman]

Hi all,

I would like to move my talk time this afternoon back by 15 minutes,
to 2:15 pm. (This is by request, so that Jasmin may attend.)

I'll see everyone in "von Neumann" then.

- Brian


On Sat, Nov 5, 2011 at 8:27 PM, Andrei Popescu <uuomul at yahoo.com> wrote:
> Here is the corrected announcement.
> Andrei
> Brian Huffman
> HOLCF-'11: A Definitional Domain Theory for Verifying
> Functional Programs
> ====================================================
> Wed. Nov. 9, 14:00, 01.11.038 ("John von Neumann")
> (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.
>
>
> _______________________________________________
> Club2 mailing list
> List page:
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/club2
> Webpage with calendar: http://www4.in.tum.de/proj/theoremprov/club2.html
>