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

[Daniel Brown]

Ahem, the question I meant to ask was: How many other people are  
interested in seeing both the BC talk and Aaron's talk?

On Oct 29, 2007, at 2:28 PM, Daniel Brown wrote:

> 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