Author name cluster

M. Coppo

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

2 papers

1 author row

I&C Journal 1995 Journal Article

Principal Types and Unification for Simple Intersection Type Systems

M. Coppo
P. Giannini

In this paper we introduce a decidable restriction of the intersection type discipline. The restriction is based on a uniform principle rather than on a notion of rank. For this system we give a type checking algorithm that we prove to be sound and complete. An extended language of types with labelled intersections and intersection schemes is needed to describe the principal type of terms which turns out to be unique module a set of equations between labels. The unification algorithm far labelled types, that extends first order unification, could be used as a basis to define inference algorithms for other (more powerful) systems with intersection.

Details DOI

I&C Journal 1987 Journal Article

Type theories, normal forms, and D∞-lambda-models

M. Coppo
M. Dezani-Ciancaglini
M. Zacchi

A (non-standard) inverse-limit λ-model D∞ ∗ is constructed which has a non Hilbert-Post complete theory. Moreover, in D∞ ∗, a simple semantic characterization of normalizable terms is given. These results are proved using the properties of a generalized type assignment system which yields a filter model (Barendregt, Coppo, and Dezani-Ciancaglini, 1983, J. Symbolic. Logic, 48, 931–940; Coppo, Dezani-Ciancaglini, Honsell, and Longo, 1983, pp. 241–262, “Logic Colloquium '82, ” North-Holland, Amsterdam), isomorphic to D∞ ∗. The type assignment system is also proved complete with respect to an interpretation of types (in the term model of β-equality) based only on normalization properties. As an application a class of maximal monoids of normalizable terms is characterized.

Details DOI