[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

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

Olivier Danvy
Department of Computer Science, University of Aarhus, Denmark

A call-by-name normalization function for the simply typed
lambda-calculus with sums and products 


Abstract:

We report on the first call-by-name normalization function for the simply
typed lambda-calculus with sums and products that is purely functional
(no `gensym' and no control operators as well as no pre-computed state)
and that passes the Filinski test.  We present two definitions: one is
typeless and we wrote it in Scheme as well as in ML with a universal type
of values; the other is typeful and we formalized it in ML, using the
type inferencer as a logical framework.

Our solution to this open problem is remarkably simple: we use an
ordinary evaluation function towards a call-by-name domain of
continuation-passing values; and we invert it by instantiating the domain
of answers with a continuation-based code generating function towards
long beta-eta-normal forms using de Bruijn levels.  The resulting
normalization function is thus lightweight and it operates at native
speed.  For all we can see, it also lends itself gracefully to validating
extra equations over normal forms.

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

Olivier will be with us all day on Wed 8/6.  If you'd like to talk to
Olivier, let me know and we'll work out a (possibly wiki-based) schedule.

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

Upcoming Events:

No events scheduled.  Come give a talk!

--Mitch