[Pl-seminar] Research talk at BC 11/02/07

[Mitchell Wand]

TITLE: Program Verification with Operational Type Theory
Speaker: Aaron Stump
Speaker Affiliation: Washington University in St. Louis

Date: 11-2-2007
Time: 11:00 AM - 12:30 PM
Location: Boston College Fulton Hall 513 (Lynch Center)

Directions to BC:  http://www.cs.bc.edu/~gtan/contact

ABSTRACT: Operational Type Theory (OpTT) is a formal system for writing
richly typed pure functional programs, and proving properties about
them.  OpTT's main contribution is in allowing possibly diverging or
aborting programs, while retaining both logical soundness and
decidability of type checking.  Traditional type theories based on the
Curry-Howard isomorphism have not been able to achieve this, since
diverging terms are unsound as proofs and spoil decidability of type
equality (which typically involves computation).  OpTT rejects the
Curry-Howard isomorphism, and strictly separates proofs from programs,
and formulas from types.  Nevertheless, proofs and programs can be
mutually dependent, thanks to proof irrelevance, which arises naturally
in OpTT from the separation of proofs and programs.  Example verified
programs include operations on containers like binary search trees,
where we statically verify that invariants like the BST property are
preserved; and language-processing examples such as an untyped lambda
calculus interpreter, where any result returned is verified not to
contain new free variables.

OpTT is being implemented in the Guru tool, a preliminary version of
which is available at www.guru-lang.org, together with a draft paper
on OpTT.

BIO: Aaron Stump received his PhD in Computer Science from Stanford
University in 2002.  His research interests are in language-based
program verification, automated reasoning, and type theory.  With
Hongwei Xi, he co-organizes the Programming Languages meets Program
Verification workshop (www.plpv.org).  With Clark Barrett and Albert
Oliveras, he also co-organizes the Satisfiability Modulo Theories
Competition (www.smt-comp.org).
-------------- next part --------------
HTML attachment scrubbed and removed