# Abstracts

Here are the abstracts of most of the works you can find referenced in my publications page, where you will find the pointers to the online available documents.

## Provable isomorphisms of types: from Lambda Calculus to Information Retrieval and Language Design.

This book (see here for a more detailed overview) is devoted to the study of the notion of type-isomorphisms in functional languages, both from a theoretical and a practical point of view.

Based on my PhD dissertation, it 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 (you can test a sample implementation right now: english or french).

## Provable isomorphisms of types

A constructive characterization is given of the isomorphisms which must hold in all models of the typed lambda calculus with surjective pairing. By the close relation between closed Cartesian categories and models of these calculi, we also produce a characterization of those isomorphisms which hold in all CCC's. By the correspondence between these calculi and proofs in intuitionistic positive propositional logic, we thus provide a characterization of equivalent formulae of this logic, where the definition of equivalence of terms depends on having ``invertible'' proofs between the two terms. Rittri (1989), on types as search keys in program libraries, provides an interesting example of use of these characterizations.

## Constuctively Equivalent Propositions and Isomorphisms of Objects (or Terms as Natural Transformations)

In these notes, we sketch a recent application of the typed and type-free l-calculus to Proof Theory and Category Theory. The proof is fairly incomplete and we refer the reader interested in the lengthy technical details to Bruce & DiCosmo & Longo [1990]. Our main purpose here is to hint a logical framework for the result therein, in a rather preliminary and problematic form.

The questions we raise here are the following: when two propositions can be considered as truly equivalent? Or, when is it that types may be viewed at as isomorphic under all circumstances?

In proof-theoretic terms this may be understood as in definition 0.1 below, on the grounds of the ``types-as-propositions'' analogy between the typed l-calculus and intuitionistic propositional logic (bf IPL).

## Type isomorphisms in a type assignment framework

This is a conference extended abstract of the following journal paper.

## Deciding Type isomorphisms in a type assignment framework

We exhibit confluent and effectively weakly normalizing (thus decidable)
rewriting systems for the full equational theory underlying cartesian closed
categories, and for polymorphic extensions of it. The l -calculus extended
with surjective pairing has been well-studied in the last two decades. It is not
confluent in the untyped case, and confluent in the typed case. But to the best
of our knowledge the present work is the first treatment of the lambda calculus
extended with surjective pairing * and* terminal object via a * confluent*
rewriting system, and is the first solution to the decidability problem of the
full equational theory of Cartesian Closed Categories extended with *
polymorphic types*. Our approach yields conservativity results as well. In
separate papers we apply our results to the study of provable type isomorphisms,
and to the decidability of equality in a typed l -calculus with subtyping.

## Second order Isomorphic Types. A proof theoretic study on second order lambda-calculus with surjective pairing and terminal object

We investigate invertible terms and isomorphic types in the second order
lambda calculus extended with surjective pairs and terminal (or * Unit*)
type. These two topics are closely related: on one side, the study of
invertibility is a necessary tool for the characterization of
isomorphic types; on the other hand, we need the notion of isomorphic types
to study the typed invertible terms. The result of our investigation is
twofold: we give a constructive characterization of the invertible terms,
extending previous work by Dezani and
Bruce-Longo citeDezani,BruceLongo85, and a decidable equational theory
of the isomorphisms of types which hold in all models of the calculus,
which is a conservative extension to the second order case of the results
previously achieved for the case of first
order typed calculi. Via the Curry-Howard correspondence, this work also
provides a decision procedure for * strong equivalence* of formulae in
second order intuitionistic positive propositional logic, that is suitable
to search equivalent proofs in automated deduction systems.

Keywords: Type Isomorphisms, Invertibility, System F, Polymorphism, Surjective Pairing, Terminal Object, Equational Theories, l -Calculus, Proof Search.

## Type isomorphisms of modules

We study a formal notion of type isomorphism for module signatures, which naturally extends the notion of isomorphism for types in functional languages. Isomorphisms between module types surprisingly have nontrivial interactions with the theory of isomorphisms of the base language to which the module system is added. We investigate the power of this notion in equating module signatures, and we study its decidability. This work does not impose any limitative assumption on the module system as we handle type declarations in signatures, type sharing and higher order modules.

## A confluent reduction system for the lambda-calculus with surjective pairing and terminal object

This is a conference extended abstract of the following journal paper.

## A confluent reduction system for the lambda-calculus with surjective pairing and terminal object

We exhibit confluent and effectively weakly normalizing (thus decidable)
rewriting systems for the full equational theory underlying cartesian closed
categories, and for polymorphic extensions of it. The l -calculus extended
with surjective pairing has been well-studied in the last two decades. It is not
confluent in the untyped case, and confluent in the typed case. But to the best
of our knowledge the present work is the first treatment of the lambda calculus
extended with surjective pairing * and* terminal object via a * confluent*
rewriting system, and is the first solution to the decidability problem of the
full equational theory of Cartesian Closed Categories extended with it
polymorphic types. Our approach yields conservativity results as well. In
separate papers we apply our results to the study of provable type isomorphisms,
and to the decidability of equality in a typed l -calculus with subtyping.

## A confluent reduction for the extensional typed lambda-calculus with pairs, sums, recursion and terminal object

This is a conference extended abstract of the following journal paper.

## Simulating Expansions without Expansions

We add extensional equalities for the functional and product types to the typed
l -calculus with not only products and terminal object, but also sums
condinitialand initial object and bounded recursion (a version of recursion
that does not allow recursive calls of infinite length). We provide a confluent
and strongly normalizing (thus decidable) rewriting system for the calculus,
that stays confluent when allowing unbounded recursion. For that, we turn the
extensional equalities into * expansion* rules, and not into contractions as
is done traditionally.
We first prove the calculus to be weakly confluent, which is a more complex and
interesting task than for the usual l -calculus. Then we provide an effective
mechanism to simulate expansions without expansion rules, so that the strong
normalization of the calculus can be derived from that of the underlying,
traditional, non extensional system. These results give us the confluence of the
full calculus, but we also show how to deduce confluence directly form our
simulation technique, without the weak confluence property.

## Combining first order algebraic rewriting systems, recursion and extensional lambda calculi

It is well known that confluence and strong normalization are preserved when
combining left-linear * algebraic rewriting systems* with the simply typed
lambda calculus. It is equally well known that confluence fails when adding
either the usual extensional rule for eta, or recursion together with the
usual contraction rule for surjective pairing.

We show that * confluence* and * normalization* are * modular*
properties for the combination of * left-linear* algebraic rewriting systems
with typed lambda calculi enriched with * expansive* extensional rules for
eta and surjective pairing. For that, we use a translation technique
allowing to simulate expansions without expansion rules. We also show that
confluence is maintained in a modular way when adding * fixpoints*. This
result is also obtained by a simple translation technique allowing to simulate
bounded recursion with beta reduction.

## Expanding Extensional Polymorphism

We prove the confluence and strong normalization properties for second order lambda calculus equipped with an expansive version of eta-reduction. Our proof technique, based on a simple abstract lemma and a labelled l-calculus, can also be successfully used to simplify the proofs of confluence and normalization for first order calculi, and can be applied to various extensions of the calculus presented here.

## An extensional operational and axiomatic semantics for type-inference with recursion and algebraic data types

In this paper, we provide an operational semantics of core-ML with recursion and
algebraic data types which agrees precisely with the usual axiomatic semantics
* in the presence of extensionality axioms/*. This result has been missed
for a long time due to the traditional use of contractive reduction rules for
familiar extensional equalities like eta and Surjective Pairing: these rules
do not interact nicely with the implicit polimorphic typing discipline that is
the base of many strongly typed functional programming languages, as even such a
fundamental property as Subject Reduction does not hold in their presence.

We use here the more satisfactory approach to extensionality that uses expansion
rules, and then we can give a simple translation of (extensional) Core-ML into
(extensional) System F that preserves types * and* allows a proper simulation
of the reductions of Core-ML. This provides an operational notion of reduction
for Core-ML that takes into account the extensional equalities on the arrow and
the product types.

But this is not all: we also show how we can add, using some simple but powerful lemmas from the theory of rewriting, algebraic data types and recursion preserving confluence (hence determinacy) of the system under very liberal conditions.

To the author's best knowledge, this is the first satisfactory treatment of a polymorphic type inference systems in the presence of extensionality.

Keywords: type-inference, language design, rewriting, ML, semantics, algebraic data types

## Rewriting with polymorphic extensional lambda-calculus

We provide a confluent and strongly normalizing rewriting system, based on
expansion rules, for the * extensional/* second order typed lambda calculus
with product and unit types: this system siunitis the second order extension
of the lambda calculus associated to the Cartesian Closed Categories, and
corresponds to the Intuitionistic Positive Calculus with implication,
conjunction, quantification over proposition and the constant True. This
result is an important step towards a new theory of reduction based on expansion
rules, and gives a natural interpretation to the notion of second order
eta-long normal forms used in higher order resolution and unification, that
are here just the normal forms of our reduction system.

## On the Power of Simple Diagrams

In this paper we focus on a set of abstract lemmas that are easy to apply and turn out to be quite valuable in order to establish confluence and/or normalization modularly, especially when adding rewriting rules for extensional equalities to various calculi. We show the usefulness of the lemmas by applying them to various systems, ranging from simply typed lambda calculus to higher order lambda calculi, for which we can establish systematically confluence and/or normalization (or decidability of equality) in a simple way. Many result are new, but we also discuss systems for which our technique allows to provide a much simpler proof than what can be found in the literature.