Computer Laboratory Home Page Search A-Z Directory Help
University of Cambridge Home Logic and Semantics Seminar
13th February, 2004: Vincent Balat
Computer Laboratory > Research > TSG > Logic and Semantics Seminar > 13th February, 2004: Vincent Balat

Speaker: Vincent Balat, Università di Genova
Title: Lambda-Calculus with Strong Sums:
Type Isomorphisms and Type-Directed Partial Evaluation
Time: 13th February, 2004, 14:00
Venue: William Gates Building, room FW11
Abstract:

The notion of type isomorphisms defines an equivalence relation upon the types of a programming language, that has practical interest for example for finding functions in libraries. I will speak about the problem of axiomatisation of these isomorphisms in the case of the lambda-calculus with product and sum types. I will show you how this issue leads us to the problem of normalisation of this calculus, and how we could solve it by creating a new normalisation tool, based on partial evaluation techniques.

Most of the work I will present has been done in collaboration with Marcelo Fiore and Roberto Di Cosmo.