Document Open Access Logo

Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper)

Author Simona Ronchi Della Rocca

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2016.2.pdf
  • Filesize: 341 kB
  • 7 pages

Document Identifiers

Author Details

Simona Ronchi Della Rocca

Cite AsGet BibTex

Simona Ronchi Della Rocca. Intersection Types and Denotational Semantics: An Extended Abstract (Invited Paper). In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 2:1-2:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.TYPES.2016.2

Abstract

This is a short survey of the use of intersection types for reasoning in a finitary way about terms interpretations in various models of lambda-calculus.
Keywords
  • Lambda-calculus
  • Lambda-models
  • Intersection types

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Fabio Alessi, Mariangiola Dezani-Ciancaglini, and Furio Honsell. A complete characterization of complete intersection-type preorders. ACM Transactions on Computational Logic, 4(1):120-147, jan 2003. Google Scholar
  2. Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in logic and the foundation of mathematics. North-Holland, revised edition, 1984. Google Scholar
  3. Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. The Journal of Symbolic Logic, 48(4):931-940, dec 1983. Google Scholar
  4. Gérard Berry. Stable models of typed λ-calculi. In Giorgio Ausiello and Corrado Böhm, editors, Fifth International Colloquium on Automata, Languages and Programming - - ICALP'78, Udine, Italy, July 17-21, 1978, volume 62 of Lecture Notes in Computer Science, pages 72-89. Springer-Verlag, 1978. Google Scholar
  5. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In CSL'07, volume 4646 of Lecture Notes in Computer Science, pages 298-312. Springer, 2007. Google Scholar
  6. Mario Coppo and Mariangiola Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic, 21(4):685-693, oct 1980. Google Scholar
  7. Mario Coppo, Mariangiola Dezani-Ciancaglini, Furio Honsell, and Giuseppe Longo. Extended type structure and filter lambda models. In Logic Colloquim'82, pages 241-262, 1984. Google Scholar
  8. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Maddalena Zacchi. Type theories, normal forms, and D_∞-lambda-models. Information and Computation, 72(2):85-116, 1987. Google Scholar
  9. Daniel de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs/0905.4251, 2009. Available also as INRIA report RR 6638. URL: http://arxiv.org/abs/0905.4251.
  10. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1-102, 1987. Google Scholar
  11. Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, 1989. Google Scholar
  12. Furio Honsell and Simona Ronchi della Rocca. Reasoning about interpretation in qualitative lambda-models. In IFIP 2.2, pages 505-521, 1990. Google Scholar
  13. Furio Honsell and Simona Ronchi Della Rocca. An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49-75, aug 1992. Google Scholar
  14. Giulio Manzonetto and Domenico Ruoppolo. Relational graph models, Taylor expansion and extensionality. Electronic Notes in Theoretical Computer Science, 308:245-272, 2014. Google Scholar
  15. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Logical semantics for stability. In MFPS'09, volume 249 of Electronic Notes in Theoretical Computer Science, pages 429-449, 2009. Google Scholar
  16. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Essential and relational models. Mathematical Structures in Computer Science, FirstView:1-25, 9 2015. URL: http://dx.doi.org/10.1017/S0960129515000316.
  17. D. M. R. Park. The Y-combinator in scott’s lambda-calculus models. Research Report CS-RR-013, Department of Computer Science, University of Warwick, Coventry, UK, jun 1976. URL: http://www.dcs.warwick.ac.uk/pub/reports/rr/013.html.
  18. Simona Ronchi Della Rocca and Luca Paolini. The Parametric λ-Calculus: a Metamodel for Computation. Texts in Theoretical Computer Science: An EATCS Series. Springer-Verlag, 2004. Google Scholar
  19. Dana S. Scott. Data types as lattices. SIAM Journal of Computing, 5:522-587, sep 1976. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact