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

[Daniel Brown]

I'm interested in seeing this, but it conflicts with Aaron's talk.  
Should we again consider rescheduling Aaron's talk?

  Dan

On Oct 28, 2007, at 3:03 PM, Mitchell Wand wrote:

> 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).
>
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar

-------------- next part --------------
HTML attachment scrubbed and removed