[Pl-seminar] Semantics Seminar Schedule

[Mitchell Wand]

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

Amal Ahmed
TTI-Chicago

All for Nothing: Gradual Typing with Polymorphism and Blame

Static and dynamic typing offer complementary advantages: static
typing provides early error detection, efficient execution, and better
documentation of code, whereas dynamic typing encourages rapid
development and makes it easier to adapt to changing requirements.
As a result, they each have their adherents, but recently interest has
emerged in a 'third way' that combines the best of both worlds.

In this talk, I will present a language that integrates statically
typed and dynamically typed components, similar to the gradual types
of Siek and Taha (2006), and show how to extend it to incorporate
parametric polymorphism.  This language, dubbed the polymorphic blame
calculus, is a core calculus of casts between more and less precise
types.  Our system includes a notion of blame (as found in contracts),
which allows us to show that when more-typed and less-typed portions
of a program interact, that any type failures are due to the
less-typed portion.

Values of polymorphic type satisfy a strong semantic property known as
relational parametricity.  Our system permits a dynamically typed
value to be cast to a polymorphic type, with the type enforced by
dynamic sealing.  We have shown that this method of enforcement is so
strong as to ensure relational parametricity.

(Joint work with Robby Findler, Jacob Matthews, and Philip Wadler)

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

Amal will be with us all day on Wed 10/22.  If you'd like to talk to
her, let me know and we'll work out a schedule.

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

Upcoming Events:

# Wed 10/29 Aaron Turon: Spec# and Boogie
# Wed 11/5 Riccardo Pucella: Stateful RCF
# Wed 11/12 no seminar
# Wed 11/19 Geoffrey Mainland (Harvard): Flask: Functional Programming
  for sensor networks (tentative)

--Mitch