[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

We have two events next week:

================================================================

NU Programming Languages Seminar
Tuesday, 1/22/08
11:45am-1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Christian Urban
TU Munich

Nominal Techniques in the Theorem Prover Isabelle or, How
Not to be Intimidated by the Variable Convention

Abstract:

Dealing with binders, renaming of bound variables, capture-avoiding
substitution, etc., is very often a major problem in formal proofs,
especially in proofs by induction. In informal proofs by induction
one often assumes a variable convention in order to sidestep all
problems and to obtain simple proofs. Unfortunately, this convention
is usually not formally justified, which makes it hard to formalise
such proofs. In this talk I will show how strong induction principles
can be formally derived that have the variable convention already
built-in. I will also show that the variable convention depends on
some non-trivial conditions in order to be a sound reasoning principle.
The aim of this work is to provide all proving technology necessary
for reasoning conveniently about the lambda-calculus and programming
languages.

================================================================

NU Programming Languages Seminar
Wednesday, 1/23/08
11:45am-1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)

Greg Morrisett
Harvard University
Ynot:  integrating effects with dependent types

I want a type system that will let me capture anything from simple
type-safety properties, to contracts, and even go all the way to full
correctness.  Ideally, the system should have a "pay-as-you-go"
property: If you only want simple types, then everything can and
should be automated.  If you want to prove really deep properties,
then you should be able to express this, but you may have to pay the
price of writing some explicit proofs (or proof scripts).
Furthermore, the language should have a uniform way to treat models,
specifications, types, code, and proofs so that abstraction is
feasible.

It turns out that Coq (more or less) has such a type system.
Unfortunately, it only works on purely functional programs, where
effects of any kind are forbidden, including non-termination, mutable
state, continuations, I/O, etc.  For the past year or two, we've been
figuring out how to add these features to Coq.  There are some really
tricky semantic issues that we had to solve, and a number of
implementation issues that we are still working on.  We've now written
some (mildly) interesting code that leverages these features,
including thing like hash-tables and parser combinators.  The
interfaces capture (partial) correctness, and are designed, in the
style of separation logic, with frame properties that make reasoning
compositional.

================================================================

Upcoming Events:

# Wed 1/30 Gene Cooperman: Multi-Core Processors: Background and
   Issues from an Applications Viewpoint 
# Wed 2/6 Riccardo Pucella: The Manticore project
# Wed 2/13 Norman Ramsay: Dataflow 'Optimization' for the Semantically Inclined
# Wed 2/20 et seq are open.  Come give a talk!

--Mitch