We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: On sets of terms with a given intersection type

Abstract: Working in a variant of the intersection type assignment system of Coppo, Dezani-Ciancaglini and Venneri [1981], we prove several facts about sets of terms having a given intersection type. One of our results is that every strongly normalizing term M admits a *uniqueness typing*, which is a pair $(\Gamma,A)$ such that
1) $\Gamma \vdash M : A$
2) $\Gamma \vdash N : A \Longrightarrow M =_{\beta\eta} N$
We also discuss several presentations of intersection type algebras, and the corresponding choices of type assignment rules.
In the second part of the paper, we prove that the set of closed terms having a given intersection type is separable, and, if infinite, forms an adequate numeral system.
Subjects: Logic in Computer Science (cs.LO)
MSC classes: 03B38
ACM classes: F.4.1
Cite as: arXiv:1809.08169 [cs.LO]
  (or arXiv:1809.08169v5 [cs.LO] for this version)

Submission history

From: Richard Statman [view email]
[v1] Wed, 19 Sep 2018 13:44:13 GMT (16kb)
[v2] Sun, 9 May 2021 00:01:41 GMT (21kb)
[v3] Thu, 9 Sep 2021 08:42:11 GMT (38kb)
[v4] Tue, 14 Sep 2021 01:28:12 GMT (38kb)
[v5] Tue, 1 Mar 2022 00:39:29 GMT (40kb)

Link back to: arXiv, form interface, contact.