Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(4)
Body of Knowledge
Intersection Types
Lambda Calculus
Standard Model
Subscribe
Academic
Publications
On isomorphisms of intersection types
On isomorphisms of intersection types,10.1145/1805950.1805955,ACM Transactions on Computational Logic,Mariangiola DezaniCiancaglini,Roberto Di Cosmo,
Edit
On isomorphisms of intersection types
BibTex

RIS

RefWorks
Download
Mariangiola DezaniCiancaglini
,
Roberto Di Cosmo
,
Elio Giovannetti
,
Makoto Tatsuta
The study of type isomorphisms for different λcalculi started over twenty years ago, and a very wide
body of knowledge
has been established, both in terms of results and in terms of techniques. A notable missing piece of the puzzle was the characterization of type isomorphisms in the presence of intersection types. While, at first thought, this may seem to be a simple exercise, it turns out that not only finding the right characterization is not simple, but that the very notion of isomorphism in
intersection types
is an unexpectedly original element in the previously known landscape, breaking most of the known properties of isomorphisms of the typed λcalculus. In particular, isomorphism is not a congruence and types that are equal in the standard models of
intersection types
may be nonisomorphic.
Journal:
ACM Transactions on Computational Logic  TOCL
, vol. 11, no. 4, pp. 124, 2010
DOI:
10.1145/1805950.1805955
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
portal.acm.org
)
(
portal.acm.org
)
(
portal.acm.org
)
References
(13)
A Filter Lambda Model and the Completeness of Type Assignment
(
Citations: 253
)
Henk Barendregt
,
Mario Coppo
,
Mariangiola Dezaniciancaglini
Journal:
Journal of Symbolic Logic  JSYML
, vol. 48, no. 4, pp. 931940, 1983
A typed lambda calculus with intersection types
(
Citations: 3
)
Viviana Bono
,
Betti Venneri
,
Lorenzo Bettini
Journal:
Theoretical Computer Science  TCS
, vol. 398, no. 13, pp. 95113, 2008
Provable Isomorphisms of Types
(
Citations: 47
)
Kim B. Bruce
,
Roberto Di Cosmo
,
Giuseppe Longo
Journal:
Mathematical Structures in Computer Science  MSCS
, vol. 2, no. 2, pp. 231247, 1992
Provable isomorphisms and domain equations in models of typed languages
(
Citations: 16
)
Kim B. Bruce
,
G Longo
Conference:
ACM Symposium on Theory of Computing  STOC
, pp. 263272, 1985
An extension of the basic functionality theory for the ?calculus
(
Citations: 140
)
M. Coppo
,
M. Dezaniciancaglini
Journal:
Notre Dame Journal of Formal Logic  NDJFL
, 1980