from lambda calculus to information retrieval and language design by Roberto Di Cosmo (dicosmo@dmi.ens.fr) Progress in Theoretical Computer Science. Birkhauser, 1995 ISBN 0-8176-3763-X
The full version of this contribution is available.
This newly published book may be of interest. It is a study of the notion of type-isomorphisms in functional languages, both from a theoretical and a practical point of view.
It is based on my PhD dissertation, but has been extensively revised, updated and provided with a completely new introduction to the topic, that makes it accessible to a wide spectrum of readers. It tries hard to provide a complete reference and discussion of all research done in this area, from the definition of confluent rewriting systems for typed lambda calculi equipped with various extensionality rules, to the characterization of isomorphisms of types in different typed calculi, to the applications to extensions of ML-style type-inference algorithms and the design of library search tools based on types.
A summary of the book is available.
Author's address:
LIENS
Ecole Normale Superieure
45, Rue d'Ulm
75005 Paris FRANCE