Rutgers University

Parametric
Polymorphism, Observational Equivalence, and Monadic Computation

Abstract:

In this talk we propose a calculus, called PolyComp, supporting polymorphism, type- and term-level recursion, and computation (i.e., monadic) types. We give PolyComp an operational semantics, which we use to construct parametric models for it. We show that equivalence in these models coincides with corresponding notions of observational equivalence and that these, in turn, depend on the types at which observations can be made. Finally, we use our models to derive operational properties of PolyComp which are independent of the choice of monad, and also discuss how monads which model specific computational effects can be incorporated into our framework. Successfully incorporating new language features into parametric models of observational equivalence is nontrivial because operational techniques are often not modular. In particular, term-level recursion typically does not interact well with other features. To our knowledge, ours is the first parametric model of observational equivalence for a calculus supporting all the features of PolyComp.

This
is joint work with Neil Ghani.

Host: Bob Harper

Appointments: Margaret Weigand

Wednesday, December 14, 2005

3:30 p.m.

Wean Hall 8220

Principles
of Programming Seminars