pith. sign in

arxiv: 2606.09526 · v1 · pith:ZTFD3CSBnew · submitted 2026-06-08 · 💻 cs.LO · cs.PL

When Types Intersect and Effects Get Handled

Ugo Dal Lago , Taro Sekiyama , Stefano Catozi This is my paper

Pith reviewed 2026-06-27 14:44 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords intersection typesalgebraic effectseffect handlerslambda calculusterminationsubject reductiontype inferencereachability
0
0 comments X

The pith

A new intersection type system for lambda calculus with algebraic effects and handlers characterizes exactly the terminating terms and reduces reachability to type inference.

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

The paper defines an intersection type system for a lambda calculus extended with algebraic effects and handlers. The system tracks behavioral properties of terms under evaluation and satisfies subject reduction and expansion. Because of these properties it identifies precisely which terms reach a normal form. The same typing discipline converts the reachability question into a type-inference question. From the intersection system the authors derive a simpler type system that remains sound yet supports a decidable higher-order model-checking problem.

Core claim

We introduce a novel intersection type system for a λ-calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys subject reduction and expansion. It thus characterizes the set of terms whose evaluation process terminates and allows reducing the reachability problem to type inference. This system induces a system of simple types which is type sound and admits a decidable HOMC problem.

What carries the argument

The intersection type system for the lambda calculus with algebraic effects and handlers, which assigns types that record both functional and effect-handling behavior.

If this is right

  • Every terminating term receives an intersection type and every typed term terminates.
  • Reachability of a given effect or handler configuration reduces directly to checking whether a type exists.
  • The induced simple type system remains sound for the effectful calculus.
  • The higher-order model-checking problem for the induced simple types is decidable.

Where Pith is reading between the lines

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

  • Type-inference algorithms developed for this system could be used as decision procedures for termination in effectful programs.
  • The reduction of reachability to typing suggests that existing type-inference engines might be repurposed for verifying handler safety.
  • The contrast with earlier systems like HEPCF indicates that intersection types can restore decidability where simple types alone fail.

Load-bearing premise

That an intersection type system can be defined for this calculus so that it satisfies subject reduction, expansion, and exactly captures termination.

What would settle it

A concrete term whose evaluation terminates yet receives no type in the system, or a typed term whose evaluation diverges, or a reduction step that violates subject reduction.

Figures

Figures reproduced from arXiv: 2606.09526 by Stefano Catozi, Taro Sekiyama, Ugo Dal Lago.

Figure 1
Figure 1. Figure 1: Reduction rules for HE With this, the seven rewriting rules defined in [PITH_FULL_IMAGE:figures/full_fig_p008_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: HEPCF typing rules. HOMC problem for a very broad class of properties, namely those captured by MSO formulas, would also make this problem decidable for HEPCF. Unfortunately, Dal Lago and Ghyselen showed [13] that this is not the case, and that the HOMC is undecidable in HEPCF already for mere reachability properties. (The latter, by the way, can be formulated for HEPCF in a completely analogous way to wha… view at source ↗
Figure 3
Figure 3. Figure 3: Visualisation of the HEBI type 𝜎 [3] nn{1} → return[1] {{ }} [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: HEBI , typing rules. Definition 4.1. Let Γ, Γ ′ be type contexts. We say Γ ′ ⊆ Γ iff for every 𝑥 : M′ ∈ Γ ′ , one has 𝑥 : M ∈ Γ with M′ ⊆ M. We write 𝑆𝑢𝑏(Γ) for the set of type contexts Γ ′ such that Γ ′ ⊆ Γ. Typing jugements. As in HEPCF, there are three kinds of typing jugements, written as follows. Γ ⊢ C 𝑡 : E Γ ⊢ V 𝑣 : M Γ ⊢ H ℎ : H A typing jugement of the form Γ ⊢ C 𝑡 : E implies that, in the context… view at source ↗
Figure 5
Figure 5. Figure 5: HEBI , Leaf Replacement. not required in HEPCF, where the handling of all operations is done through terms that are forced to adhere to the same (non-behavioral) return type and to the same signature. As a consequence, there would be no meaningful reason to type them multiple times. This situation changes in HEBI, where behavioral information becomes an integral part of the type and handling terms can be t… view at source ↗
Figure 6
Figure 6. Figure 6: HEBI Leaf Replacement: an Example Most of the typing rules presented in [PITH_FULL_IMAGE:figures/full_fig_p013_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: HEB, Typing Rules return[M] {{ }} −{M → E}→ E F −{M → G}→ E 𝜎 [M′ ] {{N → F}} −{M → G}→ 𝜎 [M′ ] {{N → E}} [PITH_FULL_IMAGE:figures/full_fig_p019_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: HEB, Leaf Replacement is more restrictive than that in HEBI, though). A natural question to ask is then whether type checking is itself decidable for HEB. Although we do not study this question in the present work, we conjecture that it is, particularly in a setting where the programmer is required to annotate variables with their types. Although computation types in HEB have an inherently behavioral natur… view at source ↗
Figure 9
Figure 9. Figure 9: HEB, Refinement on Types. 5.2 Behavioural Refinement This section introduces a refinement relation, which certifies that the HEBI typing provides strictly more fine-grained information about terms that are typable in HEB. We start by defining a refine￾ment relation M ⊏ M on pairs of an HEB type M and an HEBI type M. This relation identifies the set of HEBI types M at which a term of an HEB type M may be ty… view at source ↗
Figure 10
Figure 10. Figure 10: HEB refinement for rules, excerpt. property is satisfied, the search can be restricted to HEBI derivations refining Π? In this section we prove this property, by a relative form of subject expansion property. It is convenient, on the HEB side, to lift the reduction relation ↦→ from terms to typing derivations. We give here only a brief intuition of the construction. The goal is to mimick the transformatio… view at source ↗
Figure 11
Figure 11. Figure 11: Example of reduction between two HEB derivations. induced by Theorem 5.1 on a derivation Π typing a computation term 𝑡. We start by defining a notion of substitution directly on type derivations. Let Π ⊲ Δ; 𝑥 :: M ⊢ 𝑝 :: T and Σ ⊲ ∅ ⊢ V 𝑣 :: M be two HEB derivations and 𝑣 ∈ ΛVal a closed term. We define a derivation Π{𝑥\Σ} ⊲ Δ ⊢ 𝑝{𝑥\𝑣 } :: T by induction on Π. Intuitively, this is the derivation obtained … view at source ↗
Figure 12
Figure 12. Figure 12: Description of the function A. start to show it is that every HEB type, by construction, admits a finite number of refinements in HEBI: Lemma 5.5 (Finite Refinement Property). Let T be an HEB type. There exists a finite number of HEBI types 𝜏 such that T ⊏ 𝜏. This is an easy induction on the structure of T. Noticeably, in the inductive cases one exploits the fact that the powerset of a finite set is finit… view at source ↗
Figure 13
Figure 13. Figure 13: HEPCF Type Refinement from types to judgements and derivations in a very natural way. Moreover, reduction itself can be given on derivations rather than terms, following the recipe we used in Section 5.3 for HEB. All this leads quite quickly to the following: Lemma 6.1 (Relative Subject Expansion for HEPCF). Let 𝑡,𝑠 ∈ ΛCmp be two closed terms such that 𝑡 → 𝑠. If there exists Ξ ′ ⊲ ∅ ⊢ C 𝑠 : E and Π ′ ⊲ ∅ … view at source ↗
Figure 14
Figure 14. Figure 14: The different kinds of clashes in HE terms Both the definitions of clashes for withℎ handle 𝜎(𝑣; 𝑥.𝑡) extends easily in the case of return clauses. A.1 Section 4.3 Remark A.1 (Type Context Simplification). Let 𝑝 ∈ Λ be term and 𝑥 a variable that is not free in 𝑝. If Γ ⊢ 𝑝 : E and 𝑥 : M ∈ Γ, then M = { }. In particular, if 𝑝 is closed, then Γ is empty. Lemma A.2 (HEBI, Typability of Values). For 𝑣 ∈ ΛVal, … view at source ↗
Figure 15
Figure 15. Figure 15: HEB refinement for rules, cont’d. Also by hypothesis, there exist two derivations Ξ ′ ⊲ ∅ ⊢ C 𝑢{𝑥\𝑣 } : E and Π ′ ⊲ ∅ ⊢ C 𝑢{𝑥\𝑣 } :: U such that Π ′ ⊏ Ξ ′ . Since by hypothesis Π ⇝ Π ′ , by definition of ⇝ is clear that Π ′ = Π𝑢 {𝑥\Π𝑣 }. We can then apply anti-substitution lemma (Lemma B.10), obtaining that there exist a type M and type derivations Ξ𝑣 ⊲ ∅ ⊢ V 𝑣 : M and Ξ𝑢 ⊲ 𝑥 : M ⊢ C 𝑢 : E, where Π𝑣 ⊏ Ξ𝑣 … view at source ↗
Figure 16
Figure 16. Figure 16: Reductions between two HEB derivations, cont’d. Ξ𝑢 ⊲ 𝑥 : M ⊢ C 𝑢 : E (abs) ∅ ⊢ V 𝜆𝑥.𝑢 : {M → E} Ξ𝑣 ⊲ ∅ ⊢ V 𝑣 : M (app) ∅ ⊢ C (𝜆𝑥.𝑢)𝑣 : E Finally, is easy to see that Π ′ ⊏ Ξ ′ . Case fix. Let 𝑡,𝑡 ′ ∈ ΛCmp such that 𝑡 ′ is typed and 𝑡 →fix 𝑡 ′ . By definition, 𝑡 := (fix 𝑥.𝑣)𝑤 and 𝑡 ′ := 𝑣 {𝑥\fix 𝑥.𝑣 }𝑤. Since 𝑡 is simply typable, Π has the following shape [PITH_FULL_IMAGE:figures/full_fig_p057_16.png] view at source ↗
Figure 17
Figure 17. Figure 17: Definition of B 𝑣 : M𝑖+1 with 𝑖 ≤ 𝑛 − 1 be a sequence of HEBI type derivations such that Π ′ ⊏ Ξ𝑖 . Then, there exist Π ⊲ Δ ⊢ V fix 𝑥.𝑣 :: M → E and Ω ⊲ +𝑖≤𝑛−1Γ𝑖 ⊢ V fix 𝑥.𝑣 : M𝑛 such that Π ⊏ Ω. As we said in the discussion about HEBI computational types, they can be seen as trees. The following measure counts the number of leaves in such trees. Definition B.18. We define a measure on computation HEBI ty… view at source ↗
Figure 18
Figure 18. Figure 18: Description of the formula A, cont’d. Case Integers. Π has the following form: 0 < 𝑛 ≤ 𝑚 (int) Δ ⊢ V 𝑛 :: m We have 𝐽𝑟 ≔ Γ ⊢ V 𝑛 : M with M ∈ {{ } , {i}}. Since |= A (Π, 𝐽𝑟), we have that Γ = ∅ and either M = { } or 𝑖 = 𝑛. We can construct the derivation Ξ as follows: (var) ∅ ⊢ V 𝑛 : M Finally, Π ⊏ Ξ. Case Variable. Π has the following form: (var) Δ; 𝑥 :: M ⊢ V 𝑥 :: M We have 𝐽𝑟 ≔ Γ; 𝑥 : M′ ⊢ V 𝑥 : M, and… view at source ↗
Figure 19
Figure 19. Figure 19: HEPCF, Refinement for Computation Rule such that Π ′ ⊏ Ξ ′ and also there exist Π ⊲ ∅ ⊢ C 𝑡 :: U such that Π ⇝ Π ′ , then there exists Ξ ⊲ ∅ ⊢ C 𝑡 : E such that Π ⊏ Ξ. Proof. By case analysis on the different rewrite rules. We are going to detail only the new rewriting rules, the other cases being identical to Lemma 5.4 Case let-ret. Let 𝑡,𝑡 ′ ∈ ΛCmp such that 𝑡 ′ is typed and 𝑡 →let-ret 𝑡 ′ . By definiti… view at source ↗
Figure 20
Figure 20. Figure 20: HEPCF, Refinement for Handler Rules be the following derivation : Ξ𝑣 ⊲ ∅ ⊢ V 𝑣 : M (ret) ∅ ⊢ C return(𝑣) : return[M ]{{ }} return[M ]{{ }} −{M → F }→ F Ξ𝑢 ⊲ 𝑥 : M ⊢ C 𝑢 : F (let) Ξ ′ ⊲ ∅ ⊢ C 𝑢{𝑥\𝑣 } : F ⊢ C let 𝑥  return(𝑣) in𝑢 : F Finally, we can see that Π ⊏ Ξ. Case let-ef. Let 𝑡,𝑡 ′ ∈ ΛCmp such that 𝑡 ′ is typed and 𝑡 →let-ef 𝑡 ′ . By definition, 𝑡 := let 𝑥  𝜎(𝑣;𝑦.𝑠) in𝑢 and 𝑡 ′ := 𝜎(𝑣;𝑦.let 𝑥  𝑠 in… view at source ↗
Figure 21
Figure 21. Figure 21: HEPCF, Reduction Rules. following typing derivation: (𝐴) (𝐵) (Ξ 𝑖 𝑘 ⊲ 𝑥 : M𝑖 𝑘 ⊢ C 𝑢 : F 𝑖 𝑘 )𝑘 ∈𝐾𝑖 ,𝑖∈𝐼 (let) ∅ ⊢ C let 𝑥  𝜎(𝑣;𝑦.𝑠) in𝑢 : 𝜎 [M ]{{N𝑖 → E𝑖 }}𝑖∈𝐼 [PITH_FULL_IMAGE:figures/full_fig_p074_21.png] view at source ↗
read the original abstract

We introduce a novel intersection type system for a $\lambda$-calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties of intersection type systems, in particular subject reduction and expansion. It thus characterizes the set of terms whose evaluation process terminates and, at the same time, allows reducing the reachability problem to type inference. This new system, the first with these features for a calculus with handlers, induces a system of simple types which, although not guaranteeing termination, is type sound and admits a decidable HOMC problem, unlike similar type systems like Dal Lago and Ghyselen's HEPCF.

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.

Referee Report

0 major / 2 minor

Summary. The paper introduces a novel intersection type system for a λ-calculus with algebraic effects and handlers. The system is behavioral, enjoys subject reduction and expansion, characterizes terminating terms, reduces reachability to type inference, and induces a sound simple type system with decidable HOMC (unlike HEPCF).

Significance. If the derivations hold, the result is significant as the first intersection type system with these classical properties for a calculus with handlers. It provides a behavioral characterization of termination and a reduction of reachability to type inference, while the induced simple types offer decidability advantages over prior systems like Dal Lago and Ghyselen's HEPCF. The manuscript supplies arguments for subject reduction/expansion and soundness.

minor comments (2)
  1. The abstract claims the system 'induces a system of simple types' with decidable HOMC; the manuscript should explicitly state the induction construction and the precise HOMC instance in a dedicated section or theorem.
  2. Notation for effect operations and handlers in the typing rules should be clarified with an example derivation to aid readability, especially for readers unfamiliar with algebraic effects.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our manuscript and the recommendation of minor revision. The referee's description accurately captures the main results concerning the intersection type system for the lambda calculus with algebraic effects and handlers, including subject reduction/expansion, termination characterization, and the induced simple type system with decidable HOMC.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper introduces a new intersection type system for the lambda-calculus with algebraic effects and handlers, then establishes subject reduction, expansion, termination characterization, and reachability reduction via direct arguments on the typing rules. These steps are presented as standard formal derivations without reduction to fitted parameters, self-definitional loops, or load-bearing self-citations. The induced simple type system and its soundness/HOMC decidability are shown separately. No quoted step equates a claimed result to its own input by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no specific free parameters, axioms, or invented entities identifiable from available text. Standard background assumptions of lambda calculus and type theory are presumed but unexamined.

pith-pipeline@v0.9.1-grok · 5630 in / 1115 out tokens · 29674 ms · 2026-06-27T14:44:26.425716+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

58 extracted references · 32 canonical work pages

  1. [1]

    Beniamino Accattoli, Ugo Dal Lago, and Gabriele Vanoni. 2021. The (in) efficiency of interaction.Proceedings of the ACM on Programming Languages5, POPL (2021), 1–33

    2021

  2. [2]

    Sandra Alves, Delia Kesner, and Miguel Ramos. 2023. Quantitative global memory. InInternational Workshop on Logic, Language, Information, and Computation. Springer, 53–68

    2023

  3. [3]

    Henk Barendregt, Mario Coppo, and Mariangiola Dezani-Ciancaglini. 1983. A filter lambda model and the completeness of type assignment1.The journal of symbolic logic48, 4 (1983), 931–940

    1983

  4. [4]

    Andrej Bauer and Matija Pretnar. 2014. An Effect System for Algebraic Effects and Handlers.Logical Methods in Computer Science10, 4 (2014). doi:10.2168/LMCS-10(4:9)2014

    work page doi:10.2168/lmcs-10(4:9)2014 2014

  5. [5]

    Alexis Bernadet and Stéphane Lengrand. 2011. Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism. InComputer Science Logic - 25th International Workshop / 20th Annual Conference of the EACSL, CSL 2011, Bergen, Norway, September 12-15, 2011, Proceedings (LIPIcs, Vol. 12), Marc Bezem (Ed.). Schloss Dagstuhl - Leibniz-Zentrum für...

    work page doi:10.4230/lipics.csl.2011.51 2011

  6. [6]

    Gavin Bierman, Martín Abadi, and Mads Torgersen. 2014. Understanding typescript. InEuropean Conference on Object-Oriented Programming. Springer, 257–281. 28 Ugo Dal Lago, Taro Sekiyama, and Stefano Catozi

    2014

  7. [7]

    Viviana Bono and Mariangiola Dezani-Ciancaglini. 2020. A tale of intersection types. InProceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. 7–20

    2020

  8. [8]

    Gilad Bracha, Martin Odersky, David Stoutamire, and Philip Wadler. 1998. Making the future safe for the past: Adding genericity to the Java programming language.Acm sigplan notices33, 10 (1998), 183–200

    1998

  9. [9]

    Flavien Breuvart and Ugo Dal Lago. 2018. On intersection types and probabilistic lambda calculi. InProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming. 1–13

    2018

  10. [10]

    Pierre Clairambault, Charles Grellois, and Andrzej S Murawski. 2017. Linearity in higher-order recursion schemes. Proceedings of the ACM on Programming Languages2, POPL (2017), 1–29

    2017

  11. [11]

    Mario Coppo and Mariangiola Dezani-Ciancaglini. 1978. A new type assignment for𝜆-terms.Archiv für mathematische Logik und Grundlagenforschung19, 1 (1978), 139–156

    1978

  12. [12]

    Ugo Dal Lago, Claudia Faggian, and Simona Ronchi Della Rocca. 2021. Intersection types and (positive) almost-sure termination.Proceedings of the ACM on Programming Languages5, POPL (2021), 1–32

    2021

  13. [13]

    Ugo Dal Lago and Alexis Ghyselen. 2024. On Model-Checking Higher-Order Effectful Programs.Proc. ACM Program. Lang.8, POPL (2024), 2610–2638. doi:10.1145/3632929

    work page doi:10.1145/3632929 2024

  14. [14]

    2007.Sémantiques de la logique linéaire et temps de calcul

    Daniel De Carvalho. 2007.Sémantiques de la logique linéaire et temps de calcul. Ph. D. Dissertation. Aix-Marseille 2

    2007

  15. [15]

    Ugo Deliguoro and Adolfo Piperno. 1995. Nondeterministic extensions of untyped 𝜆-calculus.Information and Computation122, 2 (1995), 149–177

    1995

  16. [16]

    Andrej Dudenhefner and Daniele Pautasso. 2024. Mechanized Subject Expansion in Uniform Intersection Types for Perpetual Reductions. In9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 8–1

    2024

  17. [17]

    Ryunosuke Endo and Tachio Terauchi. 2025. Reachability is Decidable for ATM-Typable Finitary PCF with Effect Handlers. InProgramming Languages and Systems - 23rd Asian Symposium, APLAS 2025, Bengaluru, India, October 27-30, 2025, Proceedings (Lecture Notes in Computer Science, Vol. 16201), Alex Potanin (Ed.). Springer, 67–87. doi:10.1007/978- 981-95-3585-9_4

    work page doi:10.1007/978- 2025

  18. [18]

    Zeinab Galal, Francesco Gavazzo, Riccardo Treglia, and Gabriele Vanoni. 2025. Monadic Intersection Types, Relationally, and Ordered.ACM Transactions on Programming Languages and Systems47, 4 (2025), 1–51

    2025

  19. [19]

    Francesco Gavazzo, Riccardo Treglia, and Gabriele Vanoni. 2024. Monadic intersection types, relationally. InEuropean Symposium on Programming. Springer, 22–51

    2024

  20. [20]

    J. Y. Girard. 1972.Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse de Doctorat d’État. Université Paris 7

    1972

  21. [21]

    Colin S. Gordon. 2020. Lifting Sequential Effects to Control Operators. In34th European Conference on Object- Oriented Programming, ECOOP 2020 (LIPIcs, Vol. 166), Robert Hirschfeld and Tobias Pape (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 23:1–23:30. doi:10.4230/LIPIcs.ECOOP.2020.23

    work page doi:10.4230/lipics.ecoop.2020.23 2020

  22. [22]

    Colin S. Gordon. 2021. Polymorphic Iterable Sequential Effect Systems.ACM Trans. Program. Lang. Syst.43, 1 (2021), 4:1–4:79. doi:10.1145/3450272

    work page doi:10.1145/3450272 2021

  23. [23]

    Charles Grellois and Paul-André Melliès. 2015. Relational Semantics of Linear Logic and Higher-order Model Checking. In24th EACSL Annual Conference on Computer Science Logic (CSL 2015) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 41), Stephan Kreutzer (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 260–276....

    work page doi:10.4230/lipics.csl.2015.260 2015

  24. [24]

    Daniel Hillerström and Sam Lindley. 2016. Liberating effects with rows and handlers. InProceedings of the 1st International Workshop on Type-Driven Development, TyDe@ICFP 2016, Nara, Japan, September 18, 2016. 15–27. doi:10. 1145/2976022.2976033

    arXiv 2016

  25. [25]

    Oleg Kiselyov and Hiromi Ishii. 2015. Freer monads, more extensible effects. InProceedings of the 8th ACM SIGPLAN Symposium on Haskell, Haskell 2015. 94–105. doi:10.1145/2804302.2804319

    work page doi:10.1145/2804302.2804319 2015

  26. [27]

    Teodor Knapik, Damian Niwinski, and Pawel Urzyczyn. 2002. Higher-Order Pushdown Trees Are Easy. InFoundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002. Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8-12, 2002, Proceedings (Lecture Note...

    work page doi:10.1007/3- 2002

  27. [28]

    Naoki Kobayashi. 2009. Types and higher-order recursion schemes for verification of higher-order programs. In Proceedings of the 36th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 416–428

    2009

  28. [29]

    Naoki Kobayashi. 2013. Model checking higher-order programs.Journal of the ACM (JACM)60, 3 (2013), 1–62. When Types Intersect and Effects Get Handled 29

    2013

  29. [30]

    Naoki Kobayashi, Ugo Dal Lago, and Charles Grellois. 2019. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. In34th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2019, Vancouver, BC, Canada, June 24-27, 2019. IEEE, 1–14. doi:10.1109/LICS.2019.8785679

    work page doi:10.1109/lics.2019.8785679 2019

  30. [31]

    Naoki Kobayashi and Atsushi Igarashi. 2013. Model-Checking Higher-Order Programs with Recursive Types. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings (Lecture Notes in Compute...

    work page doi:10.1007/978-3-642-37036-6_24 2013

  31. [32]

    Luke Ong

    Naoki Kobayashi and C.-H. Luke Ong. 2009. A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. InProceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, LICS 2009. IEEE Computer Society, 179–188. doi:10.1109/LICS.2009.29

    work page doi:10.1109/lics.2009.29 2009

  32. [33]

    Eric Koskinen and Tachio Terauchi. 2014. Local Temporal Reasoning. InJoint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (CSL-LICS ’14), Thomas A. Henzinger and Dale Miller (Eds.). ACM, 59:1–59:10. doi:10.1145/2603088.2603138

    work page doi:10.1145/2603088.2603138 2014

  33. [34]

    Daan Leijen. 2017. Type directed compilation of row-typed algebraic effects. InProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017. 486–499. http://dl.acm.org/citation.cfm?id=3009872

    2017

  34. [35]

    Eugenio Moggi. 1991. Notions of computation and monads.Information and computation93, 1 (1991), 55–92

    1991

  35. [36]

    Yoji Nanjo, Hiroshi Unno, Eric Koskinen, and Tachio Terauchi. 2018. A Fixpoint Logic and Dependent Effects for Temporal Property Verification. InProceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18), Anuj Dawar and Erich Grädel (Eds.). ACM, 759–768. doi:10.1145/3209108.3209204

    work page doi:10.1145/3209108.3209204 2018

  36. [37]

    Martin Odersky, Philippe Altherr, Vincent Cremet, Burak Emir, Sebastian Maneth, Stéphane Micheloud, Nikolay Mihaylov, Michel Schinz, Erik Stenman, and Matthias Zenger. 2004. An overview of the Scala programming language. (2004)

    2004

  37. [38]

    Luke Ong

    C.-H. Luke Ong. 2006. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, W A, USA, Proceedings. IEEE Computer Society, 81–90. doi:10.1109/LICS.2006.38

    work page doi:10.1109/lics.2006.38 2006

  38. [39]

    Dominic Orchard and Nobuko Yoshida. 2016. Effects as sessions, sessions as effects.ACM SIGPLAN Notices51, 1 (2016), 568–581

    2016

  39. [40]

    Plotkin and John Power

    Gordon D. Plotkin and John Power. 2003. Algebraic Operations and Generic Effects.Applied Categorical Structures11, 1 (2003), 69–94. doi:10.1023/A:1023064908962

    work page doi:10.1023/a:1023064908962 2003

  40. [41]

    Plotkin and Matija Pretnar

    Gordon D. Plotkin and Matija Pretnar. 2009. Handlers of Algebraic Effects. InProgramming Languages and Systems, 18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, Proceedings. 80–94. doi:10.1007/978-3-642-00590-9_7

    work page doi:10.1007/978-3-642-00590-9_7 2009

  41. [42]

    Plotkin and Matija Pretnar

    Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects.Logical Methods in Computer Science9, 4 (2013). doi:10.2168/LMCS-9(4:23)2013

    work page doi:10.2168/lmcs-9(4:23)2013 2013

  42. [43]

    Matija Pretnar. 2015. An Introduction to Algebraic Effects and Handlers. Invited tutorial paper. InThe 31st Conference on the Mathematical Foundations of Programming Semantics, MFPS 2015, Nijmegen, The Netherlands, June 22-25, 2015 (Electronic Notes in Theoretical Computer Science, Vol. 319), Dan R. Ghica (Ed.). Elsevier, 19–35. doi:10.1016/J.ENTCS. 2015.12.003

    work page doi:10.1016/j.entcs 2015

  43. [44]

    Reynolds

    John C. Reynolds. 1974. Towards a theory of type structure. InProgramming Symposium, Proceedings Colloque sur la Programmation. 408–423. doi:10.1007/3-540-06859-7_148

    work page doi:10.1007/3-540-06859-7_148 1974

  44. [45]

    Reynolds

    John C. Reynolds. 1988.Preliminary Design of the Programming Language Forsythe. Technical Report CMU-CS-88-159. Carnegie Mellon University

    1988

  45. [46]

    Tom Schrijvers, Maciej Piróg, Nicolas Wu, and Mauro Jaskelioff. 2019. Monad transformers and modular algebraic effects: what binds them together. InProceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18-23, 2019, Richard A. Eisenberg (Ed.). ACM, 98–113. doi:10.1145/3331545. 3342595

    work page doi:10.1145/3331545 2019

  46. [47]

    Taro Sekiyama, Ugo Dal Lago, and Hiroshi Unno. 2025. On Higher-Order Model Checking of Effectful Answer-Type- Polymorphic Programs.Proc. ACM Program. Lang.9, OOPSLA2 (2025), 3726–3754. doi:10.1145/3763184

    work page doi:10.1145/3763184 2025

  47. [48]

    Taro Sekiyama and Hiroshi Unno. 2023. Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations.Proc. ACM Program. Lang.7, POPL, Article 71 (2023), 32 pages. doi:10.1145/3571264

    work page doi:10.1145/3571264 2023

  48. [49]

    Taro Sekiyama and Hiroshi Unno. 2024. Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification.Proc. ACM Program. Lang.8, OOPSLA2 (2024), 2662–2691. doi:10.1145/3689805

    work page doi:10.1145/3689805 2024

  49. [50]

    Taro Sekiyama and Hiroshi Unno. 2025. Algebraic Temporal Effects: Temporal Verification of Recursively Typed Higher-Order Programs.Proc. ACM Program. Lang.9, POPL (2025), 2306–2336. doi:10.1145/3704914 30 Ugo Dal Lago, Taro Sekiyama, and Stefano Catozi

    work page doi:10.1145/3704914 2025

  50. [51]

    Christian Skalka and Scott F. Smith. 2004. History Effects and Verification. InProgramming Languages and Systems: Second Asian Symposium, APLAS 2004 (Lecture Notes in Computer Science, Vol. 3302), Wei-Ngan Chin (Ed.). Springer, 107–128. doi:10.1007/978-3-540-30477-7_8

    work page doi:10.1007/978-3-540-30477-7_8 2004

  51. [52]

    Smith, and David Van Horn

    Christian Skalka, Scott F. Smith, and David Van Horn. 2008. Types and trace effects of higher order programs.J. Funct. Program.18, 2 (2008), 179–249. doi:10.1017/S0956796807006466

    work page doi:10.1017/s0956796807006466 2008

  52. [53]

    2006.Lectures on the Curry-Howard isomorphism

    Morten Heine Sørensen and Pawel Urzyczyn. 2006.Lectures on the Curry-Howard isomorphism. Vol. 149. Elsevier

    2006

  53. [54]

    Nikhil Swamy, Joel Weinberger, Cole Schlesinger, Juan Chen, and Benjamin Livshits. 2013. Verifying higher-order programs with the dijkstra monad. InACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’13, Seattle, W A, USA, June 16-19, 2013, Hans-Juergen Boehm and Cormac Flanagan (Eds.). ACM, 387–398. doi:10.1145/2491956.2491978

    work page doi:10.1145/2491956.2491978 2013

  54. [55]

    William W. Tait. 1967. Intensional Interpretations of Functionals of Finite Type I.J. Symb. Log.32, 2 (1967), 198–212. doi:10.2307/2271658

    work page doi:10.2307/2271658 1967

  55. [56]

    Wenhao Tang. 2024. Session-Typed Effect Handlers.POPL 2024 SRC(2024)

    2024

  56. [57]

    Wenhao Tang and Sam Lindley. 2026. Rows and Capabilities as Modal Effects.Proc. ACM Program. Lang.10, POPL (2026), 923–950. doi:10.1145/3776674

    work page doi:10.1145/3776674 2026

  57. [58]

    Steffen van Bakel, Franco Barbanera, and Ugo de’Liguoro. 2018. Intersection Types for the lambda-mu Calculus.Log. Methods Comput. Sci.14, 1 (2018). doi:10.23638/LMCS-14(1:2)2018

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

  58. [59]

    Takuma Yoshioka, Taro Sekiyama, and Atsushi Igarashi. 2024. Abstracting Effect Systems for Algebraic Effect Handlers. Proc. ACM Program. Lang.8, ICFP (2024), 455–484. doi:10.1145/3674641 When Types Intersect and Effects Get Handled 31 A Proofs of Section 4 In this appendix, we provide detailed proofs of all the statements presented in the main text. The o...

    work page doi:10.1145/3674641 2024