The relevance of semantic subtyping. (English) Zbl 1270.03043
van Bakel, Steffen (ed.), ITRS’02. Proceedings of the 2nd workshop on intersection types and related systems (FLoC satellite event), Copenhagen, Denmark, July 26, 2002. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 70, No. 1, 88-105 (2003).
Summary: We compare Meyer and Routley’s minimal relevant logic \(\mathbf B_{+}\) with the recent semantics-based approach to subtyping introduced by Frisch, Castagna and Benzaken in the definition of a type system with intersection and union. We show that – for the functional core of the system – such notion of subtyping, which is defined in purely set-theoretical terms, coincides with the relevant entailment of the logic \(\mathbf B_{+}\).
For the entire collection see [Zbl 1267.03007].
For the entire collection see [Zbl 1267.03007].
MSC:
| 03B47 | Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) |
References:
| [1] | Anderson, A. R.; Belnap, N. D.; Dunn, J. M., Entailment 2 (1992), Princeton · Zbl 0921.03025 |
| [2] | S. van Bakel, M. Dezani-Ciancaglini, U. deʼn Liguoro, and Y. Motohama. A Minimal Relevant Logic and the Callbyvalue Lambda Calculus, Technical Report TRARP05-2000, The Australian National University, 2000.; S. van Bakel, M. Dezani-Ciancaglini, U. deʼn Liguoro, and Y. Motohama. A Minimal Relevant Logic and the Callbyvalue Lambda Calculus, Technical Report TRARP05-2000, The Australian National University, 2000. |
| [3] | Barbanera, F.; Dezani-Ciancaglini, M., Intersection and Union Types, (TACS’01, Lecture Notes in Computer Science 526 (1991), Springer-Verlag: Springer-Verlag Berlin), 651-674 · Zbl 1493.68080 |
| [4] | Barbanera, F.; Dezani-Ciancaglini, M.; de’ Liguoro, U., Intersection and Union Types: Syntax and Semantics, Information and Computation, 119, 2, 202-230 (1995) · Zbl 0832.68065 |
| [5] | Barendregt, H.; Coppo, M.; Dezani-Ciancaglini, M., A Filter Lambda Model and the Completeness of Type Assignment, Journal of Symbolic Logic, 48, 4, 931-940 (1983) · Zbl 0545.03004 |
| [6] | Capitani, B.; Loreti, M.; Venneri, B., Hyperformulae, Parallel Deductions and Intersection Types, (BOTH ’01, Electronic Notes in Theoretical Computer Science, volume 50 (2001), Elsevier Science Publishers) · Zbl 1261.03072 |
| [7] | Coppo, M.; Dezani-Ciancaglini, M.; Honsell, F.; Longo, G., Extended Type Structures and Filter Lambda Models, (Logic Colloquium ’82 (1984), North Holland: North Holland Amsterdam), 241-262 · Zbl 0558.03007 |
| [8] | Dezani-Ciancaglini, M.; Ghilezan, S.; Venneri, B., The “Relevance” of Intersection and Union Types, Notre Dame Journal of Formal Logic, 38, 2, 246-269 (1997) · Zbl 0918.03008 |
| [9] | M. Dezani-Ciancaglini, R. K. Meyer, and Y. Motohama. The Semantics of Entailment Omega. Technical Report TRARP032000, The Australian National University, 2000.; M. Dezani-Ciancaglini, R. K. Meyer, and Y. Motohama. The Semantics of Entailment Omega. Technical Report TRARP032000, The Australian National University, 2000. · Zbl 1042.03019 |
| [10] | Hindley, J. R., Curryʼns Type-rules are Complete with Respect to F-semantics too, Theoretical Computer Science, 22, 127-133 (1983) · Zbl 0512.03010 |
| [11] | A. Frisch, G. Castagna, and V. Benzaken. Semantic Subtyping. In 17th IEEE Symposium on Logic in Computer Science; A. Frisch, G. Castagna, and V. Benzaken. Semantic Subtyping. In 17th IEEE Symposium on Logic in Computer Science · Zbl 1325.68136 |
| [12] | Mitchell, J., Polymorphic Type Inference and Containment, Information and Computation, 76, 211-249 (1988) · Zbl 0656.68023 |
| [13] | Routley, R.; Meyer, R. K., The Semantics of Entailment III, Journal of Philosophical Logic, 1, 192-208 (1972) · Zbl 0317.02019 |
| [14] | Venneri, B., Intersection Types as Logical Formulae, Journal of Logic and Computation, 4, 2, 109-124 (1994) · Zbl 0798.03013 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
