Atlas home || Conferences | Abstracts | about Atlas

Second St.Petersburg Days of Logic and Computability
August 24-26, 2003
Petersburg Department of Steklov Institute of Mathematics
St. Petersburg, Russia

Organizers
Sergei ADIAN (Russia), Sergei ARTEMOV (Russia/USA), Nikolai KOSSOVSKI (Russia), Maurice MARGENSTERN (France), Grigori MINTS (USA), Yuri MATIYASEVICH (Russia), the chairman, Nikolai NAGORNY (Russia), Vladimir OREVKOV (Russia), Anatol SLISSENKO (France)

View Abstracts
Conference Homepage

Extensional Isomorphisms of Inductive Types in Simply-Typed Lambda-Calculus
by
David Chemouil
IRIT, University Paul Sabatier, Toulouse
Coauthors: Sergei Soloviev (IRIT, University Paul Sabatier, Toulouse)

We study isomorphisms of types in the system of simply-typed lambda-cal­cu­lus with inductive types and recursion operators. It is shown that in some cases (multiproducts, copies of types), it is possible to add new reductions in such a way that strong normalisation and confluence of the calculus are preserved, and the isomorphisms may be regarded as intensional w.r.t. a stronger equality relation.

Date received: March 7, 2003

Copyright © 2003 by the author(s). The author(s) of this document and the organizers of the conference have granted their consent to include this abstract in Atlas Conferences Inc. Document # cajy-04.