Hostname: page-component-8448b6f56d-tj2md Total loading time: 0 Render date: 2024-04-20T00:07:16.685Z Has data issue: false hasContentIssue false
  • English
  • Français

Essential and relational models†

Published online by Cambridge University Press:  23 July 2015

LUCA PAOLINI ,
MAURO PICCOLO  and
SIMONA RONCHI DELLA ROCCA
LUCA PAOLINI
Affiliation:
Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera 185, 10149 Torino, Italy Emails: paolini@di.unito.it, piccolo@di.unito.it
MAURO PICCOLO
Affiliation:
Dipartimento di Informatica Scienze ed Ingegneria, Università di Bologna, Mura Anteo Zamboni 7, Bologna, Italy Email: ronchi@di.unito.it
SIMONA RONCHI DELLA ROCCA
Affiliation:
Dipartimento di Informatica, Università degli Studi di Torino, Corso Svizzera 185, 10149 Torino, Italy Emails: paolini@di.unito.it, piccolo@di.unito.it
Get access Rights & Permissions [Opens in a new window]

Abstract

Intersection type assignment systems can be used as a general framework for building logical models of λ-calculus that allow to reason about the denotation of terms in a finitary way. We define essential models (a new class of logical models) through a parametric type assignment system using non-idempotent intersection types. Under an interpretation of terms based on typings instead than the usual one based on types, every suitable instance of the parameters induces a λ-model, whose theory is sensible. We prove that this type assignment system provides a logical description of a family of λ-models arising from a category of sets and relations.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Special Issue 5: Computing with Lambda-terms. A Special Issue Dedicated to Corrado Böhm for his 90th Birthday , June 2017 , pp. 626 - 650
Copyright
Copyright © Cambridge University Press 2015 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

‡

Dedicated to Corrado Böhm for his 90th birthdays.

References

Abramsky, S. (1991). Domain theory in logical form. Annals of Pure and Applied Logic 51 (1–2) 1–77.CrossRefGoogle Scholar
Amadio, R. and Curien, P.-L. (1998). Domains and Lambda-Calculi, Cambridge Tracts in Theoretical Computer Science vol. 46, Cambridge University Press.CrossRefGoogle Scholar
Asperti, A. and Longo, G. (1991). Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist, The MIT Press.Google Scholar
Barendregt, H. (1984). The Lambda Calculus: Its Syntax and Semantics, Studies in logic and the foundation of mathematics vol. 103, North-Holland, revised edition.Google Scholar
Bernadet, A. and Lengrand, S. (2011a). Complexity of strongly normalising λ-terms via non-idempotent intersection types. In: FOSSACS'11. Springer Lecture Notes in Computer Science 6604 88–107.CrossRefGoogle Scholar
Bernadet, A. and Lengrand, S. (2011b). Filter models: Non-idempotent intersection types, orthogonality and polymorphism. In: CSL'11. Leibniz International Proceedings in Informatics (LIPIcs) vol. 12 51–66.Google Scholar
Bucciarelli, A., Ehrhard, T. and Manzonetto, G. (2007). Not enough points is enough. In: CSL'07. Springer Lecture Notes in Computer Science 4646 298–312.CrossRefGoogle Scholar
Bucciarelli, A., Kesner, D. and Ronchi Della Rocca, S. (2014). The inhabitation problem for non-idempotent intersection types. In: IFIP/TCS, Roma, 1–3 September 14. Springer Lecture Notes in Computer Science 8705 341–354.CrossRefGoogle Scholar
Carraro, A., Ehrhard, T. and Salibra, A. (2010). Exponentials with infinite multiplicities. In: Dawar, A. and Veith, H. (eds.) CSL'10. Springer Lecture Notes in Computer Science 6247 170–184.CrossRefGoogle Scholar
Coppo, M., Dezani-Ciancaglini, M., Honsell, F. and Longo, G. (1984). Extended type structure and filter lambda models. In: Logic Colloquim'82 241–262.Google Scholar
Coppo, M., Dezani-Ciancaglini, M. and Venneri, B. (1981). Functional characters of solvable terms. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 27 (1) 45–58.CrossRefGoogle Scholar
De Benedetti, E. and Ronchi Della Rocca, S. (2013). Bounding normalization time through intersection types. In: Paolini, L. (ed.) Proceedings of Sixth Workshop on Intersection Types and Related Systems (ITRS 2012). Electronic Notes in Theoretical Computer Science, Cornell University Library 48–57.Google Scholar
de Carvalho, D. (2009). Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251. Available also as INRIA report RR 6638.Google Scholar
Di Gianantonio, P., Honsell, F. and Lenisa, M. (2008). A type assignment system for game semantics. Theoretical Computer Science 398 150–169.CrossRefGoogle Scholar
Ehrhard, T. (2012). Collapsing non-idempotent intersection types. In: CSL'12. Leibniz International Proceedings in Informatics (LIPIcs) 16 259–273.Google Scholar
Hindley, J. R. and Longo, G. (1980). Lambda calculus models and extensionality. Zeitschrift für mathematische Logik und Grundlagen der Mathematik 26 289–310.CrossRefGoogle Scholar
Honsell, F. and Ronchi della Rocca, S. (1990). Reasoning about interpretation in qualitative lambda-models. In: IFIP 2.2 505–521.Google Scholar
Honsell, F. and Ronchi della Rocca, S. (1992). An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences 45 (1) 49–75.CrossRefGoogle Scholar
Kfoury, A. J. (2000). A linearization of the lambda-calculus and consequences. Journal of Logic and Computation 10 (3) 411–436.CrossRefGoogle Scholar
Kfoury, A. J. and Wells, J. B. (2004). Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311 (1–3) 1–70.CrossRefGoogle Scholar
Koymans, C. P. J. (1982). Models of the lambda calculus. Information and Computation 52 (3) 306–323.Google Scholar
Mairson, H. and Neergaard, P. M. (2004). Types, potency, and idempotency: Why nonlinearity and amnesia make a type system work. In: ICFP'04, 138–149.Google Scholar
Manzonetto, G. (2009). A general class of models of $\mathcal{H}$ *. In: MFCS'09. Springer Lecture Notes in Computer Science 5734 574–586.CrossRefGoogle Scholar
Manzonetto, G. (2012). What is a categorical model of the differential and the resource lambda-calculi? Mathematical Structures in Computer Science 22 (03) 451–520.CrossRefGoogle Scholar
Pagani, M. and Ronchi della Rocca, S. (2010a). Linearity, non-determinism and solvability. Fundamenta Informaticae 103 358–373.CrossRefGoogle Scholar
Pagani, M. and Ronchi della Rocca, S. (2010b). Solvability in resource lambda-calculus. In: FOSSACS'10. Lecture Notes in Computer Science 6014 358–373.CrossRefGoogle Scholar
Paolini, L., Piccolo, M. and Ronchi della Rocca, S. (2009). Logical semantics for stability. In: MFPS'09. Electronic Notes in Theoretical Computer Science 249 429–449.CrossRefGoogle Scholar
Ronchi della Rocca, S. and Paolini, L. (2004). The Parametric λ-Calculus: A Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series, Springer-Verlag.CrossRefGoogle Scholar
Selinger, P. (2002). The lambda calculus is algebraic. Journal of Functional Programming 12 (6) 549–566.CrossRefGoogle Scholar
Terui, K. (2006). Intersection types for computational complexity. In: Workshop on Implicit Computational Complexity (as part of GEOCAL'06), Marseille, February 2006.Google Scholar
Urzyczyn, P. (1999). The emptiness problem for intersection types. Journal of Symbolic Logic 64 (3) 1195–1215.CrossRefGoogle Scholar