Published: 23rd April 2019 DOI: 10.4204/EPTCS.293 ISSN: 2075-2180

Proceedings Twelfth Workshop onDevelopments in Computational Models and Ninth Workshop on Intersection Types and Related Systems Oxford, UK, 8th July 2018

Edited by: Michele Pagani and Sandra Alves

 Preface Invited Presentation: Polyadic Approximations and Intersection Types Damiano Mazza Invited Presentation: Quantitative Types: From Foundations to Applications Delia Kesner 1 Invited Presentation: Intersection Types for Unboundedness Problems Paweł Parys 7 Natural Deduction and Normalization Proofs for the Intersection Type Discipline Federico Aschieri 29 A Syntactic Model of Mutation and Aliasing Paola Giannini, Marco Servetto and Elena Zucca 39 Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus Giulio Guerrieri 57 Intersection Subtyping with Constructors Olivier Laurent 73 A Category Theoretic Interpretation of Gandy's Principles for Mechanisms Joseph Razavi and Andrea Schalk 85

Preface

This volume contains a selection of papers presented at DCM 2018, the Twelfth International Workshop on Developments in Computational Models, and ITRS 2018, the Ninth Workshop on Intersection Types and Related Systems. The workshops took place on July 8, 2018, in Oxford, UK as satellite events of FLoC 2018 in association with the ACM/IEEE Symposium on Logic in Computer Science (LICS) and the International Conference on Formal Structures for Computation and Deduction (FSCD).

The DCM workshop aims to bring together researchers who are currently developing new computational models or new features for traditional computational models, in order to foster their interaction, to provide a forum for presenting new ideas and work in progress, and to enable newcomers to learn about current activities in this area. Topics of interest include all abstract models of computation and their applications to the development of programming languages and systems.

The aim of the ITRS 2018 workshop series is to bring together researchers working on both the theory and practical applications of systems based on intersection types and related approaches. Over the last twenty years the scope of the research on intersection types and related systems has broadened in many directions, ranging from restricted (and more manageable) forms, to applications in areas such program analysis and higher-order model checking, to more recent research focusing on a behavioural/intensional approach to types.

The programs of the two workshops included two joint DCM/ITRS invited talks by Delia Kesner and Damiano Mazza, and two additional invited talks by Ugo Dal Lago (DCM invited speaker) and Pawel Parys (ITRS invited speaker). In addition, there were six contributed papers presented at DCM and six contributed papers presented at ITRS. For this volume containing the final proceedings, the program committees of DCM and ITRS 2018 select a total of five contributed papers: two contributed papers from DCM (A Category Theoretic Interpretation of Gandy's Principles for Mechanisms by Joseph Razavi and Andrea Schalk, and A syntactic model of mutation and aliasing by Paola Giannini, Marco Servetto and Elena Zucca) and three contributed papers from ITRS (Natural Deduction and Normalization Proofs for the Intersection Type Discipline, by Federico Aschieri, Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus, by Giulio Guerrieri, and Intersection Subtyping with Constructors by Olivier Laurent).

The volume also contains also an invited paper from ITRS (Intersection Types for Unboundedness Problems by Pawel Parys) and the abstracts from the two DCM/ITRS joint invited talks (Quantitative Types: From Foundations to Applications by Delia Kesner and Polyadic Approximations and Intersection Types by Damiano Mazza).

We wish to thank the organisers of FLoC 2018 for their support. We are indebted to the program committee members and the external referees for their careful and efficient work in the reviewing process. Finally we are grateful to the authors for submitting their work and the invited speakers for sharing their knowledge. A special thanks to EPTCS for supporting the publication of this joint issue.

Sandra Alves and Michele Pagani
DCM and ITRS Program Chairs

Program Committee of ITRS 2018:

Ugo de' Liguoro (Università di Torino, Italy), Boris Duedder (University of Copenhagen, Denmark), Joshua Dunfield (Queen's University, Canada), Charles Grellois (Université Aix-Marseille, France), Naoki Kobayashi (University of Tokyo, Japan), Michele Pagani - chair (IRIF, Université Paris Diderot, France), Joe Wells (Heriot-Watt University, Scotland).

Program Committee of DCM 2018:

Sandra Alves - chair (University of Porto, Portugal), Sabine Broda (University of Porto, Portugal), Nachum Dershowitz (University of Tel Aviv, Israel), Mariangiola Dezani (Università di Torino, Italy), Alessandra Di Pierro (Università di Verona, Italy), Maribel Fernández (King's College London, UK), Russ Harmer (ENS Lyon, France), Edward Hermann Haeusler (PUC-Rio, Brasil), Luigi Liquori (INRIA Sophia, France), Elvira Mayordomo (University of Zaragoza, Spain), Simon Perdrix (LORIA-Nancy, France), Jamie Vicary (University of Oxford, UK).

Additional Reviewers:

Pablo Arrighi (Université Aix-Marseille, France), Martin Berger (University of Sussex, UK), Jan Bessai (University of Dortmund, Germany), Mariangiola Dezani (Università di Torino, Italy), Delia Kesner (IRIF, Université Paris Diderot, France), Julien Lange (University of Kent, UK), Victor Lanvin (IRIF, Université Paris Diderot, France), Takeshi Tsukada (University of Tokyo, Japan), Pierre Vial (IRIF, Université Paris Diderot, France).

Polyadic Approximations and Intersection Types

In his paper introducing linear logic, Girard briefly mentioned how full linear logic could be seen, in an informal sense, as the limit of its purely linear fragment. Several ways of expanding and formalizing this idea have been developed through the years, including what I call polyadic approximations. In this talk, I will show how these are deeply related to intersection type systems, via a general construction that is sufficiently broad to allow recovering every well known intersection type system and their normalization properties, as well as introducing new type systems in wildly disparate contexts, with applications ranging from deadlock-freedom in the pi-calculus to a type-theoretic proof of the Cook-Levin theorem.

(Part of this work was developed jointly with Luc Pellissier and Pierre Vial).

Quantitative Types: From Foundations to Applications

Delia Kesner (IRIF, CNRS and Université Paris Diderot)

Among the well-known techniques used to reason about relevant aspects of programs we find the large world of type systems, whose development was consolidated by the famous Curry-Howard correspondence, providing a robust correspondence between proofs (in some logic) and well-typed programs (in some programming language). This discovery has already provided important conceptual foundations for typed programming languages like OCaml and proof assistants like Coq.

The Curry-Howard correspondence has already contributed to our understanding of many aspects of programming languages by establishing a rich connection with intuitionistic and classical logic, however, there are still some quantitative crucial aspects of computation that need to be logically understood, like the use of time and space resources.

In this talk we give a theoretical understanding of the use of resources in programming languages by means of quantitative type systems. We introduce different alternatives, suitable for a wide range of powerful models of computation, such as for example pattern matching, control operators and infinitary computations.

From qualitative type systems ... Several notions of type assignment systems for $\lambda$-calculus have been defined in these last years. The most natural and oldest among them is given by the simple type assignment system, which has been further extended with polymorphic functions, i.e. functions that can be applied to various kinds of arguments, even of incomparable type. The resulting system is used as the core of different typing systems used nowadays in programming languages like ML and OCaml.

Even if polymorphic types are powerful and convenient in programming practice, they have several drawbacks. For example, it is not possible to assign a type to a term of the form $\lambda x. xx$, which can be understood as a meaningful program specified by a terminating term. Intersection types, pioneered by Coppo and Dezani [11, 12], introduce a new constructor for types, written $\cap$, which allows to type the term $\lambda x. xx$ with a type of the form $( (\sigma \rightarrow \sigma)\cap\sigma ) \rightarrow \sigma$. The intuition behind this is that a term $t$ has type $\tau_1 \cap \tau_2$ if $t$ has both types $\tau_1$ and $\tau_2$. The symbol $\cap$ needs to be understood as a mathematical intersection, so in principle, intersection type theory was developed by using idempotent ($\sigma \cap \sigma = \sigma$), commutative $(\sigma \cap \tau = \tau \cap \sigma)$, and associative $((\sigma \cap \tau) \cap \delta = \sigma \cap (\tau \cap \delta))$ laws.

Intersection types are so powerful that they can be seen as a behavioural tool to reason about operational and semantical properties of different languages. They can be used in particular to characterise different properties of the $\lambda$-calculus. For example, a term/program $t$ is strongly normalising/terminating if and only if $t$ can be assigned an intersection type in an appropriate intersection type assignment system. Similarly, intersection types are able to describe and analyse models of $\lambda$-calculus [2], characterise solvability [31], head normalisation [31], linear-head normalisation [23], and weak-normalisation [31, 29] among other properties.

... to quantitative type systems This technology turns out to be a powerful tool to reason about qualitative properties of programs, but not for quantitative ones. Indeed, we know that a term is typable if and only if it verifies some property, but we cannot count the number of resources which are necessary for this term in order to verify the property. Here is where non-idempotent types, pioneered by [19, 25], come into play, making a clear distinction between $\sigma \cap \sigma$ and $\sigma$, because using the resource $\sigma$ twice or once is not the same. This change of point of view can be related to the essential spirit of Linear Logic [20], which removes the contraction and weakening structural rules in order to provide an explicit control of the use of logical resources, i.e. to give a full account of the number of times that propositions are used to derive conclusions. Typing of Church numerals provide a clear example of the peculiarity of non idempotent intersection type systems, with respect to the usual, idempotent, ones. Let $\underline n=\lambda x\lambda y.\underbrace{x(x(\ldots(x}_{n\times}y)\ldots))$ be the $n$-th Church numeral, and let us consider the typing of $\underline 2=\lambda x\lambda y.x(xy)$ in the idempotent and non-idempotent systems respectively. The idempotent type system allows to type {\em all} Church numerals with the same type $( (\alpha \rightarrow\alpha)\rightarrow \alpha) \rightarrow\alpha$, here assigned also to the Church numeral $\underline 2$. However, the non-idempotent type system would use a quantitative type information like $(( (\alpha \rightarrow\alpha ) \cap (\alpha \rightarrow\alpha )) \rightarrow \alpha) \rightarrow\alpha$, in order to enforce the fact that the variable $x$ is used twice in the Church numeral $\underline 2$. Similarly, the Church numeral $\underline 3$ will receive another type of the form $(( (\alpha \rightarrow\alpha ) \cap (\alpha \rightarrow\alpha )\cap (\alpha \rightarrow\alpha )) \rightarrow \alpha) \rightarrow\alpha$, etc. Non-idempotent intersection types have been used to give denotational semantics of linear logic [20]. They give rise to different resource aware languages, pioneered by Kfoury [25] and Boudol, Curien and Lavatelli [6]. Relational models of $\lambda$-calculi based on non-idempotent types have been investigated in [9, 16]. D. de Carvalho [9] used non-idempotent intersection type systems to obtain exact bounds on evaluation lengths for the call-by-name lambda-calculus. This approach is also applied to linear logic proof-nets [10]. Non-idempotency is used to reason about the longest reduction sequence of strongly normalising terms in both the call-by-name lambda-calculus [3,13, 4] and in different (call-by-name) lambda-calculi with explicit substitutions [4, 23]. Extensions to classical logic also consider non-idempotent union types [24]. The case of call-by-value is addressed in [16, 8], while call-by-push value is studied in [17, 18] and call-by-need in [21, 22, 1]. Non-idempotent types also appear in linearisation of the lambda-calculus [25], type inference [26, 32], different characterisations of solvability [34] and verification of higher-order programs [33]. While the inhabitation problem for intersection types is known to be undecidable in the idempotent case [35], decidability was recently proved [7] through a sound and complete algorithm in the non-idempotent case. This list is not exhaustive.

In this talk we discuss quantitative properties that can be observed and formally characterised on a broad range of programming language paradigms.

On one side, we want to go beyond toy examples, like the $\lambda$-calculus, to focus on the challenges posed by the advanced features that are found in modern higher-order programming languages, proof assistants and theorem provers such as pattern matching, infinite data, and/or control operators.

On the other side, we do not want to restrict our study to a particular programming language, so that we can cover different reduction strategies used to implement these higher-order programming languages, such as for example call-by-value (OCaml), call-by-need (Haskell), standard strategies (call-by-name languages).

Interesting connections exist, and would need to be understood better, between the use of quantitative techniques in program analysis and the emerging quantitative approach in well-established areas of computer science such as verification [27, 33], logic [28, 20] and automata [5, 15].

References

1. Beniamino Accattoli, Giulio Guerrieri & Maico Leberle (2018): Types by Need. In: Prooceedings of the 28th European Symposium on Programming, ESOP 2019, Lecture Notes in Computer Science 11423. Springer-Verlag, pp. 410–439. Available at https://doi.org/10.1007/978-3-030-17184-1\_15.
2. Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini (1983): A filter lambda model and the completeness of type assignment. Bulletin of Symbolic Logic 48, pp. 931–940. Available at https://doi.org/10.2307/2273659.
3. Alexis Bernadet & Stéphane Lengrand (2011): Complexity of strongly normalising λ-terms via non-idempotent intersection types. In: Martin Hofmann: Foundations of Software Science and Computation Structures (FOSSACS), Lecture Notes in Computer Science 6604. Springer-Verlag, pp. 88–107. Available at https://doi.org/10.1007/978-3-642-19805-2_7.
4. Alexis Bernadet & Stéphane Lengrand (2013): Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9(4). Available at http://dx.doi.org/10.2168/LMCS-9(4:3)2013.
5. Roderick Bloem, Krishnendu Chatterjee, Thomas A. Henzinger & Barbara Jobstmann (2009): Better Quality in Synthesis through Quantitative Objectives. In: Ahmed Bouajjani & Oded Maler: Computer Aided Verification, 21st International Conference (CAV), Lecture Notes in Computer Science 5643. Springer-Verlag, pp. 140–156. Available at https://doi.org/10.1007/978-3-642-02658-4_14.
6. Gérard Boudol, Pierre-Louis Curien & Carolina Lavatelli (1999): A semantics for lambda calculi with resources. Mathematical Structures in Computer Science 9(4), pp. 437–482. Available at http://dx.doi.org/10.1017/S0960129599002893.
7. Antonio Bucciarelli, Delia Kesner & Simona Ronchi Della Rocca (2014): The Inhabitation Problem for Non-Idempotent Intersection Types. In: editor = "Díaz",, pp. 341–354. Available at https://doi.org/10.1007/978-3-662-44602-7_26.
8. Alberto Carraro & Giulio Guerrieri (2014): A Semantical and Operational Account of Call-by-Value Solvability. In: Anca Muscholl: Foundations of Software Science and Computation Structures - 17th International Conference (FOSSACS), Lecture Notes in Computer Science 8412. Springer, pp. 103–118. Available at https://doi.org/10.1007/978-3-642-54830-7_7.
9. Daniel de Carvalho (2007): Sémantiques de la logique linéaire et temps de calcul. These de doctorat. Université Aix-Marseille II. Available at https://books.google.pt/books?id=erhUPgAACAAJ.
10. Daniel de Carvalho & Lorenzo Tortora de Falco (2016): A semantic account of strong normalization in linear logic. Inf. Comput. 248, pp. 104–129. Available at https://doi.org/10.1016/j.ic.2015.12.010.
11. Mario Coppo & Mariangiola Dezani-Ciancaglini (1978): A new type assignment for lambda-terms. Archive for Mathematical Logic 19, pp. 139–156. Available at https://doi.org/10.1007/BF02011875.
12. Mario Coppo & Mariangiola Dezani-Ciancaglini (1980): An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 4, pp. 685–693. Available at https://doi.org/10.1305/ndjfl/1093883253.
13. Erika De Benedetti & Simona Ronchi Della Rocca (2013): Bounding normalization time through intersection types. In: Luca Paolini: Proceedings of Sixth Workshop on Intersection Types and Related Systems (ITRS), Electronic Proceedings in Theoretical Computer Science 121. Cornell University Library, pp. 48–57. Available at http://dx.doi.org/10.4204/EPTCS.121.4.
14. Josep Díaz, Ivan Lanese & Davide Sangiorgi (2014): Proceedings of the 8th International Conference on Theoretical Computer Science (TCS). Lecture Notes in Computer Science 8705. Springer-Verlag. Available at http://dx.doi.org/10.1007/978-3-662-44602-7.
15. Manfred Droste & Paul Gastin (2007): . Theoretical Computer Science 380(1-2), pp. 69–86. Available at https://doi.org/10.1007/978-3-642-01492-5_5.
16. Thomas Ehrhard (2012): Collapsing non-idempotent intersection types. In: Patrick Cégielski & Arnaud Durand: Proceedings of 26th EACSL Conference on Computer Science Logic (CSL), LIPIcs 16. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 259–273. Available at http://dx.doi.org/10.4230/LIPIcs.CSL.2012.259.
17. Thomas Ehrhard (2016): Call-By-Push-Value from a Linear Logic Point of View. In: Peter Thiemann: 25th European European Symposium on Programming 9632, Lecture Notes in Computer Science, pp. 202–228. Available at https://doi.org/10.1007/978-3-662-49498-1_9.
18. Thomas Ehrhard & Giulio Guerrieri (2016): The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In: James Cheney & Germán Vidal: Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming, Edinburgh, United Kingdom, September 5-7, 2016. ACM, pp. 174–187. Available at https://doi.org/10.1145/2967973.2968608.
19. Philippa Gardner (1994): Discovering Needed Reductions Using Type Theory. In: Masami Hagiya & John C. Mitchell: Theoretical Aspects of Computer Software, International Conference TACS '94, Sendai, Japan, April 19-22, 1994, Proceedings, Lecture Notes in Computer Science 789. Springer, pp. 555–574. Available at https://doi.org/10.1007/3-540-57887-0_115.
20. Jean-Yves Girard (1987): Linear Logic. Theoretical Computer Science 50, pp. 1–102. Available at http://dx.doi.org/10.1016/0304-3975(87)90045-4.
21. Delia Kesner (2016): Reasoning About Call-by-need by Means of Types. In: Bart Jacobs & Christof Löding: Foundations of Software Science and Computation Structures - 19th International Conference, FOSSACS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, Lecture Notes in Computer Science 9634. Springer, pp. 424–441. Available at https://doi.org/10.1007/978-3-662-49630-5_25.
22. Delia Kesner, Alejandro Ríos & Andrés Viso (2018): Call-by-Need, Neededness and All That. In: Christel Baier & Ugo Dal Lago: Foundations of Software Science and Computation Structures - 21st International Conference, FOSSACS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Lecture Notes in Computer Science 10803. Springer, pp. 241–257. Available at https://doi.org/10.1007/978-3-319-89366-2_13.
23. Delia Kesner & Daniel Ventura (2014): Quantitative Types for the Linear Substitution Calculus. In: editor = "Díaz",, pp. 296–310. Available at https://doi.org/10.1007/978-3-662-44602-7_23.
24. Delia Kesner & Pierre Vial (2017): Types as Resources for Classical Natural Deduction. In: Dale Miller: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD), LIPIcs 84. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 1–17. Available at https://doi.org/10.4230/LIPIcs.FSCD.2017.24.
25. Assaf Kfoury (2000): A Linearization of the Lambda-Calculus and Consequences. J. Log. Comput. 10(3), pp. 411–436. Available at https://doi.org/10.1093/logcom/10.3.411.
26. Assaf Kfoury & Joe Wells (2004): Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311(1-3), pp. 1–70. Available at http://dx.doi.org/10.1016/j.tcs.2003.10.032.
27. Naoki Kobayashi (2013): Pumping by Typing. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, pp. 398–407. Available at http://dx.doi.org/10.1109/LICS.2013.46.
28. Stephan Kreutzer & Cristian Riveros (2013): Quantitative Monadic Second-Order Logic. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, pp. 113–122. Available at https://doi.org/10.1109/LICS.2013.16.
29. Jean-Louis Krivine (1993): Lambda-calculus, types and models. Ellis Horwood. Available at http://dx.doi.org/10.1016/S0167-6423(98)90004-1.
30. Betti Venneri Mario Coppo, Mariangiola Dezani-Ciancaglini (1981): Functional Characters of Solvable Terms. Mathematical Logic Quarterly 27, pp. 45–58. Available at https://doi.org/10.1002/malq.19810270205.
31. Peter Møller Neergaard & Harry G. Mairson (2004): Types, potency, and idempotency: why nonlinearity and amnesia make a type system work. In: Chris Okasaki & Kathleen Fisher: Proceedings of the Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP). ACM Press, pp. 138–149. Available at http://doi.acm.org/10.1145/1016848.1016871.
32. Luke Ong & Steven J. Ramsay (2011): Verifying Higher-Order Functional Programs with Pattern Matching Algebraic Data Types. In: Thomas Ball & Mooly Sagiv: Proceedings of the 38th Annual ACM Symposium on Principles of Programming Languages (POPL). ACM Press, pp. 587–598. Available at http://doi.acm.org/10.1145/1925844.1926453.
33. Michele Pagani & Simona Ronchi Della Rocca (2010): Solvability in Resource Lambda-Calculus. In: Luke Ong: Foundations of Software Science and Computation Structures, Lecture Notes in Computer Science 6014. Springer-Verlag, pp. 358–373. Available at https://doi.org/10.1007/978-3-642-12032-9_25.
34. Pawel Urzyczyn (1999): The Emptiness Problem for Intersection Types. Journal of Symbolic Logic 64(3), pp. 1195–1215. Available at http://doi.org/10.2307/2586625.