ITRS 2020 - Abstracts
Ugo de’ Liguoro (ed.)
Turin, March 20201

Foreword
This volume contains the abstracts of the talks accepted for presentation at the10th International Conference on Intersection Types and Related Systems, ITRS
2020, in Turin, satellite event of TYPES 2020. Unfortunately, the circumstances
have been not favorable; being planned on the 6th March 2020 in Turin, theworkshop has not been held, because of the sanitary emergency caused by the
spreading of the SARS-CoV-2 virus infection.
The ITRS workshop series aims to bring together researchers working on
both the theory and practical applications of systems based on intersection
types and related approaches. Topics for submitted papers include, but are notlimited to:• Formal properties of systems with intersection types.
• Results for related systems, such as union types, refinement types, or
singleton types.
• Applications to lambda calculus, pi-calculus and similar systems.
• Applications for programming languages, program analysis, and program
verification.
• Applications for other areas, such as database query languages and program extraction from proofs.
• Related approaches using behavioural/intensional types and/or denotational semantics to characterize computational properties.
• Quantitative refinements of intersection types.
The abstracts contained in this document were accepted for presentation to
the Turin edition of the workshop, by the program committee formed by:
Ugo de’ Liguoro (Turin University)
Jeremy Siek (Indiana University Bloomington)
Andrej Dudenhefner (Saarland University)
Antonio Bucciarelli (Université Paris Diderot)
Daniel de Carvalho (Innopolis University)
Kazushige Terui (Kyoto University)
Silvia Ghilezan (University of Novi Sad)

Ugo de’ Liguoro
Turin, 1 March 20202

Contents
1 A. Dudenhefner, P. Urzyczyn: Kripke Semantics for Intersection Formulas
4
2 A. Bucciarelli, D. Kesner, A. Rı́os, A. Viso: Revisiting theBang Calculus
7
3 A. Bucciarelli, D. Kesner, S. Ronchi della Rocca: Observability
by Means of Typability and Inhabitation
12
4 L. Peyrot, D. Kesner: Quantitative Types for the Atomic λcalculus
15
5 C. Stolze, L. Liquori: A Type Checker for a Logical Frameworkwith Union and Intersection Types
17
6 U. Dal Lago, C. Faggian, S. Ronchi della Rocca: Intersection
Types and Positive Almost Sure Termination
21
7 M. Dezani-Ciancaglini, P. Giannini, B. Venneri: Exploiting thepower of intersection types in Java
23

3

Kripke Semantics for Intersection Formulas
Andrej Dudenhefner
Saarland University, Saarland Informatics Campus, Saarbrücken, Germany
dudenhefner@ps.uni-saarland.de

Paweł Urzyczyn
Institute of Informatics, University of Warsaw, Warsaw, Poland
urzy@mimuw.edu.pl

Introduction Intersection types are broadly used in type assignment systems but are seldom
understood as logical formulas. Exceptions include [4, 8], and the line of research on intersection
logic [5, 6, 3], initiated by S. Ronchi Della Rocca and L. Roversi. The underlying semantics
accompanying those efforts is proof-theoretical. However, if we think of intersection formulas as
independent of term-assignment, we naturally ask for mathematical semantics of formulas that
could be defined and investigated without any direct reference to λ-terms.
Here, we outline the first (to the authors’ knowledge) attempt to define a sound and complete
possible-world (Kripke) semantics for intersection logic. The approach develops from the ideaof proof-search, or type inhabitation algorithm, understood as a game.
Adaptation of previous methods [7] to intersection logic is difficult for two reasons. First, forproof construction one must consider parallel inhabitation problems, where a single proof has
to satisfy multiple constraints. This complicates proof syntax (we use matrices of formulas) andmodel definition. Second, intersection formulas may be non-uniform, e.g. p ∩ (q → p), exhibiting“functional” and “atomic” behavior. To accommodate both, our models must satisfy a global
condition of being “monotone”.
Formulas and matrices Formulas (ranged over by σ, τ, ρ) are Barendregt–Coppo–Dezani(BCD) intersection types [1], i.e. σ, τ ::= p | ω | σ → τ | σ ∩ τ , where atoms are ranged over by p, q.
The preorder ≤ is intersection type subtyping [1, Def. 2.3]. The intersection type constructor (∩)
is assumed commutative, associative, and idempotent. We write τ ⊆ σ if σ = τ ∩ ρ. A formula σTTT
is functional if σ = i∈I (σi → τi ), and we define lhs(σ) = i∈I σi and rhs(σ) = i∈I τi .
A column (ranged over by γ, δ, ν) of height m is a vector of m formulas. A column is called
functional if all its coordinates are functional, otherwise it is atomic.
An m × n-matrix (ranged over by Γ) of formulas σij , where i = 1 . . . m and j = 1 . . . n, is
i=1...m . If Γ is an m × n-matrix, and γ is a column of height m, then Γ, γ stands for
written [σij ]j=1...n
an m × (n+1)-matrix obtained by adding γ as the (n+1)-st column.
Let f : {1, . . . , m2 } → {1, . . . , m1 } be onto. If γ = (σ1 , . . . , σm2 ), then f (γ) is a column ofTheight m1 whose k-th coordinate is f (i)=k σi . And if δ = (τ1 , . . . , τm1 ), then f −1 (δ) is a columnof height m2 whose j-th coordinate is τf (j) . The notation f −1 extends to matrices columnwise.
We write Γ1 vf Γ2 if there exist columns γ1 , . . . , γk such that Γ2 is f −1 (Γ1 ), γ1 , . . . , γk up tocolumn permutation. The relations ≤, ⊆ and functions lhs, rhs extend to columns coordinatewise.
If γ ≤ δ (resp. δ ⊆ γ), for some column γ of Γ, then we write Γ ≤ δ (resp. δ ⊆ Γ). If γ = (σ1 , . . . , σm )and δ = (τ1 , . . . , τm ), then γ ⇒ δ denotes the column (σ1 → τ1 , . . . , σm → τm ).
Submitted to:
ITRS 2020

c A. Dudenhefner, P. Urzyczyn
This work is licensed under theCreative Commons Attribution License.

2

Kripke Semantics for Intersection Formulas

Sequent calculus Judgments (cf. molecules of [6]) take the form Γ ` γ, where Γ is a matrixand γ is a column of the same height. The following sequent calculus is sound and complete(Proposition 1) for BCD inhabitation [1, Def. 2.5].
(Γ ≤ γ)Γ`γ(A)Γ, rhs(γ) ` δΓ ` (ω, . . . , ω)
Γ ` lhs(γ)
Γ`δ

(Ω)

(γ ⊆ Γ)(L)Γ`γΓ, γ ` δΓ`δ

f −1 (Γ), γ ` δΓ ` f (γ ⇒ δ)

(Cut)

(R)

For Γ = [σij ]i=1...mj=1...n and γ = (τ1 , . . . , τm ), we write Γ `bcd γ if there exists a λ-term M suchthat {x1 : σi1 , . . . , xn : σin } `bcd M : τi , for i = 1 . . . m.
Proposition 1. We have Γ ` γ iff Γ `bcd γ.
Kripke-style semantics We define a Kripke model M = hC, ≤, G, Hi, where: C is a nonempty
set of states; ≤ is a partial order on C; G is a function that assigns an atomic matrix ΓC to every
state C ∈ C; H is a function that assigns a surjection f to every pair C ≤ D, written C ≤f D.
Additionally, for every C, D, E ∈ C we require: if C ≤f D, then ΓC vf ΓD ; if C ≤f D ≤g E, thenC ≤g◦f E; and C ≤id C.
Forcing: Let ΓC and δ be of height m. The state C forces δ, written C δ, if either δ isequivalent to (ω, . . . , ω) under subtyping, or one of the following holds:• The column δ is atomic and ΓC ≤ δ.
• The column δ is functional, and for all D ∈ C such that C ≤f D and for every column νsuch that ν ⊆ f −1 (δ) and D lhs(ν) we have D rhs(ν).
A model is monotone 1 if for every state C and γ such that ΓC ≤ γ, we have C γ.
We write C Γ if C forces all columns in Γ. Finally, the notation Γ γ means that:
For every monotone model M and every state C, if C Γ, then C γ.
Example 2. Let δ = ((p → ω → p)∩ (ω → p → p)) be a column of height 1 and C = {1, 2}, whereΓ1 = () is a 1 × 0-matrix, Γ2 = pω ωp is a 2 × 2-matrix, and 1 ≤f 2, where f : {1, 2} → {1} is suchp→ω→p
that f (1) = f (2) = 1. For ν = ω→p→p, we have that 1 ≤f 2, ν ⊆ f −1 (δ), and 2 lhs(ν) = ωp .
ωpHowever, we have that 2 1 rhs(ν) = ω→p
p→p , because 2 lhs(rhs(ν)) = p , but 2 1 rhs(rhs(ν)) = p .
Overall, we have that 1 1 δ, providing a countermodel. Therefore, ∅ 1 δ. Besides, ∅ 6`bcd δ.
Game playing The game is played by two competitors, who influence a game position, which
is a judgment Γ ` δ. The existential player, ∃ros, tries to prove δ from Γ, i.e. to reach a positionin which δ = (ω, . . . , ω) or Γ ≤ δ. The universal player, ∀phrodite, attempts to refute his claims.
Similarly to [7, Section 2], possible game moves essentially correspond to rules (L) and (R).
Therefore, a winning ∃ros’ strategy leads to a cut-free sequent calculus proof. Complementarily,
from a winning ∀phrodite’s strategy a Kripke countermodel can be constructed.
Theorem 3 (Soundness and Completeness). We have ∅ `bcd σ iff ∅ (σ).
Proof Sketch. Soundness is shown by Proposition 1 followed by structural induction with respect
to proofs. Completeness is shown by constructing a countermodel from a winning strategy of∀phrodite using methods of [7, Section 2].
1

Model monotonicity is naturally satisfied if we restrict attention to formulas that have uniform structure, i.e.
refine some simple type in the sense of [2], such as in Example 2.

A. Dudenhefner, P. Urzyczyn

3

References[1] Henk Barendregt, Mario Coppo & Mariangiola Dezani-Ciancaglini (1983): A Filter Lambda Modeland the Completeness of Type Assignment. J. Symb. Log. 48(4), pp. 931–940.
[2] Michael Kohlhase & Frank Pfenning (1993): Unification in a Lambda-Calculus with Intersection
Types. In Dale Miller, editor: Logic Programming, Proceedings of the 1993 International Symposium,
Vancouver, British Columbia, Canada, October 26-29, 1993, MIT Press, pp. 488–505.
[3] Elaine Pimentel, Simona Ronchi Della Rocca & Luca Roversi (2012): Intersection Types from a
Proof-theoretic Perspective. Fundam. Inform. 121(1-4), pp. 253–274.
[4] Garrel Pottinger (1980): A Type Assingment for the Strongly Normalizable λ-terms. In J.P. Seldin &J.R. Hindley, editors: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, pp. 561–577.
[5] Simona Ronchi Della Rocca & Luca Roversi (2001): Intersection Logic. In Laurent Fribourg, editor:
Computer Science Logic, 15th International Workshop, CSL 2001., Lecture Notes in Computer Science
2142, Springer, pp. 414–428.
[6] Simona Ronchi Della Rocca, Alexis Saurin, Yiorgos Stavrinos & Anastasia Veneti (2010): Intersection
Logic in sequent calculus style. In Elaine Pimentel, Betti Venneri & Joe B. Wells, editors: Proceedings
Fifth Workshop on Intersection Types and Related Systems, ITRS 2010, Edinburgh, U.K., 9th July
2010., EPTCS 45, pp. 16–30.
[7] Paweł Urzyczyn (2016): Intuitionistic Games: Determinacy, Completeness, and Normalization. Studia Logica 104(5), pp. 957–1001.
[8] Betti Venneri (1994): Intersection Types as Logical Formulae. Journal of Logic and Computation
4(2), pp. 109–124.

Revisiting the Bang Calculus
Antonio Bucciarelli

Delia Kesner

IRIF, CNRS and Université de Paris, France

IRIF, CNRS and Université de Paris, FranceInstitut Universitaire de France, France

Alejandro Rı́os

Andrés Viso

Universidad de Buenos Aires, Argentina

Universidad de Buenos Aires, Argentina
Universidad Nacional de Quilmes, Argentina

Extended abstract1
Call-by-Push-Value. The Call-by-Push-Value (CBPV) paradigm, introduced by P.B. Levy [34, 35],
distinguishes between values and computations under the slogan “a value is, a computation does”. It
subsumes the λ -calculus by adding some primitives that allow to capture both the Call-by-Name (CBN)and Call-by-Value (CBV) semantics. CBN is a lazy strategy that consumes arguments without any
preliminary evaluation, potentially duplicating work, while CBV is greedy, always computing arguments
disregarding whether they are used or not, which may prevent a normalising term from terminating,e.g. (λ x.I) Ω, where I = λ x.x and Ω = (λ x.x x) (λ x.x x).
Essentially, CBPV introduces unary primitives thunk and force. The former freezes the executionof a term (i.e. it is not allowed to compute under a thunk) while the latter fires again a frozen term.
Informally, force (thunkt) is semantically equivalent to t. Resorting to the paradigm slogan, thunkturns a computation into a value, while force does the opposite. Thus, CBN and CBV are captured
by conveniently labelling a λ -term using force and thunk to pause/resume the evaluation of a subterm
depending on whether it is an argument (CBN) or a function (CBV). In doing so, CBPV provides a uniqueformalism capturing two distinct λ -calculi strategies, thus allowing to study operational and denotationalsemantics of CBN and CBV in a unified framework.
Bang calculus. T. Ehrhard [23] introduces a typed calculus, that can be seen as a variation of CBPV,
to establish a relation between this paradigm and Linear Logic (LL). A simplified version of this formalism is later dubbed Bang calculus [24], showing in particular how CBPV captures the CBN and CBVsemantics of λ -calculus via Girard’s translations of intuitionistic logic into LL. The Bang calculus isessentially an extension of λ -calculus with two new constructors, namely bang (!) and dereliction (der),together with the reduction rule der (!t) 7→ t. There are two notions of reduction for the Bang calculus,
depending on whether it is allowed to reduce under a bang constructor or not. They are called strong andweak reduction respectively. Indeed, it is weak reduction that makes bang/dereliction play the role of theprimitives thunk/force. Hence, these modalities are essential to capture the essence behind the CBN–
CBV duality. A similar approach appears in [38], studying (simply typed) CBN and CBV translations
into a fragment of IS4, recast as a very simple λ -calculus equipped with an indeterminate lax monoidal
comonad.
Non-Idempotent Types. Intersection types, pioneered by [15, 16], can be seen as a syntactical tool
to denote programs. They are invariant under the equality generated by the evaluation rules, and typeall and only all normalising terms. They are originally defined as idempotent types, so that the equation
1 The full version of this work is currently submitted to an international conference.

Submitted to:
ITRS 2020c Bucciarelli, Kesner, Rı́os & Viso
This work is licensed under theCreative Commons Attribution License.

2

Revisiting the Bang Calculusσ ∩ σ = σ holds, thus preventing any use of the intersection constructor to count resources. On the other
hand, non-idempotent types, pioneered by [25], are inspired from LL, they can be seen as a syntacticalformulation of its relational model [27, 11]. This connection suggests a quantitative typing tool, being
able to specify properties related to the consumption of resources, a remarkable investigation pioneeredby the seminal de Carvalho’s PhD thesis [17] (see also [19]). Non-idempotent types have also beenused to provide characterisations of complexity classes [8]. Several papers explore the qualitative andquantitative aspects of non-idempotent types for different higher order languages, as for example Callby-Name, Call-by-Need and Call-by-Value λ -calculi, as well as extensions to Classical Logic. Some
references are [13, 22, 4, 3, 33]. Other relational models were directly defined in the more generalcontext of LL, rather than in the λ -calculus [18, 30, 21, 20].
An interesting recent research topic concerns the use of non-idempotent types to provide bounds of
reduction lengths. More precisely, the size of type derivations has often been used as an upper bound to
the length of different evaluation strategies [36, 22, 31, 13, 32, 33]. A key notion behind these works isthat when t evaluates to t 0 , then the size of the type derivation of t 0 is smaller than the one of t, thus thesize of type derivations provides an upper bound for the length of the reduction to a normal form as well
as for the size of this normal form.
A crucial point to obtain exact bounds, instead of upper bounds, is to consider only minimal typederivations, as the ones in [17, 9, 21]. Another approach was taken in [1], which uses an appropriate
notion of tightness to implement minimality, a technical tool adapted to Call-by-Value [28, 3] and Callby-Need [4].

Contributions and Related Works
This work presents a reformulation of the untyped Bang calculus, and proposes a quantitative study of it
by means of non-idempotent types.
The Untyped Reduction. The Bang calculus in [23] suffers from the absence of commutative conversions [37, 14], making some redexes to be syntactically blocked when open terms are considered. A
consequence of this approach is that there are some normal forms that are semantically equivalent to
non-terminating programs, a situation which is clearly unsound. This is repaired in [24] by adding commutative conversions specified by means of σ -reduction rules, which are crucial to unveil hidden (value)
redexes. However, this approach presents a major drawback since the resulting combined reduction
relation is not confluent.
Our revisited Bang calculus, called λ !, fixes these two problems at the same time. Indeed, the syntax
is enriched with explicit substitutions, and σ -equivalence is integrated in the primary reduction system byusing the distance paradigm [5], without any need to unveil hidden redexes by means of an independent
relation. This approach restores confluence.
The Untyped CBN and CBV Encodings. CBN and CBV (untyped) translations are extensively
studied in [29]. The authors establish two encodings cbn and cbv, from untyped λ -terms into untyped
terms of the Bang calculus, such that when t reduces to u in CBN (resp. CBV), cbn(t) reduces to cbn(u)(resp. cbv(t) reduces to cbv(u)) in the Bang calculus. However, CBV normal forms in λ -calculus are notnecessarily translated to normal forms in the Bang calculus.
Our revisited notion of reduction naturally encodes (weak) CBN as well as (open) CBV. These two
notions are dual: weak CBN forbids reduction inside arguments, which are translated to bang terms,
while open CBV forbids reduction under λ -abstractions, also translated to bang terms. More precisely,
we simply extend to explicit substitutions the original CBN translation from λ -calculus to the Bangcalculus, which preserves normal forms, but we subtly reformulate the CBV one. In contrast to [29], ourBucciarelli, Kesner, Rı́os & Viso3

CBV translation does preserve normal forms.
The Typed System. We propose a type system for the λ !-calculus, called U , based on nonidempotent intersection types. System U is able to fully characterise normalisation, in the sense that aterm t is U -typable if and only if t is normalising. More interestingly, we show that system U has alsoa quantitative flavour, in the sense that the length of any reduction sequence from t to normal form plus
the size of this normal form is bounded by the size of the type derivation of t. We show that system U
also captures the non-idempotent intersection type system for CBN given in [25, 17], and extended with
explicit substitutions as in [32], as well as a new type system V that we define for CBV, as defined in [6].
System V characterises termination of open CBV, in the sense that t is typable in V if and only if t is terminating in open CBV. This can be seen as another (collateral) contribution of this work. Moreover, theCBV embedding in [29] is not complete with respect to their type system for CBV. System V recovers
completeness (left as an open question in [29]). Finally, an alternative CBV encoding of typed terms is
proposed. This encoding is not only sound and complete, but now enjoys preservation of normal-forms.
A Refinement of the Type System Based on Tightness. A major observation concerning β reduction in λ -calculus (and therefore in the Bang calculus) is that the size of normal forms can be
exponentially bigger than the number of steps to these normal forms. This means that bounding thesum of these two integers at the same time is too rough, not very relevant from a quantitative point ofview. Following ideas in [17, 9, 1], we go beyond upper bounds. Indeed, another major contribution ofthis work is the refinement of the non-idempotent type system U to another type system E , equippedwith constants and counters, together with an appropriate notion of tightness (i.e. minimality). This new
formulation fully exploits the quantitative aspect of the system, in such a way that upper bounds provided by system U are refined now into independent exact bounds for time and space. More precisely,
given a tight type derivation Φ with counters (b, e, s) for a term t, we can show that t is normalisable in(b + e)-steps and its normal form has size s. The opposite direction also holds. Therefore, exact measuresconcerning the dynamic behaviour of t, are extracted from a static (tight) typing property of t.
Acknowledgements. This is an extended abstract of [12], to appear in FLOPS 2020. This work has
been partially funded by the projects ECOS-Sud PA17C01 and LIA INFINIS/IRP SINFIN.

References[1] Beniamino Accattoli, Stéphane Graham-Lengrand, and Delia Kesner.
PACMPL, 2 (ICFP):94:1–94:30, 2018.

Tight typings and split bounds.

[2] Beniamino Accattoli and Giulio Guerrieri. Open call-by-value. Asian Programming Languages and Systems
Symposium (APLAS), Hanoi, Vietnam, LNCS 10017, pages 206–226, 2016.
[3] Beniamino Accattoli and Giulio Guerrieri. Types of fireballs. Asian Programming Languages and Systems
Symposium (APLAS), Wellington, New Zealand, LNCS 11275, pages 45–66. Springer, 2018.
[4] Beniamino Accattoli, Giulio Guerrieri, and Maico Leberle. Types by need. Programming Languages andSystems European Symposium on Programming (ESOP), Prague, Czech Republic, LNCS 11423, pages 410–
439. Springer, 2019.
[5] Beniamino Accattoli and Delia Kesner. The structural λ -calculus. Int. Conf. on Computer Science Logic(CSL), Brno, Czech Republic, LNCS 6247, pages 381–395. Springer, 2010.
[6] Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. Int. Symposium on Functionaland Logic Programming (FLOPS), Kobe, Japan, LNCS 7294, pages 4–16. Springer, 2012.
[7] Hendrik P. Barendregt. The Lambda Calculus Its Syntax and Semantics, volume 103. North Holland, revised
edition, 1984.

4

Revisiting the Bang Calculus[8] Erika De Benedetti and Simona Ronchi Della Rocca. A type assignment for λ -calculus complete both for
FPTIME and strong normalization. Information and Computation, 248:195–214, 2016.
[9] Alexis Bernadet and Stéphane Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013.
[10] Marc Bezem, Jan Willem Klop, and Vincent van Oostrom. Term Rewriting Systems (TeReSe). Cambridge
University Press, 2003.
[11] Antonio Bucciarelli and Thomas Ehrhard. On phase semantics and denotational semantics: the exponentials.
Annals of Pure Applied Logic, 109(3):205–241, 2001.
[12] Antonio Bucciarelli, Delia Kesner, Alejandro Rı́os and Andrés Viso. The Bang Calculus Revisited. International Symposium on Functional and Logic Programming (FLOPS), Akita, Japan, LNCS, Springer, 2020.
[13] Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for the lambdacalculus. Logic Journal of the IGPL, 25(4):431–464, 2017.
[14] Alberto Carraro and Giulio Guerrieri. A semantical and operational account of call-by-value solvability.
Int. Conf. on Foundations of Software Science and Computation Structures (FOSSACS), Grenoble, France,
LNCS 8412, pages 103–118. Springer, 2014.
[15] Mario Coppo and Mariangiola Dezani-Ciancaglini. A new type assignment for λ -terms. Archive for Mathematical Logic, 19(1):139–156, 1978.
[16] 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, 1980.
[17] Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Université AixMarseille II, 2007.
[18] Daniel de Carvalho. The relational model is injective for multiplicative exponential linear logic. Int. Conf. on
Computer Science Logic (CSL), Marseille, France, LIPIcs 62, pages 41:1–41:19. Schloss Dagstuhl - LeibnizZentrum fuer Informatik, 2016.
[19] Daniel de Carvalho. Execution time of λ -terms via denotational semantics and intersection types. Mathematical Structures in Computer Science, 28(7):1169–1203, 2018.
[20] Daniel de Carvalho and Lorenzo Tortora de Falco. A semantic account of strong normalization in linear
logic. Information and Computation, 248:104–129, 2016.
[21] Daniel de Carvalho, Michele Pagani, and Lorenzo Tortora de Falco. A semantic measure of the execution
time in linear logic. Theoretical Computer Science, 412(20):1884–1902, 2011.
[22] Thomas Ehrhard. Collapsing non-idempotent intersection types. Int. Conf. on Computer Science Logic(CSL), Fontainebleau, France, LIPIcs 16, pages 259–273. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012.
[23] Thomas Ehrhard. Call-by-push-value from a linear logic point of view. European Symposium on Programming (ESOP), Eindhoven, The Netherlands, LNCS 9632, pages 202–228. Springer, 2016.
[24] Thomas Ehrhard and Giulio Guerrieri. The bang calculus: an untyped lambda-calculus generalizing call-byname and call-by-value. Int. Symposium on Principles and Practice of Declarative Programming (PPDP),
Edinburgh, United Kingdom, pages 174–187. ACM, 2016.
[25] Philippa Gardner. Discovering needed reductions using type theory. Int. Conf. on Theoretical Aspects ofComputer Software (TACS), Sendai, Japan, LNCS 789, pages 555–574. Springer, 1994.
[26] Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50:1–102, 1987.
[27] Jean-Yves Girard. Normal functors, power series and λ -calculus. Annals of Pure Applied Logic, 37(2):129–
177, 1988.
[28] Giulio Guerrieri. Towards a semantic measure of the execution time in call-by-value lambda-calculus. Joint
Int. Workshops on Developments in Computational Models and Intersection Types and Related Systems(DCM/ITRS), Oxford, UK, EPTCS 283, pages 57–72, 2018.

Bucciarelli, Kesner, Rı́os & Viso5[29] Giulio Guerrieri and Giulio Manzonetto. The bang calculus and the two girard’s translations. Joint Int.
Workshops on Linearity & Trends in Linear Logic and Applications (Linearity-TLLA), Oxford, UK, EPTCS,
pages 15–30, 2019.
[30] Giulio Guerrieri, Luc Pellissier, and Lorenzo Tortora de Falco. Computing connected proof(-structure)sfrom their taylor expansion. Int. Conf. on Formal Structures for Computation and Deduction (FSCD), Porto,
Portugal, LIPIcs 52, pages 20:1–20:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.
[31] Delia Kesner. Reasoning about call-by-need by means of types. Int. Conf. on Foundations of Software
Science and Computation Structures (FOSSACS), Eindhoven, The Netherlands, LNCS 9634, pages 424–
441. Springer, 2016.
[32] Delia Kesner and Daniel Ventura. Quantitative types for the linear substitution calculus. Int. Conf. on
Theoretical Computer Science (IFIP/TCS), Rome, Italy, LNCS 8705, pages 296–310. Springer, 2014.
[33] Delia Kesner and Pierre Vial. Types as resources for classical natural deduction. Int. Conf. on Formal
Structures for Computation and Deduction (FSCD), Oxford, UK, LIPIcs 84, pages 24:1–24:17. Schloss
Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017.
[34] Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis, volume 2 of Semantics Structuresin Computation. Springer, 2004.
[35] Paul Blain Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order andSymbolic Computation, 19(4):377–414, 2006.
[36] Michele Pagani and Simona Ronchi Della Rocca. Solvability in resource lambda-calculus. Int. Conf. on
Foundations of Software Science and Computational Structures (FOSSACS), Paphos, Cyprus, LNCS 6014,
pages 358–373. Springer, 2010.
[37] Laurent Regnier. Une équivalence sur les lambda-termes. TCS, 2(126):281–292, 1994.
[38] José Espı́rito Santo, Luı́s Pinto, and Tarmo Uustalu. Modal embeddings and calling paradigms. Int. Conf. on
Formal Structures for Computation and Deduction (FSCD), Dortmund, Germany, LIPIcs 131, pages 18:1–
18:20. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2019.

Observability by Means of Typability and Inhabitation
Antonio Bucciarelli

Delia Kesner

IRIF, CNRS and Université de Paris, France

IRIF, CNRS and Université de Paris, FranceInstitut Universitaire de France, France

Simona Ronchi Della Rocca
Dipartimento di Informatica, Università di Torino, Italy

Extended abstract
In these last years there has been a growing interest in pattern λ -calculi [13, 10, 7, 11, 9, 12] which areused to model the pattern-matching primitives of functional programming languages (e.g. OCAML, ML,
Haskell) and proof assistants (e.g. Coq, Isabelle). These calculi are extensions of λ -calculus: abstractions
are written as λ p.t, where p is a pattern specifying the expected structure of the argument. In this work
we restrict our attention to pair patterns, which are expressive enough to illustrate the challenging notionof solvability/observability in the framework of pattern λ -calculi. More precisely, we consider a patterncalculus called p-calculus, introduced in [2], with explicit pattern-matching and reduction rules at a
distance [1]. The p-calculus is inspired from the Λp -calculus in [4]. The use of explicit pattern-matching
becomes very appropriate to implement different evaluation strategies, thus giving rise to different
languages with pattern-matching [7, 8, 3].
We aim to study observability of the p-calculus, which corresponds to solvability of λ -calculus. Let us
first recall this last notion: a closed λ -term t is solvable if there is n ≥ 0 and there are terms u1 , ..., un suchthat tu1 ...un reduces to the identity. Closed solvable terms represent meaningful programs: if t is closed
and solvable, then t can produce any desired result when applied to a suitable sequence of arguments.
The relation between solvability and meaningfulness is also evident in the semantics: it is sound to equate
all unsolvable terms, as in Scott’s original model D∞ [14]. This notion can be easily extended to open
terms, through the notion of head-context, which does the job of both closing the term and then applying
it to an appropriate sequence of arguments. Thus a term t is solvable if there is a head-context H such that,when H is filled by t, then H[t] is closed and reduces to the identity.
In order to extend the notion of solvability to the p-calculus, it is clear that pairs have to be taken
into account. A relevant question is whether a pair should be considered as meaningful in any case.
At least two choices are possible: a lazy semantics considering any pair to be meaningful, or a strict
one requiring both of its components to be meaningful. In the operational semantics we supply for the
p-calculus the constant fail is different from hfail, faili: if a term reduces to fail we do not have
any information about its result, but if it reduces to hfail, faili we know at least that it represents apair. In fact, being a pair is already an observable property, which in particular is sufficient to unblock an
explicit matching, independently from the observability of its components. As a consequence, a term t isdefined to be observable iff there exists a head-context H such that H[t] is closed and reduces to a pair.
Thus for example, the term ht, ti is always observable, also in case t is not observable. Observability
turns out to be conservative with respect to the notion of solvability for the λ -calculus.
We characterize observability for the p-calculus through two different and complementary notions
related to a type assignment system with non-idempotent intersection types that we call P. The first one
Submitted to:
ITRS 2020c Bucciarelli, Kesner, Ronchi Della Rocca
This work is licensed under theCreative Commons Attribution License.

2

Observability by Means of Typability and Inhabitation

is typability, concerning the possibility to construct a typing derivation for a given term, and the second
one is inhabitation, concerning the possibility to construct a term from a given typing. More precisely, we
first supply a notion of canonical form such that reducing a term to some canonical form is a necessary
but not a sufficient condition for being observable. In fact, canonical forms may contain blocking explicit
matchings, so that we need to guess whether or not there exists a substitution being able to simultaneously
unblock all these blocked forms. In contrast, if a λ -term is in canonical form, it is always possible to findsuitable arguments to feed it in order to produce any desired term (in fact, the identity). Hence typable
λ -terms are observable. This is somehow an accidental property, and for more general calculi, like thep-calculus, the fact that a term t has a type does not guarantee that suitable arguments to be applied to t
in order to produce the desired observable result do exist. Our type system P characterizes canonicalforms: a term t has a canonical form if and only if it is typable in system P. Types are of the shape
A1 → A2 → ... → An → σ , for n ≥ 0, where the Ai ’s are multisets of types and σ is a type. The use ofmultisets to represent the non-idempotent intersection is standard, namely [σ1 , ..., σm ] is just a notationfor σ1 ∩ ... ∩ σm . By using type system P we can supply the following characterization of observability:
a closed term t is observable if and only if t is typable in system P, let say with a type of the shape
A1 → A2 → ... → An → σ (where σ is a product type), and for all 1 ≤ i ≤ n there is a term ti such thatevery type in Ai is inhabited by ti . In fact, if ui inhabits all the types in Ai , then tu1 ...un , resulting fromplugging t into the head context u1 ...un , reduces to a pair. The extension of this notion to open terms is
obtained by suitably adapting the notion of head context.
Clearly, the property of being observable is undecidable, exactly as the solvability property for λ calculus. More precisely, the property of having canonical form is undecidable, since the λ -terms that aretypable in system P, characterizing terms having canonical form, are exactly the solvable ones. But ourcharacterization of observability through the inhabitation property of P does not add a further level ofundecidability: in fact we prove that inhabitation for system P is decidable,in constrast to the idempotent
case where the problem is known to be undecidable [15]. The inhabitation algorithm presented here is a
non trivial extension of the one given in [5, 6] for the λ -calculus, the difficulty of the extension being due
to the explicit pattern matching and to the type information of patterns.
This work simplifies a previous study of observability for pattern calculi in [4], not only from theoperational semantics of the pattern calculus, but also from the typing system point of view.

References[1] B. Accattoli and D. Kesner. The structural lambda-calculus. In A. Dawar and H. Veith, editors, Proceedings of
24th EACSL Conference on Computer Science Logic, volume 6247 of LNCS, pages 381–395. Springer, Aug.
2010.
[2] S. Alves, D. Kesner, and D. Ventura. A quantitative understanding of pattern matching. arXiv:1912.01914,
2020.
[3] T. Balabonski. On the implementation of dynamic patterns. In E. Bonelli, editor, HOR, volume 49 of EPTCS,
pages 16–30, 2010.
[4] A. Bucciarelli, D. Kesner, and S. R. D. Rocca. Observability for pair pattern calculi. In T. Altenkirch,
editor, 13th International Conference on Typed Lambda Calculi and Applications, TLCA 2015, July 1-3, 2015,
Warsaw, Poland, volume 38 of LIPIcs, pages 123–137. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik,
2015.
[5] A. Bucciarelli, D. Kesner, and S. Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types. In TCS, volume 8705 of LNCS, pages 341–354. Springer, 2014.

Bucciarelli, Kesner, Ronchi Della Rocca

3[6] A. Bucciarelli, D. Kesner, and S. Ronchi Della Rocca. Inhabitation for non-idempotent intersection types.
Logical Methods in Computer Science, 14(3), 2018.
[7] S. Cerrito and D. Kesner. Pattern matching as cut elimination. Theoretical Computer Science, 323(1-3):71–127,
2004.
[8] H. Cirstea, G. Faure, and C. Kirchner. A rho-calculus of explicit constraint application. Higher-Order andSymbolic Computation, 20(1-2):37–72, 2007.
[9] B. Jay and D. Kesner. First-class patterns. Journal of Functional Programming, 19(2):191–225, 2009.
[10] W. Kahl. Basic pattern matching calculi: A fresh view on matching failure. In Y. Kameyama and P. Stuckey,
editors, FLOPS, volume 2998 of LNCS, pages 276–290. Springer, 2004.
[11] J.-W. Klop, V. van Oostrom, and R. de Vrijer. Lambda calculus with patterns. Theoretical Computer Science,
398(1-3):16–31, 2008.
[12] B. Petit. A polymorphic type system for the lambda-calculus with constructors. In TLCA, volume 5608 oflncs, pages 234–248. Springer, 2009.
[13] S. Peyton-Jones. The Implementation of Functional Programming Languages. Prentice-Hall, Inc., 1987.
[14] D. S. Scott. Outline of a mathematical theory of computation. In Fourth Annual Princeton Conference on
Information Sciences and Systems, pages 169–176. Departement of Elctrical Engeneering, Princeton Univ.,
1970.
[15] P. Urzyczyn. The emptiness problem for intersection types. Journal of Symbolic Logic, 64(3):1195–1215,
1999.

Quantitative Types for the Atomic λ-calculus
Loı̈c Peyrot and Delia Kesner
Université de Paris (IRIF, CNRS)
lpeyrot@irif.fr, kesner@irif.fr

Deep inference is a logical formalism developed inside the framework of the calculus ofstructures. It exhibits proofs with contexts, which avoids some syntactic bureaucracies [6].
The atomic λ-calculus was designed as a Curry-Howard interpretation of deep-inference for
intuistionistic logic [7]. It is an extension of λ-calculus with sharing mechanisms resembling
explicit substitutions. When duplication of shared terms is needed, it is carried out atomically:
constructor by constructor. These two features, sharing and atomic duplication, are at thecore of fully lazy sharing [1]. Whereas this mechanism is usually specified by means of sharing
graphs or other graphical formalisms, atomic λ-calculus is to our knowledge the first algebraic
representation of the λ-calculus which can express it in a natural way. As expected, the atomic
λ-calculus can be typed inside the deep inference formalism, but also inside the sequent calculus.
Typed atomic λ-calculus enjoys the desired properties of subject reduction, confluence, andstrong normalisation [8].
Still, the calculus has not been extensively studied until today. It is also strongly syntactical:
there is still no known model for it. We approach this calculus throughout non-idempotent
intersection types [5]. We hope that their semantical flavour [4] will help us uncover some of
the calculus’ aspects.
We define a quantitative type system characterising strong normalisation, i.e we use nonidempotent types instead of the more standard idempotent ones. Our type system follows thesequent calculus style. We prove the correctness of our type system: every typed term strongly
normalises, as well as completeness: every strongly normalisable term is typable. Our proof ofcorrectness is an alternative to the original one using candidates of reducibility [8].
Usually, proofs of termination using a quantitative discipline are straightforward (a survey
can be found in [3]). During the substitution of a variable x by a term u, typing derivations
for the types of u are dispatched in place of the axioms rules of x, but none is duplicated.
Therefore, the size of the typing derivation can only decrease during reduction. But within theatomic λ-calculus, the duplication of the constructors induces an introduction of new resources(typically variables). For instance, to duplicate an application uv, we have to substitute every
variable x bound to uv by an application of two new variables, say y and z where y is boundto u and z to v. By doing that, we duplicate the types of u and v to be able to type the newvariables.
However, we are able to give a characterisation of termination through a subtle transformation of terms, that we call expansion. The idea of an expansion is to anticipate the creation of
the duplicates. Then, we show that the size of the typing derivation of the expansion of a term
decreases along any reduction step.
Our main contribution is an original type system for atomic λ-calculus, which is the firstquantitative one, to our knowledge. Because we have to use a mechanism to reveal the resourceconsuming nature of reduction in a quantitative typing discipline, we believe that a quantitative
sequent calculus type system is not the most appropriate for atomic λ-calculus. It strengthens
the idea that we should be looking for a way to describe intersection types directly in deep inference. This has already been studied but never led to a result on the full atomic λ-calculus [9].
We believe that our work will contribute to the quest of such typing system.

Quantitative Types for the Atomic λ-calculus

Peyrot and Kesner

References[1] Thibaut Balabonski. A unified approach to fully lazy sharing. ACM SIGPLAN Notices, 47:469–480,
01 2012.
[2] Alexis Bernardet and Stéphane Graham-Lengrand. Non-idempotent intersection types and strong
normalisation. Logical Methods in Computer Science, 9(4):17–42, 2013.
[3] Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. Non-idempotent intersection types for thelambda-calculus. Logic Journal of the IGPL, 25:433–464, 08 2017.
[4] Daniel de Carvalho. Sémantiques de la logique linéaire et temps de calcul. PhD thesis, Université
Aix-Marseille II, 2007.
[5] Philippa Gardner. Discovering needed reductions using type theory. In Masami Hagiya and John C.
Mitchell, editors, Theoretical Aspects of Computer Software, pages 555–574, Berlin, Heidelberg,
1994. Springer Berlin Heidelberg.
[6] Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A proof calculus which reduces syntactic bureaucracy. Proceedings of the 21st International Conference on Rewriting Techniques andApplications, RTA 2010, 6, 01 2010.
[7] Tom Gundersen, Willem Heijltjes, and Michel Parigot. Atomic lambda calculus: A typed lambdacalculus with explicit sharing. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on
Logic in Computer Science, LICS ’13, pages 311–320, Washington, DC, USA, 2013. IEEE Computer
Society.
[8] Tom Gundersen, Willem Heijltjes, and Michel Parigot. A proof of strong normalisation of the typed
atomic lambda-calculus. In Ken McMillan, Aart Middeldorp, and Andrei Voronkov, editors, Logic
for Programming, Artificial Intelligence, and Reasoning, pages 340–354, Berlin, Heidelberg, 2013.
Springer Berlin Heidelberg.
[9] Joseph W. N. Paulus and Heijltjes Willem. Deep-inference intersection types, 2018.

2

A Type Checker for a Logical Frameworkwith Union and Intersection Types
Claude Stolze

Luigi Liquori

IRIF, Université de Paris

Inria, Université Côte d’Azur

stolze@irif.fr

Luigi.Liquori@inria.fr

1 Introduction
We present the syntax, semantics, and typing rules of Bull [14], a prototype theorem prover based onthe ∆-framework, i.e. a fully-typed lambda-calculus decorated with union and intersection types, as described in [15, 9]. Bull also implements the subtyping algorithm of [10] for the Type Theory Ξ of [2].
Bull has a command-line interface where the user can declare axioms, terms, and perform computations
and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and fileloading. Moreover, it can typecheck a proof or normalize it. These terms can be incomplete, therefore
the typechecking algorithm uses unification to try to construct the missing subterms. Bull uses the syntax of Berardi’s Pure Type Systems [3] to improve the compactness and the modularity of the kernel.
Abstract and concrete syntax are mostly aligned and similar to the concrete syntax of Coq. Bull uses ahigher-order unification algorithm for terms, while typechecking and partial type inference are done bya bidirectional refinement algorithm, similar to the one found in [1]. The refinement can be split into twoparts: the essence refinement and the typing refinement. The bidirectional refinement algorithm aims tohave partial type inference, and to give as much information as possible to the unifier. For instance, if wewant to find a ?y such that `Σ hλ x:σ .x, λ x:τ.?yi : (σ → σ ) ∩ (τ → τ), we can infer that x:τ `?y : τ andthat o ?y o =β x. Binders are implemented using commonly-used de Bruijn indices. We have defined aconcrete language syntax that will allow user to write ∆-terms. We have defined the reduction rules andan evaluator. We have implemented from scratch a refiner which does partial typechecking and type reconstruction. We have experimented Bull with classical examples of the intersection and union literature,such as the ones formalized by Pfenning with his Refinement Types in LF [12].
Syntax of terms. The abstract syntax for the language is sketched below. The main differences with the∆-framework [9] are the additions of a placeholder and meta-variables, used by the refiner. We also added
a let operator and changed the syntax of the strong sum so it looks more like the concrete syntax usedin the implementation. A meta-variable ?x[∆1 ; ...; ∆n ] uses suspended substitutions, inspired by [1] andintuitively explained as follows: if we want to unify (λ x:σ .?y) c1 with c1 , we could unify ?y with c1 orwith x, the latter being the preferred solution. However, if we normalize (λ x:σ .?y) c1 , we should record
the fact that c1 can be substituted by any occurrence of x appearing the term to be replaced by ?y; the termis actually noted (λ x:σ .?y[x]) c1 and reduces to ?y[c1 ], noting that c1 has replaced x. Finally, following
the Cervesato-Pfenning jargon [5], applications are in spine form, i.e. the arguments of a function are
Submitted to:
ITRS 2020

c C. Stolze & L. Liquori
This work is licensed under theCreative Commons Attribution License.

2

Crafting a Type Checker

stored together in a list, exposing the head of the term separately.
∆, σ

S

::=
|
|
|
|
|
|
|

s|c|x|?x[∆; ...; ∆]let x:σ := ∆ in ∆
Πx:σ .∆ | λ x:σ .∆∆S | σ ∩σ | σ ∪σh∆, ∆i | pr1 ∆ | pr2 ∆smatch ∆ return σ with [x:σ ⇒ ∆ | x:σ ⇒ ∆]in1 σ ∆ | in2 σ ∆ | coe σ ∆::= () | (S; ∆)Sorts, constant, variables and placeholders
Meta-variable
Local definition
Dependent product and λ -abstraction
Application, intersection and union
Strong pair, left and right projection
Strong sum
Left/right injection and coercions
SpinesConcrete syntax is mostly aligned with the abstract one with the intention to mimic Coq.
Environments. There are four kinds of environments, namely 1) the global environment (noted Σ).
The global environment holds constants which are fully typechecked. 2) the local environment (noted
Γ). It is used for the first step of typechecking, and looks like a standard environment. 3) the essence
environment (noted Ψ). It is used for the second step of typechecking, and holds the essence of the local
variables. 4) the meta-environment (noted Φ). It is used for unification, and records meta-variables andtheir instantiation whenever the unification algorithm has found a solution.
Σ
Γ
Ψ
Φ

::=
::=
::=
::=

· | Σ, c:ς @σ | Σ, c := M@∆ : ς @σ
· | Γ, x:σ | Γ, x := ∆ : σ· | Ψ, x | Ψ, x := M
· | Φ, sort(?x) | Φ, ?x := s | Φ, (Γ `?x : σ ) | Φ, (Γ `?x := ∆ : σ ) | Φ, Ψ `?x | Φ, Ψ `?x := M

Evaluator. The evaluator follows the applicative order strategy, which recursively normalizes all subterms from left to right; in addition to the standard β δ ηζ -reduction rules, we have rules for projections
pri and injections ini .
Subtyping. It is the one extracted by Coq in [10]. The algorithm has been mechanically proved correct
in Coq by extending the certification of the algorithm for intersection types of Bessai [4], and it represent,
at the moment, the only mechanically certified (by Coq) part.
Unification. The Bull higher-order unification algorithm is inspired by the Reed [13] and Ziliani-Sozeau[16] papers. The unification algorithm takes as input a meta-environment Φ, a global environment Σ,a local environment Γ, the two terms to unify ∆1 and ∆2 , and either fails or returns the updated metaU?
environment Φ, namely Φ; Σ; Γ ` ∆1 = ∆2 Φ.
Refiner. Our typechecker is also a refiner: intuitively, a refiner takes as input an incomplete term, andpossibly an incomplete type, and tries to infer as much information as possible in order to reconstruct
a well-typed term. The Bull refiner is inspired by the work on the Matita ITP [1]. It is defined using
bi-directionality, in the style of Harper-Licata [8]. The bi-directional technique is a mix of typechecking
and type reconstruction, in order to trigger the unification algorithm as soon as possible. Moreover, it
gives more precise error messages than standard type reconstruction. There are five kind of judgments,
Φ1 ; Σ; Γ ` ∆1⇑

Φ1 ; Σ; Γ ` ∆1 : σ∆2 : σ ; Φ2⇓∆2 ; Φ2

Φ1 ; Σ; Γ ` σ1

Φ1 ; Σ; Ψ ` ∆Fσ2 : τ; Φ2

E⇑

M; Φ2

Φ1 ; Σ; Ψ ` M@∆E⇓

Φ

Read-Eval-Print-Loop. The REPL reads a command which is given by the parser as a list of atomic
commands. These commands are similar to the vernacular Coq commands and are quite intuitive. Hereis the list of the REPL commands, along with their description:

C. Stolze & L. Liquori
Help.
Load "file".
Axiom term : type.
Definition name [: type] := term.
Print name.
Printall.
Compute name.
Quit.

3
show this list of commands
for loading a script filedefine a constant or an axiom
define a term
print the definition of nameprint all the signature( axioms and definitions)normalize name and print the result
quit

Future work. The current version of Bull [14] (ver. 1.0, December 2019) is still a work-in-progress:
we plan to implement the following features: i) Inductive types à la Paulin-Mohring [11] (reasonably
feasible); ii) Mixing subtyping and unification, taking inspiration by the work of Dudenhefner, Martens,
and Rehof [7]; iii) Relevant arrow, as defined in [9], it could be useful to add more expressivity to oursystem. Relevant implication allows for a natural introduction of subtyping, in that A ⊃r B morally means
A 6 B. Relevant implication amounts to a notion of “proof-reuse”; iv) conceiving a Tactic language
should be feasible in the medium term.
Acknowledgements. This project could not be have be done without the many useful discussions with
Ugo de’Liguoro, Daniel Dougherty, Furio Honsell, and Ivan Scagnetto.

References[1] Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen & Enrico Tassi (2012): A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions. Logical Methods in Computer Science8(1).
[2] Franco Barbanera, Mariangiola Dezani-Ciancaglini & Ugo de’Liguoro (1995): Intersection and union types:
syntax and semantics. Information and Computation 119(2), pp. 202–230.
[3] Stefano Berardi (1988): Towards a mathematical analysis of the Coquand–Huet calculus of constructions
and the other systems in Barendregt’s cube. Ph.D. thesis, Dipartimento Matematica, Universita di Torino.
[4] Jan Bessai (2016): Extracting a formally verified Subtyping Algorithm for Intersection Types from Ideals andFilters. Talk at TYPES, slides.
[5] Iliano Cervesato & Frank Pfenning (2003): A linear spine calculus. Journal of Logic and Computation 13(5),pp. 639–688.
[6] Daniel J. Dougherty, Ugo de’Liguoro, Luigi Liquori & Claude Stolze (2016): A Realizability Interpretation
for Intersection and Union Types. In: Asian Symposium on Programming Languages and Systems (APLAS),
Lecture Notes in Computer Science 10017, Springer-Verlag, pp. 187–205.
[7] Andrej Dudenhefner, Moritz Martens & Jakob Rehof (2016): The Intersection Type Unification Problem. In:
Formal Structures for Computation and Deduction (FSCD), Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 19:1–19:16.
[8] Robert Harper & Daniel R. Licata (2007): Mechanizing Metatheory in a Logical Framework. Journal of
Functional Programming 17(4–5), pp. 613–673.
[9] Furio Honsell, Luigi Liquori, Claude Stolze & Ivan Scagnetto (2018): The Delta-Framework. In: Foundations of Software Technology and Theoretical Computer Science (FSTTCS), pp. 37:1–37:21.
[10] Luigi Liquori & Claude Stolze (2017): A Decidable Subtyping Logic for Intersection and Union Types.
In: Topics In Theoretical Computer Science (TTCS), Lecture Notes in Computer Science 10608, SpringerVerlag, pp. 74–90.

4Crafting a Type Checker[11] Christine Paulin-Mohring (1993): Inductive definitions in the system coq rules and properties. In: Typed
Lambda Calculi and Applications (TLCA), Springer, pp. 328–345.
[12] Frank Pfenning (1993): Refinement types for logical frameworks. In: TYPES, pp. 285–299.
[13] Jason Reed (2009): Higher-order constraint simplification in dependent type theory. In: Logical Frameworks
and Meta-Languages: Theory and Practice (LFMTP), ACM, pp. 49–56.
[14] Claude Stolze (2019): Bull. https://github.com/cstolze/Bull.
[15] Claude Stolze, Luigi Liquori, Furio Honsell & Ivan Scagnetto (2017): Towards a Logical Framework with
Intersection and Union Types. In: Logical Frameworks and Meta-languages: Theory and Practice (LFMTP),
pp. 1–9.
[16] Beta Ziliani & Matthieu Sozeau (2015): A unification algorithm for Coq featuring universe polymorphismand overloading. In: ACM SIGPLAN Notices, 50(9), ACM, pp. 179–191.

Intersection Types and Positive Almost Sure Termination
Ugo Dal Lago∗

Claudia Faggian†Simona Ronchi Della Rocca‡

Intersection types are well known not only to guarantee, but also to characterize certain normalization properties through typability. This include head, weak head, and strong normalization,and induces a compositional methodology for verifying the properties above, given that typing canbe assigned to terms in a syntax-directed way. This is not in contrast with undecidability of theunderlying decision problem: type inference itself remains an undecidabile problem.
The picture above have been generalized from termination to complexity properties [6, 3],
exploiting in a crucial way a non-idempotent form of intersection, in which any type τ is fundamentally different from τ ∩ τ . This allows to somehow count the number of copies each subterm
can be subject to, eventually allowing to give a precise bound [1, 2] on the number of reduction
steps necessary to reach the normal form.
Intersection types have recently been generalized to probabilistic lambda-calculi [7, 5] by the
first author with Flavien Breuvart [4], obtaining a characterization of almost sure termination(AST in the following), namely the condition in which non-termination can possibly happen, but
only with null probability. AST not being recursively enumerable [8], there is no hope to get a typesystem whose type derivations can be effectively enumerated and in which typability corresponds
to AST. As a consequence, AST can be checked by providing infinitely many type derivations forthe term at hand, each certifying that it normalizes with probability at least 1 − ε, this of course
for arbitrary small ε. Completeness is achieved for both CBN and CBV evaluation, and in two
different flavours, namely by way of oracle intersection types and monadic intersection types. In
both cases, however, intersection is idempotent.
Almost sure termination is however not the only possible notion of termination in a probabilistic
setting. In particular, it is well possible that a probabilistic process terminates with probability
1, but the expected number of steps to termination is infinite. As an example, the symmetricrandom walk on the natural numbers is well-known to be AST, but the journey from 1 to 0 takes,
on average, infinite times. Requiring the latter value to be finite corresponds to the so-called
positive almost sure termination constraint (PAST in the following), a more restrictive criterion
which however is itself not recursively enumerable.
In this talk, we show that injecting non-idempotency in monadic intersection types allows us tocharacterize both AST and PAST within the same intersection type system, this way matching therecursion-theoretic nature of the two notions above. This is done in presence of CBN evaluation,and requires not only dropping idempotency, but also the use of scaling.

References[1] B. Accattoli, S. Graham-Lengrand, and D. Kesner. Tight typings and split bounds. PACMPL,
2(ICFP):94:1–94:30, 2018.
[2] B. Accattoli, G. Guerrieri, and M. Leberle. Types by need. In Programming Languages andSystems - 28th European Symposium on Programming, ESOP 2019,, pages 410–439, 2019.
[3] A. Bernadet and S. Lengrand. Complexity of strongly normalising λ-terms via non-idempotent
intersection types. In Proc. of FOSSACS 2011, pages 88–107, 2011.
∗ University of Bologna and INRIA† CNRS‡ University of Torino1[4] F. Breuvart and U. Dal Lago. On intersection types and probabilistic lambda calculi. In Proc.
of PPDP 2018, pages 8:1–8:13, 2018.
[5] U. Dal Lago and M. Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO- Theor. Inf. and Applic., 46(3):413–450, 2012.
[6] D. de Carvalho. Execution time of λ-terms via denotational semantics and intersection types.
Mathematical Structures in Computer Science, 28(7):1169–1203, 2018.
[7] C. Jones and G. D. Plotkin. A probabilistic powerdomain of evaluations. In Proc. of LICS
1989, pages 186–195, 1989.
[8] B. L. Kaminski, J. Katoen, and C. Matheja. On the hardness of analyzing probabilistic
programs. Acta Inf., 56(3):255–285, 2019.

2

Exploiting the power of intersection types in Java
(Extended Abstract)
Mariangiola Dezani-Ciancaglini, Paola Giannini, Betti Venneri
Dipartimento di Informatica, Università di Torino, Italy
DiSIT, Università del Piemonte Orientale, Alessandria, Italy
Dipartimento di Statistica, Informatica, Applicazioni, Università di Firenze, Italy

Intersection types have been introduced originally for the λ -calculus to increase the set of terms
having meaningful types [1], Part III. The typability power of intersection types is essentially due to thepossibility of giving intersection types to the arguments of functions. In a programming language thiscorresponds to allowing the types of input parameters and output results to be intersection types. In an
object-oriented language also the types of fields should be intersection types. In [3], Büchi and Weckproposed to extend Java 1 by allowing intersection types (called compound types) as parameter types,
variable types, return types of methods, and cast operators. They justify intersection types by means ofan interesting example. (Here we use a simplified version of this example.) Java 8 has intersection types,
but their use in writing code is limited to type casts and bounds of generic type variables. Java 8 allows
a generic type variable bound by an intersection type as a parameter type, a variable type and a return
type of a method. In some cases intersection types can be simulated by the use of generics bounded byintersections. Consider the following example where the type of field intField in line 10 and the return
type of method sum in line 15 are meant to be intersection types:
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

i n t e r f a c e I I n t { i n t opI ( i n t x , i n t y ) ; }i n t e r f a c e I D o u b l e { d o u b l e opD ( d o u b l e x , d o u b l e y ) ; }c l a s s IntIDouble implements I I n t , IDouble {p u b l i c d o u b l e opD ( d o u b l e x , d o u b l e y ) { r e t u r n x + y ; }p u b l i c i n t opI ( i n t x , i n t y ) { r e t u r n x + y ;}}c l a s s U s e I n t e r s e c t i o n <T1 e x t e n d s I I n t &I D o u b l e > {T1 i n t F i e l d ;U s e I n t e r s e c t i o n ( T1 i n t F i e l d ) {super () ;this . intField=intField ;}<T2 e x t e n d s I I n t &I D o u b l e > T2 sum ( ) {r e t u r n ( T2 ) new U s e I n t e r s e c t i o n ( new I n t I D o u b l e ( ) ) . i n t F i e l d ;}}In Java 8 λ -expressions are poly expressions, i.e. they can have various types according to the context
requirements. More specifically, the contexts must prescribe target types for λ -expressions: indeed, Java
code does not compile when λ -expressions come without target types. A target type can be either afunctional interface (i.e., an interface with a single abstract method) or an intersection of interfaces thatinduces a functional interface. Notably the abstract method header must have a type derivable for the
λ -expression. The target type cannot be a generic type variable. This ban is needed since the variable
could be instantiated by a class or by an interface with an abstract method header which cannot be used
to type the λ -expression. As a result only the λ -expressions which are casted to intersection types in the
Submitted to:
ITRS 2020c Dezani-Ciancaglini, Giannini and Venneri
This work is licensed under theCreative Commons Attribution License.

2Intersection Types in Java

user code have target types which are intersection types. If we now define the class UseIntersection withthe method sum as follows<T2 e x t e n d s I I n t &I D o u b l e > T2 sum ( ) {r e t u r n ( T2 ) new U s e I n t e r s e c t i o n ( ( x , y )−>x+y ) . i n t F i e l d ;the code is well typed in Java. So the λ -expression (x,y)−>x+y implements both interfaces. However,this λ -expression cannot be returned by method sum, since λ -expressions in Java may be typed only byfunctional interfaces, i.e., intersections of interfaces with a single abstract method. In our example IInt
&IDouble specifies two abstract methods. However, even if we remove the method opD from the interface
IDouble, obtaining the functional type IInt &IDouble, the generic variable T2 is still not a functional type.
This is needed for safety, since extending IInt &IDouble more methods could be added and/or a class could
be obtained. Line 12 of the following code produces a compilation error in Java, since even though(x, y) −> x + y has type IInt &IDouble, still the interface T2 is not a functional interface, so cannot be thetarget type of a λ -expression.
1
2
3
4
5
6
7
8
9
10
11
12
13
14

i n t e r f a c e I I n t { i n t opI ( i n t x , i n t y ) ; }i n t e r f a c e IDouble { }c l a s s U s e I n t e r s e c t i o n <T1 e x t e n d s I I n t & I D o u b l e > {T1 i n t F i e l d ;U s e I n t e r s e c t i o n ( T1 i n t F i e l d ) {super () ;this . intField=intField ;}<T2 e x t e n d s I I n t & I D o u b l e > T2 q ( ) {r e t u r n ( T2 ) ( x , y ) −> x + y ; / / ERROR}}

In [4] we proposed to go back to [3] and allow intersection types as parameter types of constructors andmethods and as return types of methods and allow target type for a λ -expression to have an arbitrary number of abstract methods, proviso that all the method headers have types derivable for the λ -expression.
This proposal is formalised trough the calculus FJP&λ (Featherweight Java with polymorphic intersection types and λ -expressions). As expected FJP&λ enjoys subject reduction and progress.
In the current paper we show the meaningfulness of FJP&λ , by providing examples in which the useof intersection enhance the expressive power of the language. For instance, the Interface Segregation
Principle prescribes to keep Interfaces as tiny as possible, in order to avoid interface pollution. On theother hand, in other cases we need to deal with objects implementing several Interfaces. The introductionof intersection types in Java has been a crucial step in this direction, allowing to segregate different methods in separated interfaces, while combining interfaces in the type of objects when needed. However, wecannot explicitly assign an intersection type to a variable. In such cases, a partial solution could be touse the var-mechanism, the new feature introduced in Java 10 for the definition of variables whose typeis omitted and is inferred by the local type inference. Unfortunately, this solution does not work in the
crucial case of λ -expressions, that need to have explicit target types. By discussing significant use cases,
we will show that Java restrictions on intersection types result in critical drawbacks for programmingwith functions and, more in general, for a clean code design. Finally, concerning the feasibility of our
proposal, we will discuss the compiling of FJP&λ typed programs into FJ&λ . FJ&λ is a core calculusthat extends Featherweight Java with interfaces, supporting multiple inheritance in a restricted form, λ expressions, and intersection types, see [2]. FJ&λ was introduced to give a faithful formalisation of thestatic and dynamic semantics of Java 8.

Dezani-Ciancaglini, Giannini and Venneri

3

References[1] Henk Barendregt, Wil Dekkers & Richard Statman (2013): Lambda Calculus with Types. Perspectives in
Logic, Cambridge.
[2] Lorenzo Bettini, Viviana Bono, Mariangiola Dezani-Ciancaglini, Paola Giannini & Betti Venneri (2018): Java
& Lambda: a Featherweight Story. Logical Methods in Computer Science 14(3). Available at https://arxiv.org/pdf/1801.05052.pdf.
[3] Martin Büchi & Wolfgang Weck (1998): Compound Types for Java. In Bjørn N. Freeman-Benson & Craig
Chambers, editors: OOPSLA, ACM, pp. 362–373.
[4] Mariangiola Dezani-Ciancaglini, Paola Giannini & Betti Venneri (2018): Intersection Types in Java: back to
the future. In Tiziana Margaria, Susanne Graf & Kim G Larsen, editors: Models, Mindsets, Meta: The What,
the How, and the Why Not?, LNCS 11200, Springer, pp. 68–86.