Damiano Mazza
Skip Abstract Section
Skip Supplemental Material SectionAbstract
Starting from an exact correspondence between linear approximations and non-idempotent intersection types, we develop a general framework for building systems of intersection types characterizing normalization properties. We show how this construction, which uses in a fundamental way Melliès and Zeilberger's ``type systems as functors'' viewpoint, allows us to recover equivalent versions of every well known intersection type system (including Coppo and Dezani's original system, as well as its non-idempotent variants independently introduced by Gardner and de Carvalho). We also show how new systems of intersection types may be built almost automatically in this way.
Supplemental Material
- Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In Proceedings of RTA. 6–21.Google Scholar
- Henk P. Barendregt. 1984. The Lambda Calculus, Its Syntax and Semantics. Elsevier.Google Scholar
- Alexis Bernadet and Stéphane Lengrand. 2013. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9, 4 (2013). Google ScholarCross Ref
- Gérard Boudol. 1993. The Lambda-Calculus with Multiplicities (Abstract). In Proceedings of CONCUR. 1–6. Google ScholarCross Ref
- Flavien Breuvart and Ugo Dal Lago. 2016. ntersection Types and Probabilistic Lambda Calculi. In Presented at ITRS.Google Scholar
- Antonio Bucciarelli, Delia Kesner, and Simona Ronchi Della Rocca. 2014. The Inhabitation Problem for Non-idempotent Intersection Types. In Proceedings of IFIP TCS. 341–354. Google ScholarCross Ref
- Antonio Bucciarelli, Adolfo Piperno, and Ivano Salvo. 2003. Intersection Types and lambda-Definability. Mathematical Structures in Computer Science 13, 1 (2003), 15–53. Google ScholarDigital Library
- Sébastien Carlier, Jeff Polakow, J. B. Wells, and A. J. Kfoury. 2004. System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types. In Proceedings of ESOP 2004. 294–309. Google ScholarCross Ref
- François Conduché. 1972. Au sujet de l’existence d’adjoints à droite aux foncteurs ‘image reciproque’ dans la catégorie des catégories. C. R. Acad. Sci. Paris Série A, 275 (1972), 891–894.Google Scholar
- Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 21, 4 (1980), 685–693. Google ScholarCross Ref
- Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Math. Log. Q. 27, 2-6 (1981), 45–58.Google ScholarCross Ref
- Pierre-Louis Curien and Jovana Obradovic. 2017. Categorified cyclic operads. Technical Report 1706.06788 [math.CT]. ArXiv.Google Scholar
- Daniel de Carvalho. 2009. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs/0905.4251 (2009).Google Scholar
- Thomas Ehrhard and Olivier Laurent. 2010. Interpreting a Finitary Pi-Calculus in Differential Interaction Nets. Information and Computation 208, 6 (2010), 606–633. Google ScholarDigital Library
- Thomas Ehrhard and Laurent Regnier. 2008. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci. 403, 2–3 (2008), 347–372.Google ScholarDigital Library
- Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding. In Proceedings of LICS. 193–202. Google ScholarCross Ref
- Philippa Gardner. 1994. Discovering Needed Reductions Using Type Theory. In Proceedings of TACS. 555–574. Google ScholarCross Ref
- Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci. 50, 1 (1987), 1–102. Google ScholarDigital Library
- Charles Grellois and Paul-André Melliès. 2015. Relational Semantics of Linear Logic and Higher-order Model Checking. In Proceedings of CSL. 260–276.Google Scholar
- Barney P. Hilken. 1996. Towards a Proof Theory of Rewriting: The Simply Typed 2lambda-Calculus. Theor. Comput. Sci. 170, 1-2 (1996), 407–444.Google ScholarCross Ref
- Tom Hirschowitz. 2013. Cartesian closed 2-categories and permutation equivalence in higher-order rewriting. Logical Methods in Computer Science 9, 3 (2013). Google ScholarCross Ref
- Martin Hyland. 2017. Classical lambda calculus in modern dress. Math. Struct. Comput. Sci. 27, 5 (2017), 762–781. Google ScholarCross Ref
- Delia Kesner and Pierre Vial. 2017. Types as Resources for Classical Natural Deduction. Proceedings of FSCD (to appear) (2017).Google Scholar
- Assaf J. Kfoury. 2000. A linearization of the Lambda-calculus and consequences. J. Log. Comput. 10, 3 (2000), 411–436. Google ScholarCross Ref
- Naoki Kobayashi and C.-H. Luke Ong. 2009. A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. In Proceedings of LICS. 179–188. Google ScholarDigital Library
- Jean-Louis Krivine. 1993. Lambda Calculus, Types and Models. Ellis Horwood.Google Scholar
- Olivier Laurent. 2003. Polarized proof-nets and lambda-mu-calculus. Theor. Comput. Sci. 290, 1 (2003), 161–188. Google ScholarDigital Library
- Olivier Laurent. 2004. On the denotational semantics of the untyped lambda-mu calculus. (2004). Unpublished note.Google Scholar
- Tom Leinster. 2004. Higher Operads, Higher Categories. Cambridge University Press. Google ScholarCross Ref
- Damiano Mazza. 2012. An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus. In Proceedings of LICS. 471–480. Google ScholarDigital Library
- Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. 2009. An Explicit Formula for the Free Exponential Modality of Linear Logic. In Proc. ICALP 2009. 247–260. Google ScholarDigital Library
- Paul-André Melliès and Noam Zeilberger. 2015. Functors are Type Refinement Systems. In Proceedings of POPL. 3–16. Google ScholarDigital Library
- Peter Møller Neergaard and Harry G. Mairson. 2004. Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In Proceedings of ICFP. 138–149. Google ScholarDigital Library
- Susan Niefield. 2004. Change of Base for Relational Variable Sets. Theory Appl. Categ. 12, 7 (2004), 248–261.Google Scholar
- Michel Parigot. 1992. λµ-Calculus: An algorithmic interpretation of classical natural deduction. Springer Berlin Heidelberg, Berlin, Heidelberg, 190–201. Google ScholarCross Ref
- Luc Pellissier. 2017. Réductions et approximations linéaires. PhD. Thesis. Université Paris 13.Google Scholar
- Laurent Regnier. 1992. Lambda-calcul et réseaux. PhD Thesis. Université Paris 7.Google Scholar
- R. A. G. Seely. 1987. Modelling Computations: A 2-Categorical Framework. In Proceedings of LICS. 65–71.Google Scholar
- Terese. 2003. Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science, Vol. 55. Cambridge University Press.Google Scholar
- Steffen van Bakel. 1995. Intersection Type Assignment Systems. Theor. Comput. Sci. 151, 2 (1995), 385–435. Google ScholarDigital Library
- Pierre Vial. 2017. Infinitary intersection types as sequences: A new answer to Klop’s problem. In Proceedings of LICS. 1–12. Google ScholarCross Ref
- Christopher P. Wadsworth. 1971. Semantics and Pragmatics of the Lambda Calculus. PhD Thesis. University of Oxford.Google Scholar
Index Terms
- Polyadic approximations, fibrations and intersection types
Recommendations
Gradual typing with union and intersection types
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
Disjoint intersection types
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingDunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression ...
Disjoint intersection types
ICFP '16Dunfield showed that a simply typed core calculus with intersection types and a merge operator is able to capture various programming language features. While his calculus is type-safe, it is not coherent: different derivations for the same expression ...
Comments