Interaction Improvement

Adrienne Lancelot; Gabriele Vanoni; Giulio Manzonetto; Guy McCusker

arxiv: 2601.01638 · v2 · submitted 2026-01-04 · 💻 cs.LO · cs.PL

Interaction Improvement

Adrienne Lancelot , Giulio Manzonetto , Guy McCusker , Gabriele Vanoni This is my paper

Pith reviewed 2026-05-16 17:45 UTC · model grok-4.3

classification 💻 cs.LO cs.PL

keywords relational semanticslinear logiclambda calculuscontextual preordercheckers calculusquantitative semanticsinteraction counting

0 comments

The pith

Relational semantics of linear logic refines contextual preorders on lambda terms by limiting the number of interactions with contexts.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows how the checkers calculus supplies a quantitative and contextual reading of the preorder induced by the relational model of linear logic. This reading makes the preorder sensitive to the actual number of interactions that related terms can have with an arbitrary context. A sympathetic reader cares because standard interpretations of relational semantics only recover qualitative comparisons up to extensional Bohm trees, leaving resource usage invisible in the induced ordering. The new interpretation therefore turns the model into one that actually constrains observable interaction counts.

Core claim

The relational semantics refines the contextual preorder constraining the number of interactions between the related terms and the context. This refinement is obtained by employing the checkers calculus to give the preorder a quantitative and contextual interpretation.

What carries the argument

The checkers calculus, which supplies a faithful quantitative and contextual interpretation of the preorder induced by the relational model of linear logic.

If this is right

The preorder on terms now distinguishes behaviors according to concrete interaction counts with contexts.
Equational theories derived from the relational model become sensitive to resource-bounded interaction limits.
Contextual equivalence in the presence of the relational model must respect matching interaction budgets.
Quantitative aspects of linear logic models are reflected directly in the induced preorders rather than only in the model itself.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same technique might be used to add interaction counting to other relational or game-based models of computation.
Program equivalence checkers could exploit the refined preorder for more precise resource-aware optimizations.
Extensions to typed settings or probabilistic variants of the relational semantics may follow similar checkers-based routes.

Load-bearing premise

The checkers calculus supplies a faithful quantitative and contextual interpretation of the preorder induced by the relational model of linear logic.

What would settle it

Two lambda terms that the relational semantics orders one way yet require observably different numbers of interactions with some context under the checkers calculus.

Figures

Figures reproduced from arXiv: 2601.01638 by Adrienne Lancelot, Gabriele Vanoni, Giulio Manzonetto, Guy McCusker.

**Figure 1.** Figure 1: The operational semantics of the checkers calculus. (iii) The contextual closure of a binary relation R on Λ◦• is the least relation C◦•⟨R⟩ such that t C◦•⟨R⟩ u entails C⟨t⟩ C◦•⟨R⟩ C⟨u⟩, for all C ∈ C◦•. Its head-contextual closure H◦•⟨R⟩ is defined analogously, by taking C ∈ H◦•. There are two kinds of colored β-redexes (λcx.t) · d u, the silent ones and the interaction ones. Silent redexes are β-redexes … view at source ↗

**Figure 2.** Figure 2: Checkers multi type system ⊢ . Example 2. Consider I• and D◦ from Example 1, and 1• from Remark 1. – Since Ω := (λx.xx)(λy.yy) has no hnf, any of its colorings will be a bottom element w.r.t. ⊑int and ⊑ imp. E.g. Ω • ⊑int I• and Ω ◦ ⊑int 1•. – More generally, t ≡int u holds whenever t, u ∈ Λ◦• have no h◦•-nf. – To see that λ◦x.x ̸⊑ imp λ•x.x, just take the context C := ⟨·⟩ • I•. Indeed, C⟨λ◦x.x⟩ ⇓ 1 h◦• wh… view at source ↗

**Figure 3.** Figure 3: Polarized whitening of a type. Definition 9 (Polarized Whitening). (i) Given a polarity p ∈ {+, −} we denote by ¬p the opposite polarity. (ii) For all k ∈ N, define T ′ ≤ + k T and T ′ ≤ − k T by mutual induction in [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

read the original abstract

The relational semantics of linear logic is a powerful framework for defining resource-aware models of the $\lambda$-calculus. However, its quantitative aspects are not reflected in the preorders and equational theories induced by these models. Indeed, they can be characterized in terms of (in)equalities between B\"ohm trees up to extensionality, which are qualitative in nature. We employ the recently introduced checkers calculus to provide a quantitative and contextual interpretation of the preorder associated to the relational semantics. This way, we show that the relational semantics refines the contextual preorder constraining the number of interactions between the related terms and the context.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper uses checkers calculus to quantify the relational preorder via interaction counts, which is new but rests on an unverified faithfulness claim.

read the letter

The main takeaway is that this work applies the checkers calculus to recover the relational preorder as a bound on the number of interactions between terms and contexts. That moves the characterization beyond the usual qualitative Böhm-tree comparison and supplies a resource-sensitive reading of the preorder induced by the relational model of linear logic. If the details check out, it gives a concrete way to talk about how much one term can interact with another under the preorder. The authors do a clean job setting up the background on relational semantics and explaining why the standard equational theory stays qualitative. The connection to checkers feels like a natural next step for anyone already tracking resource models in this subfield. The soft spot is the faithfulness of the interpretation. The central claim requires that checkers reduction rules line up exactly with the relational model's resource counting across arbitrary contexts, so that every relational inequality produces a matching interaction bound and no extras appear. The abstract states the refinement but gives no proof sketch, commuting diagram, or induction outline, so the body must supply that argument explicitly. Without it the result only holds in restricted cases. No circular definitions or free parameters show up in the description, and the citations track the relevant prior work on relational models and checkers without obvious omissions. This paper is for readers who already know the relational semantics and the checkers calculus. Someone working on quantitative denotational models or resource-aware lambda calculus will find the refinement useful if the proofs hold. It deserves a serious referee because the claim is specific and falsifiable once the translation is written out, even if revisions are needed to close the faithfulness gap.

Referee Report

1 major / 0 minor

Summary. The paper claims that the relational semantics of linear logic, while inducing only qualitative preorders characterized by Böhm trees up to extensionality, can be given a quantitative and contextual interpretation via the checkers calculus. This interpretation is used to show that the relational semantics refines the contextual preorder by constraining the number of interactions between related terms and contexts.

Significance. If the faithfulness of the checkers calculus to the relational preorder holds for arbitrary contexts, the result would usefully connect qualitative relational models with explicit quantitative bounds on interaction counts. This could strengthen resource-aware reasoning in the lambda-calculus and linear logic, particularly if the checkers reduction rules are shown to match the relational resource counting exactly.

major comments (1)

[Abstract] Abstract: the central refinement claim (that relational inequalities imply bounds on interaction counts in every context) rests on the unshown assumption that the checkers calculus supplies a faithful quantitative interpretation of the relational preorder. No proof sketch, commuting diagram, or explicit translation between the two semantics is supplied, so the load-bearing step cannot be verified from the given material.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the careful reading and for highlighting the need for greater explicitness in connecting the checkers calculus to the relational preorder. We address the single major comment below and outline the revisions we will make.

read point-by-point responses

Referee: [Abstract] Abstract: the central refinement claim (that relational inequalities imply bounds on interaction counts in every context) rests on the unshown assumption that the checkers calculus supplies a faithful quantitative interpretation of the relational preorder. No proof sketch, commuting diagram, or explicit translation between the two semantics is supplied, so the load-bearing step cannot be verified from the given material.

Authors: We accept the observation that the abstract states the refinement result without an accompanying proof outline. The body of the manuscript defines the checkers calculus (Section 2), proves that its interaction counts coincide with the relational resource measures (Lemma 3.4), and establishes the contextual faithfulness result for arbitrary contexts (Theorem 4.1). To improve verifiability we will (i) expand the abstract with a one-sentence proof sketch, (ii) insert a commuting-diagram figure in the introduction, and (iii) add a short paragraph in Section 4 that explicitly translates relational inequalities into checkers reduction sequences. These changes make the load-bearing step directly inspectable without altering any theorems. revision: yes

Circularity Check

0 steps flagged

Minor self-citation to checkers calculus; central refinement claim remains independent

full rationale

The paper invokes the recently introduced checkers calculus as an external quantitative tool to interpret the relational preorder and derive the interaction-count refinement. No equations in the abstract or described derivation reduce the target result to a fitted parameter, self-definition, or unverified self-citation chain; the checkers rules are treated as given prior machinery whose faithfulness is assumed rather than constructed inside this work. The derivation therefore stays self-contained against external benchmarks and receives only a low score for the routine citation of prior work.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The abstract relies on the standard characterization of relational semantics via Böhm trees up to extensionality and on the correctness of the recently introduced checkers calculus; no free parameters or invented entities are mentioned.

axioms (1)

domain assumption The preorder induced by relational semantics of linear logic is characterized by inequalities between Böhm trees up to extensionality.
Stated directly in the abstract as the qualitative nature of existing models.

pith-pipeline@v0.9.0 · 5395 in / 1099 out tokens · 30829 ms · 2026-05-16T17:45:30.133700+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

57 extracted references · 57 canonical work pages

[1]

Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000). https://doi.org/10.1006/INCO.2000.2930

work page doi:10.1006/inco.2000.2930 2000
[2]

Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993). https://doi.org/10.1006/INCO.1993.1044

work page doi:10.1006/inco.1993.1044 1993
[3]

Accattoli, B., Dal Lago, U., Vanoni, G.: Multi types and reasonable space. Proc. ACM Program. Lang.6(ICFP), 799–825 (2022). https://doi.org/10.1145/3547650

work page doi:10.1145/3547650 2022
[4]

Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds, fully developed. J. Funct. Program.30, e14 (2020). https://doi.org/10.1017/ S095679682000012X

work page 2020
[5]

Accattoli, B., Lancelot, A., Manzonetto, G., Vanoni, G.: Interaction equivalence. Proc. ACM Program. Lang.9(POPL) (Jan 2025). https://doi.org/10.1145/3704891, https://doi.org/10.1145/3704891

work page doi:10.1145/3704891 2025
[6]

In: Bojanczyk, M., Simpson, A

Alcolei, A., Clairambault, P., Laurent, O.: Resource-tracking concurrent games. In: Bojanczyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Soft- ware, ETAPS 2019, Prague, Czech Republic, April 6-11, ...

work page doi:10.1007/978-3-030-17127-8_2 2019
[7]

Barendregt, H.: The Lambda Calculus – Its Syntax and Semantics, Studies in logic and the foundations of mathematics, vol. 103. North-Holland (1984)

work page 1984
[8]

Research Report RR-0080, INRIA (1981), https://inria.hal.science/inria-00076481

Berry, G.: Some syntactic and categorical constructions of lambda-calculus models. Research Report RR-0080, INRIA (1981), https://inria.hal.science/inria-00076481

work page 1981
[9]

In: Bojanczyk, M., Simpson, A

Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normal-form bisimilarity for state. In: Bojanczyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April...

work page doi:10.1007/978-3-030-17127-8_6 2019
[10]

In: Ariola, Z.M

Biernacki, D., Lenglet, S., Polesiuk, P.: A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 7:1–7:22. Schloss Dagstuhl–Leibniz-Zentrum für Informa...

work page doi:10.4230/lipics.fscd.2020.7 2020
[11]

Electronic Notes in Theoretical Computer Science336, 41– 56 (2018)

Biernacki, D., Lenglet, S., Polesiuk, P.: Proving soundness of extensional normal- form bisimilarities. Electronic Notes in Theoretical Computer Science336, 41– 56 (2018). https://doi.org/https://doi.org/10.1016/j.entcs.2018.03.015, https:// www.sciencedirect.com/science/article/pii/S1571066118300185, the Thirty-third Conference on the Mathematical Founda...

work page doi:10.1016/j.entcs.2018.03.015 2018
[12]

Breuvart, F., Manzonetto, G., Ruoppolo, D.: Relational graph models at work. Log. Methods Comput. Sci.14(3) (2018). https://doi.org/10.23638/LMCS-14(3:2)2018, https://doi.org/10.23638/LMCS-14(3:2)2018

work page doi:10.23638/lmcs-14(3:2)2018 2018
[13]

In: Duparc, J., Henzinger, T.A

Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Not enough points is enough. In: Duparc, J., Henzinger, T.A. (eds.) Computer Science Logic, 21st International Interaction Improvement 21 Workshop,CSL2007,16thAnnualConferenceoftheEACSL,Lausanne,Switzerland, September 11-15, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4646, pp. 298–312. Springer...

work page doi:10.1007/978-3-540-74915-8_24 2007
[14]

Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL25(4), 431–464 (2017). https://doi.org/10.1093/ JIGPAL/JZX018

work page 2017
[15]

Thèse de doctorat, Université Aix-Marseille II (2007)

de Carvalho, D.: Sémantiques de la logique linéaire et temps de calcul. Thèse de doctorat, Université Aix-Marseille II (2007)

work page 2007
[16]

de Carvalho, D.: Execution time ofλ-terms via denotational semantics and in- tersection types. Math. Struct. Comput. Sci.28(7), 1169–1203 (2018). https: //doi.org/10.1017/S0960129516000396

work page doi:10.1017/s0960129516000396 2018
[17]

Habilitation à diriger des recherches, Aix-Marseille Université, Marseille, France (2024), https: //tel.archives-ouvertes.fr/tel-04523273

Clairambault, P.: Causal Investigations in Interactive Semantics. Habilitation à diriger des recherches, Aix-Marseille Université, Marseille, France (2024), https: //tel.archives-ouvertes.fr/tel-04523273

work page 2024
[18]

In: ESOP 2019 - European Symposium on Programming

Dal Lago, U., Gavazzo, F.: Effectful Normal Form Bisimulation. In: ESOP 2019 - European Symposium on Programming. Prague, Czech Republic (Apr 2019), https://hal.inria.fr/hal-02386004

work page 2019
[19]

In: Kamin- ski, M., Martini, S

Dal Lago, U., Laurent, O.: Quantitative game semantics for linear logic. In: Kamin- ski, M., Martini, S. (eds.) Computer Science Logic. pp. 230–245. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)

work page 2008
[20]

Ehrhard, T., Pagani, M., Tasson, C.: Full abstraction for probabilistic PCF. J. ACM65(4), 23:1–23:44 (2018). https://doi.org/10.1145/3164540, https://doi.org/ 10.1145/3164540

work page doi:10.1145/3164540 2018
[21]

Springer, Berlin, Heidelberg (2007)

Fokkink, W.J.: Modelling Distributed Systems. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-49321-0

work page doi:10.1007/978-3-540-49321-0 2007
[22]

In: Palsberg, J., Abadi, M

Ghica, D.R.: Slot games: a quantitative model of computation. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. pp. 85–97. ACM (2005). https://doi.org/10.1145/1040305. 1040313

work page doi:10.1145/1040305 2005
[23]

Howe, D.J.: Proving congruence of bisimulation in functional programming lan- guages. Inf. Comput.124(2), 103–112 (1996). https://doi.org/10.1006/inco.1996. 0008, https://doi.org/10.1006/inco.1996.0008

work page doi:10.1006/inco.1996 1996
[24]

Journal of the London Mathematical Societys2-12(3), 361–370 (1976)

Hyland, M.: A syntactic characterization of the equality in some models for the lambda calculus. Journal of the London Mathematical Societys2-12(3), 361–370 (1976). https://doi.org/https://doi.org/10.1112/jlms/s2-12.3.361

work page doi:10.1112/jlms/s2-12.3.361 1976
[25]

In: Seda, A.K., Hurley, T., Schellekens, M.P., an Airchinnigh, M.M., Strong, G

Hyland, M., Nagayama, M., Power, J., Rosolini, G.: A category theoretic formu- lation for engeler-style models of the untyped lambda. In: Seda, A.K., Hurley, T., Schellekens, M.P., an Airchinnigh, M.M., Strong, G. (eds.) Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2004, D...

work page doi:10.1016/j.entcs.2006.04.024 2004
[26]

Hyland, M., Ong, C.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000). https://doi.org/10.1006/INCO.2000.2917

work page doi:10.1006/inco.2000.2917 2000
[27]

Ker, A.D., Nickau, H., Ong, C.L.: Innocent game models of untyped lambda- calculus. Theor. Comput. Sci.272(1-2), 247–292 (2002). https://doi.org/10.1016/ S0304-3975(00)00353-4, https://doi.org/10.1016/S0304-3975(00)00353-4 22 A. Lancelot, G. Manzonetto, G. McCusker, G. Vanoni

work page doi:10.1016/s0304-3975(00)00353-4 2002
[28]

Ker, A.D., Nickau, H., Ong, C.L.: Adapting innocent game models for the böhm tree λ-theory. Theor. Comput. Sci.308(1-3), 333–366 (2003). https://doi.org/10. 1016/S0304-3975(02)00849-6

work page 2003
[29]

In: Proceedings of LICS

Koutavas, V., Lin, Y.Y., Tzevelekos, N.: Fully abstract normal form bisimulation for call-by-value pcf. In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–13 (2023). https://doi.org/10.1109/LICS56636. 2023.10175778

work page doi:10.1109/lics56636 2023
[30]

https://doi.org/10.1016/S1571-0661(04)80083-5

Lassen, S.B.: Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context20, 346–374 (1999). https://doi.org/10.1016/S1571-0661(04)80083-5

work page doi:10.1016/s1571-0661(04)80083-5 1999
[31]

Levy, P.B., Staton, S.: Transition systems over games. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2603...

work page doi:10.1145/2603088.2603150 2014
[32]

Morris, J.H.: Lambda-calculus Models of Programming Languages. Ph.D. thesis, Massachusetts Institute of Technology (1968), https://books.google.is/books?id= DklAAQAAIAAJ

work page 1968
[33]

Paolini, L., Piccolo, M., Ronchi Della Rocca, S.: Essential and relational mod- els. Math. Struct. Comput. Sci.27(5), 626–650 (2017). https://doi.org/10.1017/ S0960129515000316, https://doi.org/10.1017/S0960129515000316

work page doi:10.1017/s0960129515000316 2017
[34]

ACM Comput

Patrignani, M., Ahmed, A., Clarke, D.: Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput. Surv.51(6), 125:1–125:36 (2019). https://doi.org/10.1145/3280984

work page doi:10.1145/3280984 2019
[35]

In: Sangiorgi, D., Rutten, J.J.M.M

Pitts, A.M.: Howe’s method for higher-order languages. In: Sangiorgi, D., Rutten, J.J.M.M. (eds.) Advanced Topics in Bisimulation and Coinduction, Cambridge tracts in theoretical computer science, vol. 52, pp. 197–232. Cambridge University Press (2012). https://doi.org/10.1017/CBO9780511792588.006

work page doi:10.1017/cbo9780511792588.006 2012
[36]

Plotkin, G.D.: A powerdomain construction. SIAM J. Comput.5(3), 452–487 (1976). https://doi.org/10.1137/0205035, https://doi.org/10.1137/0205035

work page doi:10.1137/0205035 1976
[37]

Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977). https://doi.org/10.1016/0304-3975(77)90044-5

work page doi:10.1016/0304-3975(77)90044-5 1977
[38]

Ronchi Della Rocca, S.: Characterization theorems for a filter lambda model. Inf. Control.54(3), 201–216 (1982). https://doi.org/10.1016/S0019-9958(82)80022-3, https://doi.org/10.1016/S0019-9958(82)80022-3

work page doi:10.1016/s0019-9958(82)80022-3 1982
[39]

Sands, D.: Proving the correctness of recursion-based automatic program transfor- mations. Theor. Comput. Sci.167(1&2), 193–233 (1996). https://doi.org/10.1016/ 0304-3975(96)00074-6

work page 1996
[40]

ACM Trans

Sands,D.:Totalcorrectnessbylocalimprovementinthetransformationoffunctional programs. ACM Trans. Program. Lang. Syst.18(2), 175–234 (mar 1996). https: //doi.org/10.1145/227699.227716

work page doi:10.1145/227699.227716 1996
[41]

Sands, D.: Improvement theory and its applications, p. 275–306. Cambridge Uni- versity Press, USA (1999)

work page 1999
[42]

21: Proceedings of the Symposium on Computers and Automata

Scott,D.,Strachey,C.:Towardamathematicalsemanticsforcomputerlanguages.In: MRI Symposium Proceedings, vol. 21: Proceedings of the Symposium on Computers and Automata. pp. 19–46. Fox, J. (Ed.). Polytechnic Press, Polytechnic Institute of Brooklyn, New York (1971)

work page 1971
[43]

In: Proc

Støvring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequen- tial control and state. In: Proc. 34th Annual ACM Symposium on Principles of Programming Languages. pp. 161–172. Nice, France (2007), http://doi.acm.org/10. 1145/1190215.1190244 Interaction Improvement 23

work page arXiv 2007
[44]

Wadsworth, C.P.: The Relation Between Computational and Denotational Prop- erties for Scott’sD∞-Models of the Lambda-Calculus. SIAM J. Comput.5(3), 488–521 (1976). https://doi.org/10.1137/0205036 24 A. Lancelot, G. Manzonetto, G. McCusker, G. Vanoni A Proofs of Section 3 Lemma 7(Splitting multisets with respect to derivations).Let t be a term, π▷Γ⊢ k t :M...

work page doi:10.1137/0205036 1976
[45]

Linear types,i.e.T :=L. Cases of the last derivation rule: (a)Unsubstituted variable,i.e.: π= x:0, y: [L]⊢ 0 y:L ax Then asM=0,σmust be of the following shape: ∆⊢ 0 u:0 many Hence π′ := π works, asy{x:=u} = y and k′ = 0. Clearly,|π|@ = |π′|@ = 0, as required. (b)Substituted variable,i.e.: π= x: [L]⊢ 0 x:L ax Then, asM= [L],σmust be of the following shape:...

work page
[46]

The last rule of the derivation must bemany: (πi ▷Γ i, x:M i ⊢li t:L i)i∈I ⊎i∈I Γi, x:M⊢ P i∈I li t: [Li]i∈I many withM=⊎ i∈I Mi andk= P i∈I li and⊎ i∈I Γi =Γ

Multi types,i.e.T := [L i]i∈I with I finite. The last rule of the derivation must bemany: (πi ▷Γ i, x:M i ⊢li t:L i)i∈I ⊎i∈I Γi, x:M⊢ P i∈I li t: [Li]i∈I many withM=⊎ i∈I Mi andk= P i∈I li and⊎ i∈I Γi =Γ. By the multiset splitting lemma (Lemma 7), the derivationσ for u in the hypotheses splits in several derivations of final judgmentsσi ▷∆ i ⊢k′ i u :M i ...

work page
[47]

Linear types,i.e.T :=L. Cases of the last derivation rule: (a)Unsubstituted variable,i.e.:y{x:=u}=yand π= y: [L]⊢ 0 y:L ax Then, takingM :=0,π u must be of the following shape: ∆⊢ 0 u:0 many Henceπ t :=πworks. (b) Substituted variable,i.e.: x{x:=u} = u and π▷∆⊢ k′ u :L. We take M := [L]. Then: π▷∆⊢ k′ u:L πu ▷∆⊢ k′ u: [L] and πt =x: [L]⊢ 0 x:L ax (c)Abstr...

work page
[48]

Multi types,i.e.T := [L i]i∈I with I finite. The last rule of the derivation must bemany: (π′ i ▷ Γi ∪∆ i ⊢ki+k′ i t{x:=u}:L i)i∈I ⊎i∈I Γi ∪∆ i ⊢ P i∈I (ki+k′ i) t{x:=u}: [L i]i∈I many By applying thei.h., we obtain for eachi∈I : πi ▷Γ i, x :M i ⊢ki t :L i and σi ▷∆ i ⊢k′ i u :M i. πu is obtaining by merging theσi (Lemma 9). πt is as follows: (πi ▷ Γi, x:...

work page
[49]

Moreover: (i) ift→ h t′ thenk ′ =k−1; (ii) otherwise, ift→ hτ t′ thenk ′ =k

Quantitative subject reduction: ifπ ▷ Γ⊢ k t :Lthen there is a derivation π′ ▷ Γ⊢ k′ t′ :Lsuch that|π ′|@ =|π| @ −1. Moreover: (i) ift→ h t′ thenk ′ =k−1; (ii) otherwise, ift→ hτ t′ thenk ′ =k

work page
[50]

Subject expansion: if π′ ▷ Γ⊢ k′ t′ :Lthen there is a derivation π ▷ Γ⊢ k t :L. Proof

work page
[51]

Then the last rule of the derivationπis@and is followed by theλrule on the left: Γ, x:M⊢ k1 s:L Γ⊢ k1 λc x.s:M c − →L∆⊢ k2 u:M Γ⊎∆⊢ k (λc x.s)· d u:L @ wherek=k 1 +k 2 +δ ⊥ c,d

(a)Root step,i.e.t= (λ c x.s)· d u→ h◦• s{x:=u}=t ′. Then the last rule of the derivationπis@and is followed by theλrule on the left: Γ, x:M⊢ k1 s:L Γ⊢ k1 λc x.s:M c − →L∆⊢ k2 u:M Γ⊎∆⊢ k (λc x.s)· d u:L @ wherek=k 1 +k 2 +δ ⊥ c,d. By the Substitution Lemma 8, we have that there exists a derivation π′ ▷Γ⊎∆⊢ k1+k2 s{x:=r} :Lsuch that |π′|@ = |πs|@ + |πu|@ =...

work page
[52]

By the Anti-Substitution Lemma 10, there existσ▷Γ ′, x :M ⊢k1 s :L andρ▷Γ ′′ ⊢k2 u:Msuch thatΓ=Γ ′ ⊎Γ ′′ andk=k 1 +k 2

(a)Root step,i.e.t= (λ c x.s)· d u7→ βτ s{x:=u}=t ′. By the Anti-Substitution Lemma 10, there existσ▷Γ ′, x :M ⊢k1 s :L andρ▷Γ ′′ ⊢k2 u:Msuch thatΓ=Γ ′ ⊎Γ ′′ andk=k 1 +k 2. Then we can build the type derivationπ▷Γ⊢ k′ t:Las follows: σ▷Γ ′, x:M⊢ k1 s:L Γ ′ ⊢k1 λc x.s:M c − →Lρ▷Γ ′′ ⊢k2 u:M Γ ′ ⊎Γ ′′ ⊢k′ (λc x.s)· d u:L @ wherek ′ =k+δ ⊥ c,d. (b)Contextual ...

work page
[53]

Ift is head normal then t is head normalizable in0 ≤k interaction steps

By induction on|π| and case analysis on whethert is head normal. Ift is head normal then t is head normalizable in0 ≤k interaction steps. Ift→ h◦• u then there two cases: –t→ hτ u. Then by quantitative subject reduction (Prop. 1(1)), there is σ▷Γ⊢ k u :Lsuch that |π|@ = |σ|@ + 1. By i.h.,u is head normalizable in less thankinteraction steps. Then, the sam...

work page
[54]

By induction onm

We have thatt→ m h◦• h, where h is a head normal form. By induction onm. Cases: 30 A. Lancelot, G. Manzonetto, G. McCusker, G. Vanoni (a) Ifm= 0, thent=h. Then we conclude by Proposition 6. (b) If m > 0, thent→ h◦• u→ m−1 h◦• h. Byi.h., there existsσ▷Γ⊢ k′′ u :Land u⇓ k′′ h◦• . By subject expansion (Prop. 1(2)), there existsπ▷Γ⊢ k′ t :L. By subject reduct...

work page
[55]

If Γ⊢ k t • :Lthen there existL ′, L′′ such that Γ = x : [L′],L ′′ ≤− k′ L′ and L′′ ≤+ k′′ Lwithk=k ′ +k ′′

work page
[56]

If Γ⊢ k t • :Mthen there existM ′, M′′ such that Γ = x : [M′],M ′′ ≤− k′ M′ and M′′ ≤+ k′′ Mwithk=k ′ +k ′′. Proof. We proceed by mutual induction and call HI1 and HI2 the corresponding induction hypotheses. More precisely, we prove (1) by induction on a derivation of Γ⊢ k t • :Land (2) on a derivation ofΓ⊢ k t • :M. Wlog we can considert to be in head no...

work page
[57]

This implies that there are d1, d2 such that d = d1 + d2 + δ⊥ c,c′ and ⟨Γ ′ 1, L′⟩ ≤ + d1 ⟨Γ1, L⟩ and Interaction Improvement 43 M′ ≤− d2 M

∈JuK with ⟨Γ ′ 1, M′ c′ − →L′⟩ ≤ + d ⟨Γ1, M c − →L⟩ and k1 ≥k ′ 1 + d. This implies that there are d1, d2 such that d = d1 + d2 + δ⊥ c,c′ and ⟨Γ ′ 1, L′⟩ ≤ + d1 ⟨Γ1, L⟩ and Interaction Improvement 43 M′ ≤− d2 M. By Proposition 3 there exists(Γ ′′ 1 + Γ ′ 2, L′′, m) ∈Ju· d sK with ⟨Γ ′′ 1 + Γ ′ 2, L′′⟩ ≤ + d′ ⟨Γ ′ 1 + Γ2, L′⟩ and m≤k ′ 1 + k2 + δ⊥ c′,d + d...

work page

[1] [1]

Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. Comput. 163(2), 409–470 (2000). https://doi.org/10.1006/INCO.2000.2930

work page doi:10.1006/inco.2000.2930 2000

[2] [2]

Abramsky, S., Ong, C.L.: Full abstraction in the lazy lambda calculus. Inf. Comput. 105(2), 159–267 (1993). https://doi.org/10.1006/INCO.1993.1044

work page doi:10.1006/inco.1993.1044 1993

[3] [3]

Accattoli, B., Dal Lago, U., Vanoni, G.: Multi types and reasonable space. Proc. ACM Program. Lang.6(ICFP), 799–825 (2022). https://doi.org/10.1145/3547650

work page doi:10.1145/3547650 2022

[4] [4]

Accattoli, B., Graham-Lengrand, S., Kesner, D.: Tight typings and split bounds, fully developed. J. Funct. Program.30, e14 (2020). https://doi.org/10.1017/ S095679682000012X

work page 2020

[5] [5]

Accattoli, B., Lancelot, A., Manzonetto, G., Vanoni, G.: Interaction equivalence. Proc. ACM Program. Lang.9(POPL) (Jan 2025). https://doi.org/10.1145/3704891, https://doi.org/10.1145/3704891

work page doi:10.1145/3704891 2025

[6] [6]

In: Bojanczyk, M., Simpson, A

Alcolei, A., Clairambault, P., Laurent, O.: Resource-tracking concurrent games. In: Bojanczyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Soft- ware, ETAPS 2019, Prague, Czech Republic, April 6-11, ...

work page doi:10.1007/978-3-030-17127-8_2 2019

[7] [7]

Barendregt, H.: The Lambda Calculus – Its Syntax and Semantics, Studies in logic and the foundations of mathematics, vol. 103. North-Holland (1984)

work page 1984

[8] [8]

Research Report RR-0080, INRIA (1981), https://inria.hal.science/inria-00076481

Berry, G.: Some syntactic and categorical constructions of lambda-calculus models. Research Report RR-0080, INRIA (1981), https://inria.hal.science/inria-00076481

work page 1981

[9] [9]

In: Bojanczyk, M., Simpson, A

Biernacki, D., Lenglet, S., Polesiuk, P.: A complete normal-form bisimilarity for state. In: Bojanczyk, M., Simpson, A. (eds.) Foundations of Software Science and Computation Structures - 22nd International Conference, FOSSACS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April...

work page doi:10.1007/978-3-030-17127-8_6 2019

[10] [10]

In: Ariola, Z.M

Biernacki, D., Lenglet, S., Polesiuk, P.: A Complete Normal-Form Bisimilarity for Algebraic Effects and Handlers. In: Ariola, Z.M. (ed.) 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), vol. 167, pp. 7:1–7:22. Schloss Dagstuhl–Leibniz-Zentrum für Informa...

work page doi:10.4230/lipics.fscd.2020.7 2020

[11] [11]

Electronic Notes in Theoretical Computer Science336, 41– 56 (2018)

Biernacki, D., Lenglet, S., Polesiuk, P.: Proving soundness of extensional normal- form bisimilarities. Electronic Notes in Theoretical Computer Science336, 41– 56 (2018). https://doi.org/https://doi.org/10.1016/j.entcs.2018.03.015, https:// www.sciencedirect.com/science/article/pii/S1571066118300185, the Thirty-third Conference on the Mathematical Founda...

work page doi:10.1016/j.entcs.2018.03.015 2018

[12] [12]

Breuvart, F., Manzonetto, G., Ruoppolo, D.: Relational graph models at work. Log. Methods Comput. Sci.14(3) (2018). https://doi.org/10.23638/LMCS-14(3:2)2018, https://doi.org/10.23638/LMCS-14(3:2)2018

work page doi:10.23638/lmcs-14(3:2)2018 2018

[13] [13]

In: Duparc, J., Henzinger, T.A

Bucciarelli, A., Ehrhard, T., Manzonetto, G.: Not enough points is enough. In: Duparc, J., Henzinger, T.A. (eds.) Computer Science Logic, 21st International Interaction Improvement 21 Workshop,CSL2007,16thAnnualConferenceoftheEACSL,Lausanne,Switzerland, September 11-15, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4646, pp. 298–312. Springer...

work page doi:10.1007/978-3-540-74915-8_24 2007

[14] [14]

Bucciarelli, A., Kesner, D., Ventura, D.: Non-idempotent intersection types for the lambda-calculus. Log. J. IGPL25(4), 431–464 (2017). https://doi.org/10.1093/ JIGPAL/JZX018

work page 2017

[15] [15]

Thèse de doctorat, Université Aix-Marseille II (2007)

de Carvalho, D.: Sémantiques de la logique linéaire et temps de calcul. Thèse de doctorat, Université Aix-Marseille II (2007)

work page 2007

[16] [16]

de Carvalho, D.: Execution time ofλ-terms via denotational semantics and in- tersection types. Math. Struct. Comput. Sci.28(7), 1169–1203 (2018). https: //doi.org/10.1017/S0960129516000396

work page doi:10.1017/s0960129516000396 2018

[17] [17]

Habilitation à diriger des recherches, Aix-Marseille Université, Marseille, France (2024), https: //tel.archives-ouvertes.fr/tel-04523273

Clairambault, P.: Causal Investigations in Interactive Semantics. Habilitation à diriger des recherches, Aix-Marseille Université, Marseille, France (2024), https: //tel.archives-ouvertes.fr/tel-04523273

work page 2024

[18] [18]

In: ESOP 2019 - European Symposium on Programming

Dal Lago, U., Gavazzo, F.: Effectful Normal Form Bisimulation. In: ESOP 2019 - European Symposium on Programming. Prague, Czech Republic (Apr 2019), https://hal.inria.fr/hal-02386004

work page 2019

[19] [19]

In: Kamin- ski, M., Martini, S

Dal Lago, U., Laurent, O.: Quantitative game semantics for linear logic. In: Kamin- ski, M., Martini, S. (eds.) Computer Science Logic. pp. 230–245. Springer Berlin Heidelberg, Berlin, Heidelberg (2008)

work page 2008

[20] [20]

Ehrhard, T., Pagani, M., Tasson, C.: Full abstraction for probabilistic PCF. J. ACM65(4), 23:1–23:44 (2018). https://doi.org/10.1145/3164540, https://doi.org/ 10.1145/3164540

work page doi:10.1145/3164540 2018

[21] [21]

Springer, Berlin, Heidelberg (2007)

Fokkink, W.J.: Modelling Distributed Systems. Springer, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-49321-0

work page doi:10.1007/978-3-540-49321-0 2007

[22] [22]

In: Palsberg, J., Abadi, M

Ghica, D.R.: Slot games: a quantitative model of computation. In: Palsberg, J., Abadi, M. (eds.) Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2005, Long Beach, California, USA, January 12-14, 2005. pp. 85–97. ACM (2005). https://doi.org/10.1145/1040305. 1040313

work page doi:10.1145/1040305 2005

[23] [23]

Howe, D.J.: Proving congruence of bisimulation in functional programming lan- guages. Inf. Comput.124(2), 103–112 (1996). https://doi.org/10.1006/inco.1996. 0008, https://doi.org/10.1006/inco.1996.0008

work page doi:10.1006/inco.1996 1996

[24] [24]

Journal of the London Mathematical Societys2-12(3), 361–370 (1976)

Hyland, M.: A syntactic characterization of the equality in some models for the lambda calculus. Journal of the London Mathematical Societys2-12(3), 361–370 (1976). https://doi.org/https://doi.org/10.1112/jlms/s2-12.3.361

work page doi:10.1112/jlms/s2-12.3.361 1976

[25] [25]

In: Seda, A.K., Hurley, T., Schellekens, M.P., an Airchinnigh, M.M., Strong, G

Hyland, M., Nagayama, M., Power, J., Rosolini, G.: A category theoretic formu- lation for engeler-style models of the untyped lambda. In: Seda, A.K., Hurley, T., Schellekens, M.P., an Airchinnigh, M.M., Strong, G. (eds.) Proceedings of the Third Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2004, D...

work page doi:10.1016/j.entcs.2006.04.024 2004

[26] [26]

Hyland, M., Ong, C.L.: On full abstraction for PCF: I, II, and III. Inf. Comput. 163(2), 285–408 (2000). https://doi.org/10.1006/INCO.2000.2917

work page doi:10.1006/inco.2000.2917 2000

[27] [27]

Ker, A.D., Nickau, H., Ong, C.L.: Innocent game models of untyped lambda- calculus. Theor. Comput. Sci.272(1-2), 247–292 (2002). https://doi.org/10.1016/ S0304-3975(00)00353-4, https://doi.org/10.1016/S0304-3975(00)00353-4 22 A. Lancelot, G. Manzonetto, G. McCusker, G. Vanoni

work page doi:10.1016/s0304-3975(00)00353-4 2002

[28] [28]

Ker, A.D., Nickau, H., Ong, C.L.: Adapting innocent game models for the böhm tree λ-theory. Theor. Comput. Sci.308(1-3), 333–366 (2003). https://doi.org/10. 1016/S0304-3975(02)00849-6

work page 2003

[29] [29]

In: Proceedings of LICS

Koutavas, V., Lin, Y.Y., Tzevelekos, N.: Fully abstract normal form bisimulation for call-by-value pcf. In: 2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–13 (2023). https://doi.org/10.1109/LICS56636. 2023.10175778

work page doi:10.1109/lics56636 2023

[30] [30]

https://doi.org/10.1016/S1571-0661(04)80083-5

Lassen, S.B.: Bisimulation in untyped lambda calculus: Böhm trees and bisimulation up to context20, 346–374 (1999). https://doi.org/10.1016/S1571-0661(04)80083-5

work page doi:10.1016/s1571-0661(04)80083-5 1999

[31] [31]

Levy, P.B., Staton, S.: Transition systems over games. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS ’14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2603...

work page doi:10.1145/2603088.2603150 2014

[32] [32]

Morris, J.H.: Lambda-calculus Models of Programming Languages. Ph.D. thesis, Massachusetts Institute of Technology (1968), https://books.google.is/books?id= DklAAQAAIAAJ

work page 1968

[33] [33]

Paolini, L., Piccolo, M., Ronchi Della Rocca, S.: Essential and relational mod- els. Math. Struct. Comput. Sci.27(5), 626–650 (2017). https://doi.org/10.1017/ S0960129515000316, https://doi.org/10.1017/S0960129515000316

work page doi:10.1017/s0960129515000316 2017

[34] [34]

ACM Comput

Patrignani, M., Ahmed, A., Clarke, D.: Formal approaches to secure compilation: A survey of fully abstract compilation and related work. ACM Comput. Surv.51(6), 125:1–125:36 (2019). https://doi.org/10.1145/3280984

work page doi:10.1145/3280984 2019

[35] [35]

In: Sangiorgi, D., Rutten, J.J.M.M

Pitts, A.M.: Howe’s method for higher-order languages. In: Sangiorgi, D., Rutten, J.J.M.M. (eds.) Advanced Topics in Bisimulation and Coinduction, Cambridge tracts in theoretical computer science, vol. 52, pp. 197–232. Cambridge University Press (2012). https://doi.org/10.1017/CBO9780511792588.006

work page doi:10.1017/cbo9780511792588.006 2012

[36] [36]

Plotkin, G.D.: A powerdomain construction. SIAM J. Comput.5(3), 452–487 (1976). https://doi.org/10.1137/0205035, https://doi.org/10.1137/0205035

work page doi:10.1137/0205035 1976

[37] [37]

Plotkin, G.D.: LCF considered as a programming language. Theor. Comput. Sci. 5(3), 223–255 (1977). https://doi.org/10.1016/0304-3975(77)90044-5

work page doi:10.1016/0304-3975(77)90044-5 1977

[38] [38]

Ronchi Della Rocca, S.: Characterization theorems for a filter lambda model. Inf. Control.54(3), 201–216 (1982). https://doi.org/10.1016/S0019-9958(82)80022-3, https://doi.org/10.1016/S0019-9958(82)80022-3

work page doi:10.1016/s0019-9958(82)80022-3 1982

[39] [39]

Sands, D.: Proving the correctness of recursion-based automatic program transfor- mations. Theor. Comput. Sci.167(1&2), 193–233 (1996). https://doi.org/10.1016/ 0304-3975(96)00074-6

work page 1996

[40] [40]

ACM Trans

Sands,D.:Totalcorrectnessbylocalimprovementinthetransformationoffunctional programs. ACM Trans. Program. Lang. Syst.18(2), 175–234 (mar 1996). https: //doi.org/10.1145/227699.227716

work page doi:10.1145/227699.227716 1996

[41] [41]

Sands, D.: Improvement theory and its applications, p. 275–306. Cambridge Uni- versity Press, USA (1999)

work page 1999

[42] [42]

21: Proceedings of the Symposium on Computers and Automata

Scott,D.,Strachey,C.:Towardamathematicalsemanticsforcomputerlanguages.In: MRI Symposium Proceedings, vol. 21: Proceedings of the Symposium on Computers and Automata. pp. 19–46. Fox, J. (Ed.). Polytechnic Press, Polytechnic Institute of Brooklyn, New York (1971)

work page 1971

[43] [43]

In: Proc

Støvring, K., Lassen, S.B.: A complete, co-inductive syntactic theory of sequen- tial control and state. In: Proc. 34th Annual ACM Symposium on Principles of Programming Languages. pp. 161–172. Nice, France (2007), http://doi.acm.org/10. 1145/1190215.1190244 Interaction Improvement 23

work page arXiv 2007

[44] [44]

Wadsworth, C.P.: The Relation Between Computational and Denotational Prop- erties for Scott’sD∞-Models of the Lambda-Calculus. SIAM J. Comput.5(3), 488–521 (1976). https://doi.org/10.1137/0205036 24 A. Lancelot, G. Manzonetto, G. McCusker, G. Vanoni A Proofs of Section 3 Lemma 7(Splitting multisets with respect to derivations).Let t be a term, π▷Γ⊢ k t :M...

work page doi:10.1137/0205036 1976

[45] [45]

Linear types,i.e.T :=L. Cases of the last derivation rule: (a)Unsubstituted variable,i.e.: π= x:0, y: [L]⊢ 0 y:L ax Then asM=0,σmust be of the following shape: ∆⊢ 0 u:0 many Hence π′ := π works, asy{x:=u} = y and k′ = 0. Clearly,|π|@ = |π′|@ = 0, as required. (b)Substituted variable,i.e.: π= x: [L]⊢ 0 x:L ax Then, asM= [L],σmust be of the following shape:...

work page

[46] [46]

The last rule of the derivation must bemany: (πi ▷Γ i, x:M i ⊢li t:L i)i∈I ⊎i∈I Γi, x:M⊢ P i∈I li t: [Li]i∈I many withM=⊎ i∈I Mi andk= P i∈I li and⊎ i∈I Γi =Γ

Multi types,i.e.T := [L i]i∈I with I finite. The last rule of the derivation must bemany: (πi ▷Γ i, x:M i ⊢li t:L i)i∈I ⊎i∈I Γi, x:M⊢ P i∈I li t: [Li]i∈I many withM=⊎ i∈I Mi andk= P i∈I li and⊎ i∈I Γi =Γ. By the multiset splitting lemma (Lemma 7), the derivationσ for u in the hypotheses splits in several derivations of final judgmentsσi ▷∆ i ⊢k′ i u :M i ...

work page

[47] [47]

Linear types,i.e.T :=L. Cases of the last derivation rule: (a)Unsubstituted variable,i.e.:y{x:=u}=yand π= y: [L]⊢ 0 y:L ax Then, takingM :=0,π u must be of the following shape: ∆⊢ 0 u:0 many Henceπ t :=πworks. (b) Substituted variable,i.e.: x{x:=u} = u and π▷∆⊢ k′ u :L. We take M := [L]. Then: π▷∆⊢ k′ u:L πu ▷∆⊢ k′ u: [L] and πt =x: [L]⊢ 0 x:L ax (c)Abstr...

work page

[48] [48]

Multi types,i.e.T := [L i]i∈I with I finite. The last rule of the derivation must bemany: (π′ i ▷ Γi ∪∆ i ⊢ki+k′ i t{x:=u}:L i)i∈I ⊎i∈I Γi ∪∆ i ⊢ P i∈I (ki+k′ i) t{x:=u}: [L i]i∈I many By applying thei.h., we obtain for eachi∈I : πi ▷Γ i, x :M i ⊢ki t :L i and σi ▷∆ i ⊢k′ i u :M i. πu is obtaining by merging theσi (Lemma 9). πt is as follows: (πi ▷ Γi, x:...

work page

[49] [49]

Moreover: (i) ift→ h t′ thenk ′ =k−1; (ii) otherwise, ift→ hτ t′ thenk ′ =k

Quantitative subject reduction: ifπ ▷ Γ⊢ k t :Lthen there is a derivation π′ ▷ Γ⊢ k′ t′ :Lsuch that|π ′|@ =|π| @ −1. Moreover: (i) ift→ h t′ thenk ′ =k−1; (ii) otherwise, ift→ hτ t′ thenk ′ =k

work page

[50] [50]

Subject expansion: if π′ ▷ Γ⊢ k′ t′ :Lthen there is a derivation π ▷ Γ⊢ k t :L. Proof

work page

[51] [51]

Then the last rule of the derivationπis@and is followed by theλrule on the left: Γ, x:M⊢ k1 s:L Γ⊢ k1 λc x.s:M c − →L∆⊢ k2 u:M Γ⊎∆⊢ k (λc x.s)· d u:L @ wherek=k 1 +k 2 +δ ⊥ c,d

(a)Root step,i.e.t= (λ c x.s)· d u→ h◦• s{x:=u}=t ′. Then the last rule of the derivationπis@and is followed by theλrule on the left: Γ, x:M⊢ k1 s:L Γ⊢ k1 λc x.s:M c − →L∆⊢ k2 u:M Γ⊎∆⊢ k (λc x.s)· d u:L @ wherek=k 1 +k 2 +δ ⊥ c,d. By the Substitution Lemma 8, we have that there exists a derivation π′ ▷Γ⊎∆⊢ k1+k2 s{x:=r} :Lsuch that |π′|@ = |πs|@ + |πu|@ =...

work page

[52] [52]

By the Anti-Substitution Lemma 10, there existσ▷Γ ′, x :M ⊢k1 s :L andρ▷Γ ′′ ⊢k2 u:Msuch thatΓ=Γ ′ ⊎Γ ′′ andk=k 1 +k 2

(a)Root step,i.e.t= (λ c x.s)· d u7→ βτ s{x:=u}=t ′. By the Anti-Substitution Lemma 10, there existσ▷Γ ′, x :M ⊢k1 s :L andρ▷Γ ′′ ⊢k2 u:Msuch thatΓ=Γ ′ ⊎Γ ′′ andk=k 1 +k 2. Then we can build the type derivationπ▷Γ⊢ k′ t:Las follows: σ▷Γ ′, x:M⊢ k1 s:L Γ ′ ⊢k1 λc x.s:M c − →Lρ▷Γ ′′ ⊢k2 u:M Γ ′ ⊎Γ ′′ ⊢k′ (λc x.s)· d u:L @ wherek ′ =k+δ ⊥ c,d. (b)Contextual ...

work page

[53] [53]

Ift is head normal then t is head normalizable in0 ≤k interaction steps

By induction on|π| and case analysis on whethert is head normal. Ift is head normal then t is head normalizable in0 ≤k interaction steps. Ift→ h◦• u then there two cases: –t→ hτ u. Then by quantitative subject reduction (Prop. 1(1)), there is σ▷Γ⊢ k u :Lsuch that |π|@ = |σ|@ + 1. By i.h.,u is head normalizable in less thankinteraction steps. Then, the sam...

work page

[54] [54]

By induction onm

We have thatt→ m h◦• h, where h is a head normal form. By induction onm. Cases: 30 A. Lancelot, G. Manzonetto, G. McCusker, G. Vanoni (a) Ifm= 0, thent=h. Then we conclude by Proposition 6. (b) If m > 0, thent→ h◦• u→ m−1 h◦• h. Byi.h., there existsσ▷Γ⊢ k′′ u :Land u⇓ k′′ h◦• . By subject expansion (Prop. 1(2)), there existsπ▷Γ⊢ k′ t :L. By subject reduct...

work page

[55] [55]

If Γ⊢ k t • :Lthen there existL ′, L′′ such that Γ = x : [L′],L ′′ ≤− k′ L′ and L′′ ≤+ k′′ Lwithk=k ′ +k ′′

work page

[56] [56]

If Γ⊢ k t • :Mthen there existM ′, M′′ such that Γ = x : [M′],M ′′ ≤− k′ M′ and M′′ ≤+ k′′ Mwithk=k ′ +k ′′. Proof. We proceed by mutual induction and call HI1 and HI2 the corresponding induction hypotheses. More precisely, we prove (1) by induction on a derivation of Γ⊢ k t • :Land (2) on a derivation ofΓ⊢ k t • :M. Wlog we can considert to be in head no...

work page

[57] [57]

This implies that there are d1, d2 such that d = d1 + d2 + δ⊥ c,c′ and ⟨Γ ′ 1, L′⟩ ≤ + d1 ⟨Γ1, L⟩ and Interaction Improvement 43 M′ ≤− d2 M

∈JuK with ⟨Γ ′ 1, M′ c′ − →L′⟩ ≤ + d ⟨Γ1, M c − →L⟩ and k1 ≥k ′ 1 + d. This implies that there are d1, d2 such that d = d1 + d2 + δ⊥ c,c′ and ⟨Γ ′ 1, L′⟩ ≤ + d1 ⟨Γ1, L⟩ and Interaction Improvement 43 M′ ≤− d2 M. By Proposition 3 there exists(Γ ′′ 1 + Γ ′ 2, L′′, m) ∈Ju· d sK with ⟨Γ ′′ 1 + Γ ′ 2, L′′⟩ ≤ + d′ ⟨Γ ′ 1 + Γ2, L′⟩ and m≤k ′ 1 + k2 + δ⊥ c′,d + d...

work page