When: Wednesday, December 14, 3:30 p.m.- 5:00 p.m.

Where: 8220 Wean Hall

Patricia Johann

POP Seminar CANCELED

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

<< Back