Mathematics, Logic and Computation

A Satellite workshop of ICALP03

In honour of N.G. de Bruijn's 85th anniversary

4-5 July 2003

Eindhoven, the Netherlands

http://www.cedar-forest.org/forest/events/Bruijn03/


Remarks on Isomorphisms of Simple Inductive Types

David Chemouil and Sergei Soloviev

Abstract

We study isomorphisms of types in the system of simply-typed lambda-calculus 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.