**Orna Kupferman Pawel Sobocinski (Eds.)**

# **Foundations of Software Science and Computation Structures**

**26th International Conference, FoSSaCS 2023 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023 Paris, France, April 22–27, 2023 Proceedings**

## Lecture Notes in Computer Science 13992

Founding Editors

Gerhard Goos, Germany Juris Hartmanis, USA

## Editorial Board Members

Elisa Bertino, USA Wen Gao, China

Bernhard Steffen , Germany Moti Yung , USA

## Advanced Research in Computing and Software Science Subline of Lecture Notes in Computer Science

Subline Series Editors

Giorgio Ausiello, University of Rome 'La Sapienza', Italy Vladimiro Sassone, University of Southampton, UK

Subline Advisory Board

Susanne Albers, TU Munich, Germany Benjamin C. Pierce, University of Pennsylvania, USA Bernhard Steffen , University of Dortmund, Germany Deng Xiaotie, Peking University, Beijing, China Jeannette M. Wing, Microsoft Research, Redmond, WA, USA More information about this series at https://link.springer.com/bookseries/558

Orna Kupferman • Pawel Sobocinski Editors

# Foundations of Software Science and Computation Structures

26th International Conference, FoSSaCS 2023 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023 Paris, France, April 22–27, 2023 Proceedings

Editors Orna Kupferman The Hebrew University of Jerusalem Jerusalem, Israel

Pawel Sobocinski Tallinn University of Technology Tallinn, Estonia

ISSN 0302-9743 ISSN 1611-3349 (electronic) Lecture Notes in Computer Science ISBN 978-3-031-30828-4 ISBN 978-3-031-30829-1 (eBook) https://doi.org/10.1007/978-3-031-30829-1

© The Editor(s) (if applicable) and The Author(s) 2023. This book is an open access publication.

Open Access This book is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

The use of general descriptive names, registered names, trademarks, service marks, etc. in this publication does not imply, even in the absence of a specific statement, that such names are exempt from the relevant protective laws and regulations and therefore free for general use.

The publisher, the authors, and the editors are safe to assume that the advice and information in this book are believed to be true and accurate at the date of publication. Neither the publisher nor the authors or the editors give a warranty, expressed or implied, with respect to the material contained herein or for any errors or omissions that may have been made. The publisher remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

This Springer imprint is published by the registered company Springer Nature Switzerland AG The registered company address is: Gewerbestrasse 11, 6330 Cham, Switzerland

## ETAPS Foreword

Welcome to the 26th ETAPS! ETAPS 2023 took place in Paris, the beautiful capital of France. ETAPS 2023 was the 26th instance of the European Joint Conferences on Theory and Practice of Software. ETAPS is an annual federated conference established in 1998, and consists of four conferences: ESOP, FASE, FoSSaCS, and TACAS. Each conference has its own Program Committee (PC) and its own Steering Committee (SC). The conferences cover various aspects of software systems, ranging from theoretical computer science to foundations of programming languages, analysis tools, and formal approaches to software engineering. Organising these conferences in a coherent, highly synchronized conference programme enables researchers to participate in an exciting event, having the possibility to meet many colleagues working in different directions in the field, and to easily attend talks of different conferences. On the weekend before the main conference, numerous satellite workshops took place that attracted many researchers from all over the globe.

ETAPS 2023 received 361 submissions in total, 124 of which were accepted, yielding an overall acceptance rate of 34.3%. I thank all the authors for their interest in ETAPS, all the reviewers for their reviewing efforts, the PC members for their contributions, and in particular the PC (co-)chairs for their hard work in running this entire intensive process. Last but not least, my congratulations to all authors of the accepted papers!

ETAPS 2023 featured the unifying invited speakers Véronique Cortier (CNRS, LORIA laboratory, France) and Thomas A. Henzinger (Institute of Science and Technology, Austria) and the conference-specific invited speakers Mooly Sagiv (Tel Aviv University, Israel) for ESOP and Sven Apel (Saarland University, Germany) for FASE. Invited tutorials were provided by Ana-Lucia Varbanescu (University of Twente and University of Amsterdam, The Netherlands) on heterogeneous computing and Joost-Pieter Katoen (RWTH Aachen, Germany and University of Twente, The Netherlands) on probabilistic programming.

As part of the programme we had the second edition of TOOLympics, an event to celebrate the achievements of the various competitions or comparative evaluations in the field of ETAPS.

ETAPS 2023 was organized jointly by Sorbonne Université and Université Sorbonne Paris Nord. Sorbonne Université (SU) is a multidisciplinary, research-intensive and worldclass academic institution. It was created in 2018 as the merge of two first-class research-intensive universities, UPMC (Université Pierre and Marie Curie) and Paris-Sorbonne. SU has three faculties: humanities, medicine, and 55,600 students (4,700 PhD students; 10,200 international students), 6,400 teachers, professor-researchers and 3,600 administrative and technical staff members. Université Sorbonne Paris Nord is one of the thirteen universities that succeeded the University of Paris in 1968. It is a major teaching and research center located in the north of Paris. It has five campuses, spread over the two departments of Seine-Saint-Denis and Val d'Oise: Villetaneuse, Bobigny, Saint-Denis, the Plaine Saint-Denis and Argenteuil. The university has more than 25,000 students in different fields, such as health, medicine, languages, humanities, and science. The local organization team consisted of Fabrice Kordon (general co-chair), Laure Petrucci (general co-chair), Benedikt Bollig (workshops), Stefan Haar (workshops), Étienne André (proceedings and tutorials), Céline Ghibaudo (sponsoring), Denis Poitrenaud (web), Stefan Schwoon (web), Benoît Barbot (publicity), Nathalie Sznajder (publicity), Anne-Marie Reytier (communication), Hélène Pétridis (finance) and Véronique Criart (finance).

ETAPS 2023 is further supported by the following associations and societies: ETAPS e.V., EATCS (European Association for Theoretical Computer Science), EAPLS (European Association for Programming Languages and Systems), EASST (European Association of Software Science and Technology), Lip6 (Laboratoire d'Informatique de Paris 6), LIPN (Laboratoire d'informatique de Paris Nord), Sorbonne Université, Université Sorbonne Paris Nord, CNRS (Centre national de la recherche scientifique), CEA (Commissariat à l'énergie atomique et aux énergies alternatives), LMF (Laboratoire méthodes formelles), and Inria (Institut national de recherche en informatique et en automatique).

The ETAPS Steering Committee consists of an Executive Board, and representatives of the individual ETAPS conferences, as well as representatives of EATCS, EAPLS, and EASST. The Executive Board consists of Holger Hermanns (Saarbrücken), Marieke Huisman (Twente, chair), Jan Kofroň (Prague), Barbara König (Duisburg), Thomas Noll (Aachen), Caterina Urban (Inria), Jan Křetínský (Munich), and Lenore Zuck (Chicago).

Other members of the steering committee are: Dirk Beyer (Munich), Luís Caires (Lisboa), Ana Cavalcanti (York), Bernd Finkbeiner (Saarland), Reiko Heckel (Leicester), Joost-Pieter Katoen (Aachen and Twente), Naoki Kobayashi (Tokyo), Fabrice Kordon (Paris), Laura Kovács (Vienna), Orna Kupferman (Jerusalem), Leen Lambers (Cottbus), Tiziana Margaria (Limerick), Andrzej Murawski (Oxford), Laure Petrucci (Paris), Elizabeth Polgreen (Edinburgh), Peter Ryan (Luxembourg), Sriram Sankaranarayanan (Boulder), Don Sannella (Edinburgh), Natasha Sharygina (Lugano), Pawel Sobocinski (Tallinn), Sebastián Uchitel (London and Buenos Aires), Andrzej Wasowski (Copenhagen), Stephanie Weirich (Pennsylvania), Thomas Wies (New York), Anton Wijs (Eindhoven), and James Worrell (Oxford).

I would like to take this opportunity to thank all authors, keynote speakers, attendees, organizers of the satellite workshops, and Springer-Verlag GmbH for their support. I hope you all enjoyed ETAPS 2023.

Finally, a big thanks to Laure and Fabrice and their local organization team for all their enormous efforts to make ETAPS a fantastic event.

April 2023 Marieke Huisman ETAPS SC Chair ETAPS e.V. President

## Preface

This volume contains the papers presented at the 26th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2023), which was held 24–27 April, 2023, in Paris, France. The conference is dedicated to foundational research with a clear significance for software science and brings together research on theories and methods to support the analysis, integration, synthesis, transformation, and verification of programs and software systems.

The program consisted of 26 contributed papers, selected from among 85 submissions. Each submission was assessed by three or more Program Committee members. The conference management system EasyChair was used to handle the submissions, to conduct the electronic Program Committee discussions, and to assist with the assembly of the proceedings.

We wish to thank all the authors who submitted papers for consideration, the members of the Program Committee for their conscientious work, and all additional reviewers who assisted the Program Committee in the evaluation process. Finally, we would like to thank the ETAPS organization for providing an excellent environment for FoSSaCS, other conferences, and workshops.

February 2023 Orna Kupferman Pawel Sobocinski

## Organization

## Program Committee

Nathalie Bertrand Inria, France Thomas Colcombet CNRS, France Assia Mahboubi Inria, France

Parosh Aziz Abdulla Uppsala University, Sweden Giovanni Bacci Aalborg University, Denmark Patrick Baillot CNRS and Université de Lille, France Lars Birkedal Aarhus University, Denmark Véronique Bruyère University of Mons, Belgium Marco Carbone IT University of Copenhagen, Denmark Ugo Dal Lago Università di Bologna, Italy and Inria Sophia Antipolis, France Emmanuel Filiot Université libre de Bruxelles, Belgium Marco Gaboardi Boston University, USA Bart Jacobs Radboud University, The Netherlands Bartek Klin University of Oxford, UK Orna Kupferman Hebrew University of Jerusalem, Israel Barbara König University of Duisburg-Essen, Germany Shahar Maoz Tel Aviv University, Israel Kuldeep S. Meel National University of Singapore, Singapore Stefan Milius FAU Erlangen, Germany Filip Murlak University of Warsaw, Poland Koko Muroya RIMS, Kyoto University, Japan Joel Ouaknine Max Planck Institute for Software Systems, Germany Alexandra Silva University College London, UK Pawel Sobocinski Tallinn University of Technology, Estonia Sam Staton University of Oxford, UK Alwen Tiu Australian National University, Australia Frank Valencia LIX, Ecole Polytechnique, France Daniele Varacca LACL - Université Paris Est Créteil, France

## Additional Reviewers

Aguirre, Alejandro Akshay, S. Aranda, Jesus Arsiwalla, Xerxes Asada, Kazuyuki Aubert, Clément Bacci, Giorgio Bahr, Patrick Balachander, Mrudula Balaji, Nikhil Balasubramanian, A. R. Baldan, Paolo Bansal, Suguman Barbarossa, Davide Basold, Henning Benerecetti, Massimo Bengtson, Jesper Bernardi, Giovanni Boker, Udi Bonchi, Filippo Brice, Léonard Béal, Marie-Pierre Casares, Antonio Castiglioni, Valentina Chockler, Hana Chroboczek, Juliusz Clairambault, Pierre Clemente, Lorenzo Clouston, Ranald Cohen, Liron Corbyn, Nathan Corradini, Andrea Danielsson, Nils Anders Dantchev, Stefan de Groot, Jim de Vilhena, Paulo Dell'Erba, Daniele Demangeon, Romain Dima, Catalin Dragoi, Cezara Dubut, Jérémy Fahrenberg, Uli Feier, Cristina

Fijalkow, Nathanaël Finster, Eric Fiterau-Brostean, Paul Freund, Anton Ganty, Pierre Gavazzo, Francesco Geeraerts, Gilles Ghyselen, Alexis Goy, Alexandre Gratzer, Daniel Guilmant, Quentin Gurke, Sebastian Gutierrez, Julian Hadzihasanovic, Amar Hamel-de Le Court, Edwin Hansen, Helle Hvid Helouet, Loic Henry, Léo Hirschowitz, Tom Hofman, Piotr Hou, Zhe Jaber, Guilhem Jaquard, Arthur Jindal, Gorav Jonsson, Bengt Kappé, Tobias Karimov, Toghrul Kavvos, Alex Kelmendi, Edon Kerjean, Marie Kopczynski, Eryk Kruckman, Alex Lebeda, Christian Janos Li, Yong Lucyshyn-Wright, Rory Luttik, Bas Main, James C. A. Marin, Sonia Markey, Nicolas Mascle, Corto Mathur, Umang Mazza, Damiano McKenzie, Pierre

Michaliszyn, Jakub Michaux, Christian Mimram, Samuel Morales Elena, Marianela Nieuwveld, Joris Niewerth, Matthias Niwinski, Damian Norrish, Michael Nuyts, Andreas Olarte, Carlos Oliva, Paulo Pagani, Michele Patterson, Evan Perez, Guillermo Piedeleu, Robin Pinzón, Carlos Pommellet, Adrien Pous, Damien Pradic, Pierre Praveen, M. Purser, David Ramírez, Sergio Raskin, Jean-Francois Reynouard, Raphaël Riba, Colin Román, Mario Rossberg, Andreas Rot, Jurriaan Saivasan, Prakash Sakayori, Ken Sanan, David Sangnier, Arnaud Sankur, Ocan Schmid, Todd Schmitz, Sylvain

Shevrin, Ilia Shillito, Ian Shirmohammadi, Mahsa Skrzypczak, Michał Sokolova, Ana Spies, Simon Stefanesco, Leo Stefański, Rafał Stein, Dario Sterling, Jonathan Totzke, Patrick Traytel, Dmitriy Tsampas, Stelios Tsukada, Takeshi Ulrik, Nikolaj Jensen Urbat, Henning Vahanwala, Mihir van der Weide, Niels van Dijk, Tom van Glabbeek, Rob van Gool, Sam Vandenhove, Pierre Vignudelli, Valeria Vilmart, Renaud Vákár, Matthijs Wagemaker, Jana Wang, Di Weininger, Maximilian Winskel, Glynn Winter, Sarah Wißmann, Thorsten Worrell, James Yamakami, Tomoyuki Yatapanage, Nisansala

## Contents

## When Programs Have to Watch Paint Dry

Danel Ahmanp q

Faculty of Mathematics and Physics, University of Ljubljana, Ljubljana, Slovenia<EMAIL_ADDRESS>
Abstract. We explore type systems and programming abstractions for the safe usage of resources. In particular, we investigate how to use types to modularly specify and check *when* programs are allowed to use their resources, e.g., when programming a robot arm on a production line, it is crucial that painted parts are given enough time to dry before assembly. We capture such *temporal resources* using a time-graded variant of Fitch-style modal type systems, develop a corresponding modally typed, effectful core calculus, and equip it with a graded-monadic denotational semantics illustrated by a concrete presheaf model. Our calculus also includes graded algebraic effects and effect handlers. They are given a novel temporally aware treatment in which operations' specifications include their execution times and their continuations know that an operation's worth of additional time has passed before they start executing, making it possible to safely access further temporal resources in them.

Keywords: Temporal resources · Modal types · Graded monads · Algebraic effects · Effect handlers.

## 1 Introduction

The correct usage of resources is at the heart of many programs, especially if they control safety-critical machinery. Such resources can take many different forms: ensuring that file handles are not arbitrarily duplicated or discarded (as captured by linear and uniqueness types) [11,25,40], or guaranteeing that communication happens according to protocols (as specified by session types) [30,70], or controlling how data is laid out in memory (as in Hoare and separation logics) [2,34,56,64], or assuring that resources are correctly finalised [1,43].

In contrast to the above approaches that predominantly focus on *how* resources are used, we study how to modularly specify and verify *when* programs can use their resources—we call such resources *temporal*. For instance, consider the following code snippet controlling a robot arm on a (car) production line:

let pbody', left-door', right-door'q " paint pbody, left-door, right-doorq in assemble pbody', left-door', right-door'q

Here, the correct execution of the program (and thus operation of the robot arm it is controlling) relies on the car parts given enough time to dry between painting and assembly. Therefore, in its current form, the above code is correct only if a compiler (or a scheduler) inserts enough of a time delay at compile time (resp. dynamically blocks program's execution for enough time) between the calls to paint and assemble. However, in either case, one still faces the question of how to reason about the correctness of the compiled code (resp. dynamic checks).

In this paper, we focus on developing a type system based means for reasoning about the temporal correctness of the code that the above-mentioned compiler might produce, or that a programmer might write directly when full control of the code is important. In particular, we had *three desiderata* we set out to fulfil:

Paper Structure We achieve these goals by designing a *mathematically natural core programming language* for safe and correct programming with temporal resources: on the one hand, based on a time-graded, temporal variant of *Fitch-style modal type systems* [19,27], and on the other hand, on *graded monads* [35,51,67].

We review modal types and discuss how we use them to capture temporal resources in §2. In §3, we present λrτs—our modally typed, effectful, equationally presented core calculus for safe programming with temporal resources. We justify the design of λrτs by giving it a mathematically natural sound denotational semantics in §4, based on graded monads and adjunctions between strong monoidal functors, including a concrete presheaf example. In §5, we briefly discuss a specialisation of λrτs with equations for time delays. We review related work and remark on future work in §6, and conclude in §7. This paper is also accompanied by an online appendix (https://arxiv.org/abs/2210.07738) that presents further details of renamings and denotational semantics that we omit in §3 and §4.

For supplementary rigour, we have formalised the main results of §3 and §4 also in Agda [68], available at https://github.com/danelahman/temporalresources/releases/tag/fossacs2023. Regrettably, it currently lacks (i) proofs of some auxiliary lemmas noted in Prop. 4 due to a bug in Agda where withabstractions produce ill-typed terms,1 and (ii) two laws of the presheaf model because unfolding of definitions produces unmanageably large terms for Agda.

## 2 Modal Types for Temporal Resources

We begin with an overview of (Fitch-style) modal type systems and how a timegraded variant of them naturally captures temporal aspects of resources.

1 Eta-contraction is not type-preserving: https://github.com/agda/agda/issues/2732

#### 2.1 (Fitch-Style) Modal Types

A *modal type system* extends the types of an underlying type system with new *modal type formers*, 2 e.g.,˝X, which states that the type is to be considered and reasoned about in a *different mode* compared to X, which can take many forms. For instance, in Kripke's possible worlds semantics, ˝X means that values of type X are *available in all future worlds* [41]; in run-time code generation, the type ˝X captures *generators of* X*-typed code* [72]; and in asynchronous and distributed programming, the type ˝X specifies *mobile* X*-typed values* [3,54,63].

Many different approaches to presenting modal type systems have been developed, with one of the main culprits being the difficulty of getting the *introduction rule* for ˝X correct. Namely, bearing in mind Kripke's possible worlds semantics, the introduction rule for ˝X must allow one to use only those hypotheses that also hold in all future worlds, while at the same time ensuring that the system still enjoys expected structural properties. Solutions to this problem have involved proving ˝X in a context containing only ˝-types [62] (with a failure of structural properties in the naive approaches), or building a form of explicit substitutions into the introduction rule for ˝X to give the rule premise access to only ˝-types [12], or incorporating the Kripke semantics in the type system by explicitly indexing types with worlds [66]—see [37] for an in-depth survey.

In this paper, we build on *Fitch-style modal type systems* [15,19,27,48], where the typing rules for ˝X are given with respect to another modality, - , that acts on contexts, resulting in a particularly pleasant type-theoretic presentation.

As an illustrative example, in a Fitch-style modal type system corresponding to the modal logic S4 (whose Kripke models require the order on worlds to be reflexive and transitive, thus also corresponding to natural properties of time), the typing rules for variables and the ˝X type have the following form:3

$$\begin{array}{c} \stackrel{\text{VAR}}{\longrightarrow} \mathcal{C} \notin \varGamma'\\ \stackrel{\text{\tiny{\tiny{\text{U}}}}{\Gamma, x:X, \Gamma' \vdash x:X}} \end{array} \qquad \begin{array}{c} \stackrel{\text{S\_{\text{HUT}}}{\longrightarrow} \mathcal{C} \text{-} t:X} \\ \stackrel{\text{\tiny{\tiny{\text{O}}}}{\Gamma \vdash t \text{ \text{s}} \text{t} : \square X} \end{array} \qquad \begin{array}{c} \stackrel{\text{\tiny{\text{O}}}{\longrightarrow} t: \square X} \\ \stackrel{\text{\tiny{\text{O}}}{\Gamma \vdash t \text{ \text{ }} \square X} \end{array}$$

Intuitively, the *context modality* creates a barrier in the premise of Shut so that only ˝-typed variables can be used from Γ in t, achieving the abovementioned correctness goal for the introduction rule of ˝X. Alternatively, in the context of Kripke's possible worlds semantics, one can also read the occurrences of the modality as advancing the underlying world—in Shut, t in the premise is typed in some future world compared to where shut t is typed at. This intuition will be useful to how we use a similar modality to capture the passage of time in λrτs. The context weakening Γ, Γ1 in Open ensures the admissibility of structural rules, and in the possible worlds reading, it intuitively expresses that if ˝X is available in some world, then X will be available in all possible future worlds.

2 For brevity, we use the term *modal type system* to interchangeably refer to both modal type systems and natural deduction systems of (intuitionistic) modal logics.

3 Depending on which exact modal logic one is trying to capture, the form of contexts used in the introduction/elimination rules can differ, see [19] for a detailed overview.

## 2.2 Modal Types for Temporal Resources

Next, we give a high-level overview of how we use a time-graded variant of Fitchstyle modal type systems to capture temporal properties of resources in λrτs. For this, we use the production line code snippet from §1 as a working example.

A Naive Approach Before turning to modal types, a naive solution to achieve the desired time delay would be for paint to return the required drying time and for the program to delay execution for that time duration, e.g., as expressed in

let pτdry, body', left-door', right-door'q " paint pbody, left-door, right-doorq in delay τdry; assemble pbody', left-door', right-door'q

It is not difficult to see that we could generalise this solution to allow performing other useful activities while waiting for τdry time to pass. So are we done and can we conclude the paper here? Well, no, because this solution puts all the burden for writing correct code on the shoulders of the programmer, with successful typechecking giving no additional guarantees that τdry indeed will have passed.

A Temporal Resource Type Instead, inspired by Fitch-style modal type systems and Kripke's possible worlds semantics of the ˝-modality, we propose a *temporal resource type*, written rτ s X, to specify that a value of type X will become available for use in *at most* τ time units, or to put it differently, the boxed value of type X can be explicitly unboxed only when *at least* τ time units have passed. Concretely, rτ s X is presented by the following two typing rules:

Box Γ, xτ y \$ V : X Γ \$ boxτ V : rτ s X Unbox τ ď time Γ Γ ´ τ \$ V : rτ s X Γ, x : X \$ N : Y ! τ 1 Γ \$ unboxτ V as x in N : Y ! τ 1

Above, τ s are natural numbers that count discrete time moments, and Y ! τ 1 is a type of computations returning Y -typed values and executing in τ 1 time units.

Analogously to the context modality of Fitch-style modal type systems, we introduce a similar *modality on contexts*, written xτ y, to express that when typechecking a term of the form Γ, xτ y \$ V : X, we can safely assume that *at least* τ time will have passed before V is accessed or executed, as in the premise of the Box rule. Accordingly, in Unbox, we require that at least τ time units have passed since the resource V of type rτ s X was created or brought into scope, by typing V in the "earlier" context Γ ´ τ (we define this operation in §3.3).

Encapsulating temporal resources as a type gives us flexible first-class access to them, and allows to pack them in data structures and pass them to functions.

Modelling Passage of Time As we see in the Unbox rule, we can unbox a temporal resource only when enough time has passed since its creation. This begs the question: How can the passage of time be modelled within the type system? For this, we propose a new notion of *temporally aware graded algebraic effects*, where each operation op is specified not only by its parameter and result types, but also by its prescribed execution time, and with op's continuation knowing that op's worth of additional time has passed before it begins executing. We refer the reader to [8,31,35,60] for background on ordinary (graded) algebraic effects.

For instance, the paint operation, taking τpaint time, is typed in λrτs as4

$$\frac{\begin{array}{c} \Gamma \vdash V : \mathsf{Body} \times \mathsf{Door} \times \mathsf{Door} \\ \Gamma, \langle \tau\_{\mathsf{pair}} \rangle, x : \lceil \tau\_{\mathsf{dry}} \rceil \mathsf{Body} \times \lceil \tau\_{\mathsf{dry}} \rceil \mathsf{Door} \times \lceil \tau\_{\mathsf{dry}} \rceil \mathsf{Door} \vdash M : X \,\mathsf{T} \end{array}}{\begin{array}{c} \Gamma \vdash \mathsf{paint} \; V \; \langle x . M \rangle : X \,\mathsf{fpaint} + \tau \end{array}}$$

Here, xτpainty expresses that from the perspective of any unboxes in M, an *additional* τpaint *time* will have passed compared to the beginning of the execution of paint V px.Mq, which is typed in the "earlier" context Γ. Also, observe that paint's result x is available *after* τpaint time has passed (i.e., after paint finishes), and its type has the car part types wrapped as temporal resources, ensuring that any further operations (e.g., assemble) can access them only after *at least* τdry time has passed *after* paint finishes. The delay τ operation is typed analogously.

Finally, similarly to algebraic operations, we also use the context modality xτ y to model the passage of time in sequential composition, as specified in

$$\frac{\Gamma \vdash M : X \mathrel{!\tau} \qquad \Gamma, \langle \tau \rangle, x : X \vdash N : Y \mathrel{!\tau'}}{\Gamma \vdash \text{let } x = M \text{ in } N : Y \mathrel{!\tau} + \tau'}$$

The type X ! τ (for specifying the execution time of computations) is standard from graded monads style effect systems [35]. The novelty of our work is to use this effect information to inform continuations that they can safely assume that the given amount of additional time has passed before they start executing.

Putting It All Together We conclude this overview by revisiting the production line code snippet and note that in the λrτs-calculus we can write it as

let pbody', left-door', right-door'q " paint pbody, left-door, right-doorq in delay τdry; unbox body' as body" in unbox left-door' as left-door" in unbox right-door' as right-door" in assemble pbody", left-door", right-door"q

Observe that apart from the unbox operations, the code looks identical to the naive, unsafe solution discussed earlier. However, crucially, now any code that wants to use the outputs of paint will typecheck only if these resources are accessed after at least τdry time units have passed after paint finishes. In the code snippet, this is achieved by blocking execution with delay τdry for τdry time units, but this could have been equally well achieved by executing other useful operations op1; ... ; opn, as long as they collectively take at least τdry time.

4 We present λrτs formally using algebraic operations with explicit continuations, while in code snippets we use so-called *generic effects* [59] without explicit continuations.

Time grade: τ P **N** Ground type A, B, C ::" b ˇ ˇ unit ˇ ˇ A ˆ B ˇ ˇ rτ s A Value type X, Y , Z ::" A ˇ ˇ X ˆ Y ˇ ˇ X Ñ Y ! τ ˇ ˇ rτ s X Computation type: X ! τ

Fig. 1. Types of λrτs.

## 3 A Calculus for Programming with Temporal Resources

We now recast the ideas explained above as a formal, modally typed, effectful core calculus, called λrτs. We base it on the fine-grain call-by-value λ-calculus [44].

#### 3.1 Types

The types of λrτs are given in Fig. 1. *Ground types* include base types b, and are closed under finite products and the modal *temporal resource type* rτ s A. The latter denotes that an A-typed value will become available in *at most* τ time units, where τ P **N** counts discrete time moments.5 The ground types can also come with *constants* f with associated *constant signatures* f : pA1,...,Anq Ñ B.

To model operations such as paint and assemble discussed in §2.2, we assume a set of *operations symbols* O, with each op P O assigned an *operation signature* op : Aop - Bop ! τop, which specifies that op accepts inputs of type Aop, returns values of type Bop, and its execution takes τop time units. Observe that by typing operations with ground types, as opposed to simply with base types, we can specify operations such as paint : Part prτdrys Partq!τpaint, returning values that can be accessed only after a certain amount of time, here, after τdry.

*Value types* extend ground types with *function type* X Ñ Y ! τ that specifies functions taking X-typed arguments to computations that return Y -typed values and take τ time to execute, as expressed by the *computation type* Y ! τ .

#### 3.2 Terms

The syntax of terms is given in Fig. 2, separated into values and computations.

*Values* include variables, constants, finite tuples, functions, and the *boxing up of temporal resources*, boxτ V , which allows us to consider an arbitrary value V as a temporal resource as long as it is safe to access V after τ time units.

*Computations* include returning values, sequential composition, function application, pattern-matching6, algebraic operation calls, effect handling, and the *unboxing of temporal resources*, where given a temporal resource V of type rτ s X, 5 For concreteness, we work with p**N**, 0, `, ´9 , ďq for time grades, but we do not foresee

problems generalising these to come from other analogous algebraic structures.

6 The form let px, y, zq " M in N in §1,2 is the natural combination of let and match.

Fig. 2. Values, computations, and effect handlers of λrτs.

the computation unboxτ V as x in N is used to access the underlying value of type X if at least τ time units have passed since the creation of the resource V .

In addition to user-specifiable operation calls (via operation signatures and effect handling), we include a separate delay τ M operation that blocks the execution of its continuation for the given amount of time. For simplicity, we require effect handlers to have *operation clauses* Mop for all op P O, but we do not allow delays to be handled in light of the equations we want of them in §5, where all consecutive delays are collapsed and all zero-delays are removed.

#### 3.3 Type System

We now equip λrτs with a modal type-and-effect system. On the one hand, for modelling temporal resources, we build on Fitch-style modal type systems [19]. On the other hand, for modelling effectful computations and their specifications, we build on type-and-effect systems for calculi based on graded monads [35].

The *typing judgements* are written as Γ \$ V : X and Γ \$ M : X ! τ , where τ specifies M's execution time and Γ is a *temporal typing context*, given by

$$
\Gamma \implies \cdot \mid \quad \Gamma, x:X \mid \quad \Gamma, \langle \tau \rangle \cdot
$$

Here, xτ y is a *temporal context modality*, akin to in Fitch-style systems. We use it to express that when typechecking a term of the form Γ, xτ y \$ V : X, we

#### Values

Fig. 3. Typing rules of λrτs.

can safely assume that *at least* τ time will have passed before the resource V is accessed or executed. The *rules* defining these judgements are given in Fig. 3.

In contrast to Fitch-style modal type systems discussed in §2.1, Var does not restrict the Γ1 right of x to not include any context modalities. This is so because in the possible worlds reading of λrτs (see §4) we treat all types as being monotone for time—this is not usually the case for formulae in modal logics such as S4, but in λrτs this models that once any value is available it will remain so.

As in systems based on graded monads, Return specifies that returning a value takes zero time, and Let that the execution time of sequentially composed computations is the sum of the individual ones. Novel to λrτs, Let, Op, Delay, and Handle state that the continuations can safely assume that relevant amount of additional time has passed before they start executing, as discussed in §2.2.

When typing the operation clauses Mop in Handle, we universally quantify (at the meta-level) over the execution time τ 2 of the continuation k of Mop. We do so as the operation clauses Mop must be able to execute at any point when effect handling recursively traverses M. Further, observe that k is wrapped inside a resource type. This ensures that k is invoked only after τop amount of time has been spent in Mop, thus guaranteeing that the temporal discipline is respected. Note that this enforces a *linear* discipline for our effect handlers: for τop ą 0, k must be executed exactly once for Mop's execution time to match τop ` τ 2.

Finally, Box specifies that in order to box up a value V of type X as a temporal resource of type rτ s X, we must be able to type V when assuming that τ additional time units will have passed before V is accessed. At the same time, Unbox specifies that we can unbox a temporal resource V of type rτ s X only if at least τ time units have passed since its creation: the time captured by Γ must be at least τ , and we must be able to type V in a τ time units "earlier" context Γ ´ τ . The *time captured by a context*, time Γ, is calculated recursively as

time ¨ def " 0 time pΓ, x : Xq def " time Γ time pΓ, xτ yq def " time Γ ` τ

and the *"time travelling" operation* Γ ´ τ as (where τ` " 1 ` τ 2 for some τ 2)

$$\begin{array}{ll} \text{\(\pi\)} \quad \text{\(\pi\)} \quad \text{\(\pi\)} \quad \text{\(\pi\)} \quad \text{\(\pi\)} \quad \text{\(\pi\)} \quad \text{\(\pi\)} \\\ \Gamma - 0 \stackrel{\text{\(\pi\)}}{=} \Gamma \qquad \text{\(\pi\)} \quad \text{\(\pi\)} \quad \text{\(\Gamma, x:X\)} - \tau\_{+} \stackrel{\text{\(af\)}}{=} \Gamma - \tau\_{+} \\\ \Gamma(\Gamma, \langle \tau' \rangle) - \tau\_{+} \stackrel{\text{\(af\)}}{=} \text{\(if } \tau\_{+} \leqslant \tau' \text{ then } \Gamma, \langle \tau' \dashrightarrow \tau\_{+} \rangle \text{ \(\text{else } \Gamma - \langle \tau\_{+} \dashrightarrow \tau' \rangle\)} \end{array}$$

taking Γ to an "earlier" state by removing τ worth of modalities and variables.

#### 3.4 Admissibility of Renamings and Substitutions

We now show that expected *structural* and *substitution rules* [7] are admissible.

Theorem 1. *The typing relations* Γ \$ V : X *and* Γ \$ M : X ! τ *are closed under standard structural rules of weakening, exchange of consecutive variables, and contraction (omitted here). Furthermore, both typing relations are also closed under rules making* x´y *into a strong monoidal functor (with a co-strength) [45]:*

$$\frac{\Gamma, \langle 0 \rangle \vdash J}{\Gamma \vdash J} \quad \frac{\Gamma, \langle \tau\_1 + \tau\_2 \rangle \vdash J}{\Gamma, \langle \tau\_1 \rangle, \langle \tau\_2 \rangle \vdash J} \quad \frac{\Gamma, \langle \tau \rangle \vdash J \quad \tau \leqslant \tau'}{\Gamma, \langle \tau' \rangle \vdash J} \quad \frac{\Gamma, \langle \tau \rangle, x: X \vdash J}{\Gamma, x: X, \langle \tau \rangle \vdash J}$$

*where* Γ \$ J *ranges over both typing relations, where the first two rules hold in both directions, and the last rule expresses that if we can type* J *using a variable "now", we can also type* J *if that variable was brought into scope "earlier".*

*Proof.* First, we define a *renaming relation* ρ : Γ - Γ1 , and then prove by induction that if Γ \$ J and ρ : Γ - Γ1 then Γ1 \$ Jrρs, where Jrρs is J renamed with ρ. The relation is defined as the reflexive-transitive-congruent closure of rules corresponding to the desired structural rules, e.g., varr x:XPΓ : Γ, y : X - Γ and μr : Γ, xτ1 ` τ2y -Γ, xτ1y, xτ2y. The full list is given in the online appendix.

For the Var and Unbox cases of the proof, we show that if ρ : Γ - Γ1 and x Pτ Γ, then ρ x Pτ1 Γ1 for some τ 1 with τ ď τ 1 , where x Pτ Γ means that x P Γ and there is τ worth of modalities right of x in Γ, and ρ x is the variable that ρ maps x to. For Unbox, we further prove that if ρ : Γ - Γ1 , then for any τ

we can build ρ ´ τ : Γ ´ τ - Γ1 ´ τ , using the result about Pτ to ensure that ρ does not map any x P Γ ´ τ outside of Γ1 ´ τ . We also establish that if Γ - Γ1 , then time Γ ď time Γ1 , allowing us to deduce τ ď time Γ1 from τ ď time Γ.

The admissibility of the rules corresponding to μr (and its inverse) relies on us having defined context splitting in Unbox using Γ ´ τ , as opposed to more rigidly as Γ, Γ1 , as in [19], as then it would be problematic if the split happens between xτ1y, xτ2y. Inverses of the last two rules in Thm. 1 are not valid—they would allow unboxing temporal resources without enough time having passed.

Theorem 2. *The typing relations* Γ \$ V : X *and* Γ \$ M : X ! τ *are closed under substitution, i.e., if* Γ, x : X, Γ1 \$ J *and* Γ \$ W : X*, then* Γ, Γ1 \$ JrW{xs*, where* JrW{xs *is standard recursively defined capture-avoiding substitution [7].*

*Proof.* The proof proceeds by induction on the derivation of Γ, x : X, Γ1 \$ J. The most involved case is Unbox, where we construct the derivation of Γ, Γ1 \$ unboxτ V rW{xs as y in NrW{xs : Y ! τ 1 by first analysing whether τ ď time Γ1 , which tells us whether x is in the context pΓ, x : X, Γ1 q´τ of V , based on which we learn whether W continues to be substituted for x in V or whether V rW{xs " V .

## 3.5 Equational Theory

We conclude the definition of λrτs by equipping it with an *equational theory* to reason about program equivalence, defined using judgements Γ \$ V " W : X and Γ \$ M " N : X ! τ , where we presuppose that the terms are well-typed for the given contexts and types. The rules defining these relations are given in Fig. 4. We omit standard equivalence, congruence, and substitutivity rules [7].

The equational theory consists of standard β{η-equations for the unit, product, and function types. We also include monadic equations for return and let [52]. For op and delay, we include algebraicity equations, allowing us to pull them out of let [8]. For handle, we include equations expressing that effect handling recursively traverses a term, replacing each op-occurrence with the operation clause Mop, leaving delays untouched, and finally executes the continuation N when reaching return values [61]. Finally, we include β/η-equations for box and unbox, expressing that unbox behaves as a pattern-matching elimination form for box.

## 4 Denotational Semantics

We justify the design of λrτs by giving it a mathematically natural semantics based on *adjunctions between strong monoidal functors* [45] (modelling modalities) and a *strong*7 *graded monad* [35] (modelling computations). We assume general knowledge of category theory, only spelling out details specific to λrτs. To optimise for space, we discuss the abstract model structure simultaneously with a concrete example using presheaves [46], but note that the interpretation is defined, and its soundness proved, with respect to the abstract structure.

7 To be more specific, we use a modal notion of r´s*-strength* that we define below.

$$() = V: \mathtt{unit} \tag{\eta}$$

$$\text{fun } (x:X) \mapsto Vx \equiv V:X \to Y \mathrel{!} \tau \tag{\eta}$$

$$(\text{fun } (x : X) \twoheadrightarrow M) \, V \equiv M \, [V/x] \tag{\beta}$$

$$\text{match}\ (V, W) \text{ with } \{(x, y) \mapsto N\} \equiv N[V/x, W/y] \tag{\beta}$$

$$\text{match } V \text{ with } \{(x, y) \mapsto N[(x, y)/z] \} \equiv N[V/z] \tag{\eta}$$

$$\text{let } x = \text{(return } V \text{) in } N = N[V/x] \tag{\beta}$$

$$\text{let } y = \text{(let } x = M \text{ in } N\text{) in } P \equiv \text{let } x = M \text{ in } \text{(let } y = N \text{ in } P\text{)}\tag{\beta}$$

$$\text{let } x = M \text{ in return } x \equiv M \tag{\eta}$$

$$\text{let } x = \left(\text{op } V \left(y \cdot M\right)\right) \text{ in } N = \text{op } V \text{ (}y \text{.} \text{ let } x = M \text{ in } N\text{)}\tag{\beta}$$

$$\text{let } x = (\text{delay } \tau \ M) \text{ in } N \equiv \text{delay } \tau \text{ (let } x = M \text{ in } N\text{)}\tag{\beta}$$

$$\text{handle (return } V \text{) with } H \text{ to } x \text{ in } N \equiv N[V/x] \tag{\beta}$$

handle pop V py . Mqq with H to x in N "

$$M\_{\textsf{op}}[V/x, \textsf{box}\_{\tau\_{\textsf{op}}} \left( \text{fun } (y:B\_{\textsf{op}}) \twoheadrightarrow \textsf{handle} \left. M \text{ with } H \text{ to } x \text{ in } N \right) / k] \tag{\beta}$$

$$\text{Random (delay } \tau \text{ } M \text{) with } H \text{ to } x \text{ in } N \equiv \text{delay } \tau \text{ (handle } M \text{ with } H \text{ to } x \text{ in } N\text{)}\tag{\beta}$$

$$\mathsf{unbox}\_{\tau} \text{ (}\mathsf{box}\_{\tau} V\text{) as } x \text{ in } N \equiv N[V/x] \tag{\beta}$$

$$\mathtt{unbox}\_{\tau} \; V \; \mathtt{as} \; x \; \text{in} \; N[\mathtt{box}\_{\tau} \; x/y] \coloneqq N[V/y] \tag{\eta}$$

Fig. 4. Equational theory of λrτs.

When referring to the *abstract model structure*, we denote the underlying category with **C**. Meanwhile, the *concrete presheaf example* is given in Setp**N**,ďq, consisting of functors from p**N**, ďq to the category Set of sets and functions.

The model in Setp**N**,ďq is similar to Kripke's possible worlds semantics, except that in Setp**N**,ďq all objects are *monotone* for ď, i.e., for any A P Setp**N**,ďq we have functions Apt1 ď t2q : Apt1q Ñ Apt2q respecting reflexivity and transitivity, whereas Kripke models are commonly given by discretely indexed presheaves and only modalities change worlds. For λrτs, working in Setp**N**,ďq gives us that when a resource becomes available, it will remain so without need for reboxing, leading to a more natural system for temporal resources and a simpler Var rule.

#### 4.1 Interpretation of Types

Value Types and Contexts To interpret value types, we require the category **C** to have *finite products* p**1**, A ˆ Bq and *exponentials* A ñ B, so as to model the unit, product, and function types. In Setp**N**,ďq, the former are given pointwise using the finite products in Set, and the latter are given as pA ñ Bqptq def " Setp**N**,ďqphom t ˆ A, Bq, where hom t : p**N**, ďq Ñ Set is the covariant *hom-functor* for p**N**, ďq, given by hom t def " t ď p´q [46]. When unfolding it further, the above means that pA ñ Bqptq is the set of functions pft1 : Apt 1 q Ñ Bpt 1 qqt1Ptt1P**N**|tďt1u that are natural in t 1 , capturing the intuition that in λrτs functions can be applied in any future context. For base types, we require an object rrbss of **C** for each b.

To interpret the temporal resource type, we require a *strong monoidal functor* r´s : p**N**, ďq Ñ r**C**, **C**s, where r**C**, **C**s is the category of endofunctors on **C**. This means that we have functors rτ s : **C** Ñ **C**, for all τ P **N**, together with morphisms rτ1 ď τ2sA : rτ1sA Ñ rτ2sA, natural in A and respecting ď. Strong monoidality of r´s means that we have natural isomorphisms εA : r0sA – Ñ A and δA,τ1,τ2 : rτ1 ` τ2sA – Ñ rτ1sprτ2sAq, satisfying time-graded variants of comonad laws [10]:

$$\varepsilon \circ \delta\_{A,0,\tau} \equiv \mathrm{id} \qquad \left[\tau\right](\varepsilon) \circ \delta\_{A,\tau,0} \equiv \mathrm{id} \qquad \delta\_{\left[\tau\_3\right]A,\tau\_1,\tau\_2} \circ \delta\_{A,\tau\_1+\tau\_2,\tau\_3} \equiv \left[\tau\_1\right](\delta) \circ \delta$$

We also require pδA,τ1,τ2 , δ´1 A,τ1,τ2 q to be monotone in τ1, τ2, i.e., if τ1 ď τ 1 1 and τ2 ď τ 1 2, then rτ 1 1sprτ2 ď τ 1 2sq ˝ rτ1 ď τ 1 1s ˝ δ " δ ˝ rτ1 ` τ<sup>2</sup> ď τ <sup>1</sup> <sup>1</sup> ` τ 1 2sA. We omit the indices of the components of natural transformations when convenient.

In Setp**N**,ďq, we define prτ sAqptq def " Apt ` τ q, with rτ sA-values given by future A-values, and with pεA, ε´1 A , δA, δ´1 A q given by identities on A-values, combined with the laws of p0, `q, e.g., as pεAq<sup>t</sup> ` a P pr0sAqptq " Apt ` 0q ˘ def " a P Aptq.

Using the above, we interpret a value type X as an object rrXss of **C**, as

$$\begin{aligned} \left\lbrack \begin{bmatrix} A \\ \end{bmatrix} \stackrel{\text{def}}{=} \left\lbrack \begin{bmatrix} A \\ \end{bmatrix} \right\rbrack^g & \qquad \left\lbrack \begin{bmatrix} \mathsf{unit} \\ \end{bmatrix} \right\rbrack \stackrel{\text{def}}{=} \mathbb{1} & \qquad \left\lbrack \begin{bmatrix} X \times Y \\ \end{bmatrix} \stackrel{\text{def}}{=} \left\lbrack \begin{bmatrix} X \\ \end{bmatrix} \right\rbrack \times \left\lbrack \begin{bmatrix} Y \\ \end{bmatrix} \right\rbrack \\ \left\lbrack \begin{bmatrix} X \to Y \end{bmatrix} \stackrel{\text{def}}{=} \left\lbrack \begin{bmatrix} X \\ \end{bmatrix} \right\rbrack & \qquad \left\lbrack \begin{bmatrix} \tau \end{bmatrix} \begin{bmatrix} X \\ \end{bmatrix} \right\rbrack \stackrel{\text{def}}{=} \left\lbrack \begin{bmatrix} \tau \end{bmatrix} \right\rbrack \end{aligned}$$

where T is a graded monad for modelling computations—we return to it below. The interpretation of ground types rrAssg is defined similarly, so we omit it here.

Next, we define the interpretation of contexts, for which we require another *strong monoidal functor*, x´y : p**N**, ďqop Ñ r**C**, **C**s. Note that x´y is *contravariant*—this enables us to model the structural rules that allow terms typed in an earlier context to be used in future ones (see Thm. 1). We denote the strong monoidal structure of x´y with ηA : A – Ñ x0yA and μA,τ1,τ2 : xτ1ypxτ2yAq – Ñ xτ1 `τ2yA, required to satisfy time-graded variants of monad laws [45], given by

$$\mu\_{A,0,\tau} \circ \eta \equiv \text{id} \qquad \mu\_{A,\tau,0} \circ \langle \tau \rangle(\eta) \equiv \text{id} \qquad \mu\_{A,\tau\_1+\tau\_2,\tau\_3} \circ \mu\_{\langle \tau\_3 \rangle A,\tau\_1,\tau\_2} \equiv \mu \circ \langle \tau\_1 \rangle(\mu)$$

and pμA,τ1,τ2 , μ´1 A,τ1,τ2 q have to be monotone in τ1, τ2, similarly to pδ, δ´1q above. In Setp**N**,ďq, we define pxτ yAqptq def " pτ ď tq ˆ Apt ´9 τ q, as past A-values, with

the *side-condition* τ ď t crucial for the existence of the adjunctions xτ y%rτ s we require below. We define pηA, η´1 A , μA, μ´1 A q similarly to earlier, as identities on A-values, combined with the laws of p0, `, ´q9 , so as to satisfy the side-conditions.

With this, we can interpret *contexts* Γ as *functors* rrΓss : **C** Ñ **C**, given by:

$$\|\lnot\|A \stackrel{\text{def}}{=} A \qquad \|\lnot T, x: X\|\\A \stackrel{\text{def}}{=} \|\lnot\| \|A \times \|\lnot\|\\\|\ell' \langle \tau \rangle\| \|A \stackrel{\text{def}}{=} \langle \tau \rangle (\|\!\|I\| \|A)$$

We interpret contexts as functors to easily manipulate denotations of composite contexts, e.g., we then have ιΓ;Γ1;A : rrΓ, Γ1 ssA – Ñ rrΓ1 ssprrΓssAq, natural in A.

Finally, to formulate the semantics of computation types and terms, we require there to be a family of *adjunctions* xτ y%rτ s, i.e., natural transformations η% A,τ : A Ñ rτ spxτ yAq (the *unit*) and ε% A,τ : xτ yprτ sAq Ñ A (the *counit*), for all τ P **N**, satisfying time-graded variants of standard adjunction laws [45], given by

$$\iota\_{\langle \tau \rangle A, \tau}^{\dashv} \circ \langle \tau \rangle (\eta\_{A, \tau}^{\dashv}) \equiv \mathsf{id} \qquad [\tau] (\varepsilon\_{A, \tau}^{\dashv}) \circ \eta\_{\{\tau\} A, \tau}^{\dashv} \equiv \mathsf{id}$$

We also require pη%, ε%q to interact well with the strong monoidal structures:

$$\begin{aligned} \left[\tau\right](\left(0\leqslant\tau\right))\circ\eta\_{A,\tau}^{\dashv}\circ\eta^{-1}\circ\varepsilon &= \left[0\leqslant\tau\right] \quad & \left[\tau\_1\right](\left[\tau\_2\right](\mu))\circ\left[\tau\_1\right](\eta\_{\left<\tau\_1\right>A,\tau\_2}^{\dashv})\circ\eta\_{A,\tau\_1}^{\dashv} = \delta\circ\eta^{-1} \\ \left<0\right>(\left[0\leqslant\tau\right])\circ\eta\circ\varepsilon^{-1}\circ\varepsilon\_{A,\tau}^{\dashv} &= \left<0\leqslant\tau\right>\quad\varepsilon\_{A,\tau\_1}^{\dashv}\circ\left<\tau\_1\right](\varepsilon\_{\left[\tau\_1\right]A,\tau\_2}^{\dashv})\circ\left<\tau\_1\right>(\leftlangle\tau\_2\right>\delta) = \varepsilon^{\dashv}\circ\mu \end{aligned}$$

Proposition 1. *It then follows that* η% A,0 " ε´1 x0yA ˝ ηA *and* ε% A,0 " εA ˝ η´1 r0sA*.*

In Setp**N**,ďq, η% A,τ and ε% A,τ are given by identities on A-values, respectively combined with τ ď t ` <sup>τ</sup> and monotonicity for <sup>p</sup><sup>t</sup> ´<sup>9</sup> <sup>τ</sup> q ` τ " t. For the latter, we crucially know τ ď t due to the side-condition included in the definition of x´y.

We note that modulo the time grades τ , the above structure is analogous to the models of the Fitch-style presentation of S4 [19], where ˝ is modelled by an idempotent comonad, by an idempotent monad, and boxing/unboxing by -% ˝. This is also why we present r´s and x´y as comonad- and monad-like.

Computation Types For computation types, we require a r´s*-strong graded monad* pT,ηT , μT ,strT q on **C**, with grades in **N**. 8 In detail, this means a functor T : **N** Ñ r**C**, **C**s, together with natural transformations ηT A : A Ñ T 0 A (the *unit*), μT A,τ1,τ2 : T τ1pT τ2 Aq Ñ T pτ1 ` τ2q A (the *multiplication*), and strT A,B,τ : rτ sAˆTBτ Ñ T pAˆBq τ (the *strength*), with the first two satisfying standard graded monad laws (see [35] or pη, μq of x´y). Below we only present the laws for strT because it has a novel temporal aspect to it—its first argument appears under rτ s. As such, strT expresses that if we know an A-value will be available after τ time units, we can push it into computations taking τ -time to execute.

We say that T is a r´s-strong graded monad following the parlance of Bierman and de Paiva [12]—in their work they model the possibility modality ˛A as a ˝-strong monad. While the laws governing strT are not overly different from standard graded strength laws [35], we have to correctly account for r´s in them

$$\begin{aligned} \mathsf{str}\_{A,B,0}^T \circ (\varepsilon\_A^{-1} \times \eta\_A^T) &\equiv \eta\_{A \times B}^T \quad \mu\_{A \times B, \tau\_1, \tau\_2}^T \circ T \, (\mathsf{str}^T) \circ \mathsf{str}^T \equiv \mathsf{str}^T \circ (\delta^{-1} \times \mu^T) \\ T \, (\mathsf{nsd}) \circ \mathsf{str}\_{A,B,\tau}^T &\equiv \mathsf{nsd} \quad T \, (\alpha) \circ \mathsf{str}^T \circ (\mathsf{m} \times \mathsf{id}) \circ \alpha^{-1} \equiv \mathsf{str}\_{A,B \times C,\tau}^T \circ (\mathsf{id} \times \mathsf{str}^T) \end{aligned}$$

where αA,B,C : pAˆBqˆC – Ñ AˆpBˆCq, and mA,B,τ : rτ sAˆrτ sB Ñ rτ spAˆBq witnesses that rτ s is monoidal for ˆ, which follows from rτ s being a right adjoint [45]. Observe that it is the r´s-strength that naturally gives T a temporal flavour—the rest of it is standard [35]. Below we show that strT is also mathematically natural, admitting an analogous characterisation to ordinary strength.

8 As λrτs does not include sub-effecting (see §6.2), a discretely graded monad T suffices.

Proposition 2. *Analogously to ordinary strong and enriched monads [39],* T *having* r´s*-strength is equivalent to* r´s-enrichment *of* T*, given by morphisms* rτ spA ñ BqÑpTτA ñ TτBq *respecting* **C***'s self-enrichment [38] and* pηT , μT q*.*

In order to model operations op and delay in §4.2, we require T to be equipped with *algebraic operations*: we ask there to be families of natural transformations opT A,τ : rrAopssg ˆ rτopsprrBopssg ñ TτAq Ñ T pτop ` τ q A, for all op : Aop - <sup>B</sup>op ! <sup>τ</sup>op <sup>P</sup> <sup>O</sup>, and delay<sup>T</sup> A,τ<sup>1</sup> τ : rτ spT τ <sup>1</sup> Aq Ñ T pτ `τ 1 q A, for all τ P **N**, satisfying algebraicity laws [61], which state that both commute with μT and strT , e.g.,

$$\mathsf{str}\_{A,B,\tau+\tau'}^T \circ (\mathsf{id} \times \mathsf{del} \mathsf{ay}^T \tau) \equiv \mathsf{del} \mathsf{ay}\_{A \times B,\tau'}^T \tau \circ [\tau](\mathsf{str}^T) \circ \mathsf{m} \circ (\delta\_{A,\tau,\tau'} \times \mathsf{id})$$

In Setp**N**,ďq, we can define T as the initial algebra of a corresponding signature functor for operations op and delay, analogously to the usual treatment of algebraic effects [8]. Concretely, such T is determined inductively by three cases

$$\frac{a \in A(t)}{\text{ret}\,a \in (T \, 0 \, A)(t)} \quad \frac{k \in (\left[\tau\_{\text{op}}\right] \big(\left[B\_{\text{op}}\right] \big)^{g} \Rightarrow T \,\tau \,A\big))(t)}{\text{op}\,a \,k \in (T \, \left(\tau\_{\text{op}} + \tau\right)A)(t)} \quad \frac{k \in \left[\tau\right](T \, \tau' A)(t)}{\text{del}\,\text{ay} \,\tau \,k \in (T \, \left(\tau + \tau'\right)A\right)(t)}$$

with pηT , μT ,strT , opT , delayT q defined in the expected way, e.g., strT is given by recursively traversing a computation of type TτB and moving the argument of type rτ sA under ret cases, modifying τ when going under the op and delay cases.

#### 4.2 Interpretation of Value and Computation Terms

The interpretation of values and computations is defined simultaneously. We only present the temporally interesting cases—full details are in the online appendix.

As λrτs does not have sub-effecting and includes enough type annotations for typing derivations to be unique, this interpretation is *coherent* by construction.

Values We assume a morphism rrfss : rrA1ssg ˆ ... ˆ rrAnssg Ñ rrBssg for every f : pA1,...,Anq Ñ B. We interpret a well-typed value Γ \$ V : X as a morphism rrΓ \$ V : Xss : rrΓss**1** Ñ rrXss in **C** by induction on the given typing derivation.

Most of the value cases are standard, and analogous to other calculi based on fine-grain call-by-value [44] and graded monads [35], using the Cartesian-closed structure of **C**. The temporally interesting cases are Var and Box, given by

$$\begin{aligned} \left\| \left[ \Gamma, x:X, I' \vdash x:X \right] \right\| \stackrel{\text{def}}{=} \left\| \left[ \Gamma, x:X, I' \right] \right\| \mathbb{1} \stackrel{\iota}{\longrightarrow} \left\| \left[ I' \right] \right\| \mathbb{1} \times \left\| \left[ X \right] \right\| \\ \stackrel{\stackrel{\bullet}{\longrightarrow}}{\longrightarrow} \left\langle \text{time } I' \right\rangle \Big( \left\| I' \right\| \mathbb{1} \times \left\| X \right\| \Big) \stackrel{\iota^{\triangleleft}}{\longrightarrow} \left\| \left[ I' \right] \mathbb{1} \times \left\| X \right\| \stackrel{\text{snd}}{\longrightarrow} \left\| X \right\| \Big) \end{aligned}$$

rrΓ \$ boxτ V : rτ s Xss def " rrΓss**1** η% ´ÝÑ rτ s ` xτ yprrΓss**1**q ˘ rτsprrV ssq ´´´ÝÑ rτ srrXss

where eA,Γ : rrΓssA Ñ xtime ΓyA extracts and collapses all temporal modalities in Γ, and the counit-like ε xy A,τ is given by the composite xτ yA x0ďτyA ´´´Ñ x0yA η´1 A ´Ñ A. Computations We interpret a well-typed computation Γ \$ M : X ! τ as a morphism rrΓ \$ M : X ! τ ss : rrΓss**1** Ñ T τ rrXss in **C** by induction on the typing derivation. The definition is largely unsurprising and follows a pattern similar to [35,44]—the novelty lies in controlling the occurrences of x´y and r´s.

In Let, we use xτ y%rτ s to push the environment "into the future", and then follow the standard monadic strength-followed-by-multiplication pattern [35,52]:

rrΓ \$ let x " M in N : Y ! τ ` τ <sup>1</sup> ss def " rrΓss**<sup>1</sup>** xη%,rrMssy ´´´´ÝÑ rτ s ` xτ yprrΓss**1**q ˘ ˆ T τ rrXss strT ´ÝÑ T τ ` <sup>x</sup><sup>τ</sup> yprrΓss**1**q ˆ rrXss˘ <sup>T</sup> prrNssq ´´´´ÝÑ T τ <sup>p</sup>T τ <sup>1</sup> rr<sup>Y</sup> ssq <sup>μ</sup><sup>T</sup> ´ÝÑ T pτ ` τ 1 q rrY ss

An analogous use of xτ y%rτ s also appears in the cases for operations, e.g., in

$$\begin{array}{c} \left\| \begin{array}{l} \Gamma \vdash \mathsf{op} \, V \; (x . M) : X \ \mathsf{I} \; \tau\_{\mathsf{op}} + \tau \end{array} \right\| \stackrel{\mathsf{def}}{=} \left\| \begin{array}{l} \Pi \end{array} \right\| \mathbb{1} \xrightarrow{\langle \Pi \| \mathsf{I} \; \eta^{-} \rangle} \left\| \begin{array}{l} A\_{\mathsf{op}} \right\| \mathbb{g}^{g} \times \left[ \tau\_{\mathsf{op}} \right] \left( \langle \tau\_{\mathsf{op}} \rangle (\| \Gamma \| \mathsf{I} \rangle) \right) \end{array} \right\| \end{array}$$

$$\stackrel{\mathsf{id} \times \left\| \tau\_{\mathsf{op}} \right\| \left( \mathsf{curl} \, \eta \right) \left\| \begin{array}{l} \Pi \mathsf{a} \mathsf{p} \end{array} \right\| \right\| ^{g} \times \left\| \tau\_{\mathsf{op}} \right\| \left( \left\| \mathsf{I} \; \mathsf{a} \mathsf{p} \right\| \right) \stackrel{\mathsf{op}^{T}}{\Longrightarrow} T \, \tau \left\| \begin{array}{l} X \end{array} \right\| \stackrel{\mathsf{op}^{T}}{\longrightarrow} T \, \left( \tau\_{\mathsf{op}} + \tau \right) \left\| X \right\| \, \mathsf{I} \; \eta \end{array}$$

Next, the Unbox case of the interpretation is defined as

$$\begin{aligned} \left\| I \vdash \text{unbox}\_{\tau} \; V \; \text{as } x \text{ in } N: Y \; ! \; \tau' \right\| & \stackrel{\text{def}}{=} \left\| I \right\| \mathbb{1} \xrightarrow{\langle \mathbf{d}, \eta^{\text{PAR}} \rangle} \left\| I \right\| \mathbb{1} \times \left\langle \tau \right\rangle \left( \left\| I \; \tau - \tau \right\| \mathbb{1} \right) \\ & \xrightarrow{\left\| \mathbf{d} \times \langle \tau \rangle (\left\| I \right\| \mathbb{1}) \right\|} \left\| I \right\| \mathbb{1} \times \left\langle \tau \right\rangle (\left\| \left\| I \right\| \mathbb{1}) \xrightarrow{\left\| \mathbf{d} \times \mathbf{c}^{-i} \right\|} \left\| I \right\| \mathbb{1} \times \left\| \left\| X \right\| \xrightarrow{\left\| N \right\|} T \; \tau' \left\| \left\| Y \right\| \end{aligned} $$

showing that temporal resources follow the common pattern in which elimination forms are modelled by counits of adjunctions, whereas units model introduction forms (akin to functions). The morphism ηPRA Γ,A,τ : rrΓssA Ñ xτ yprrΓ ´ τ ssAq extracts and collapses τ worth of context modalities in Γ, as long as τ ď time Γ. It is a semantic counterpart to an observation that the context modality Γ, xτ y is a *parametric right adjoint* to the Γ ´ τ operation, as in recent dependently typed presentations of Fitch-style modal types [27], see §6.1 for further discussion.

Finally, we discuss the interpretation of effect handling. For this, we additionally require **C** to have *set-indexed products* ΠiPIAi and *handling morphisms*

$$\begin{aligned} \left( \chi\_{A,\tau,\tau'} : \Pi\_{\mathsf{op}\in\mathsf{C}} \Pi\_{\tau'' \in \mathbb{N}} \left( (\left\| A\_{\mathsf{op}} \right\| ^g \times \left\{ \tau\_{\mathsf{op}} \right\} (\left\| B\_{\mathsf{op}} \right\| ^g \Rightarrow T \,\tau'' \, A) \right) & \Rightarrow T \left( \tau\_{\mathsf{op}} + \tau'' \right) \, A \right) \\ & \qquad \to T \,\tau \left( T \,\tau' \, A \right) \Rightarrow T \left( \tau + \tau' \right) \, A \end{aligned}$$

satisfying laws which state that χA returns a graded T-algebra [22,50], e.g., we require uncurrypχA,0,τ1q˝pid ˆ ηT q " snd, where uncurry (and curry earlier) is part of the universal property of A ñ B. We also require similar laws for χ's interaction with opT and delayT . In Setp**N**,ďq, χ is defined by recursively traversing a given tree, replacing all occurrences of op a k with respective operation clauses.

Writing H for the domain of χrrY ss,τ,τ1 , the Handle case is then defined as

rrΓ \$ handle M with H to x in N : Y ! τ ` τ 1 ss def "

$$\begin{split} \llbracket \llbracket I' \rrbracket \rrbracket & \xrightarrow{\langle \mathrm{id}, \langle \gamma^{\top}, \llbracket \mathrm{I} \rrbracket \rrbracket \rangle \rangle} & \llbracket I' \rrbracket \rrbracket \rrbracket \, \mathbbm{1} \times \left( [\tau] \big( (\tau) (\llbracket I' \rrbracket \rrbracket \rrbracket) \rangle \times T \tau \llbracket \rrbracket X \rrbracket \right) \\ & \xrightarrow{\mathrm{id} \times \mathrm{str}^{T}} \llbracket I' \rrbracket \rrbracket \, \mathbbm{1} \times T \tau \left( (\tau) (\llbracket I' \rrbracket \rrbracket \rrbracket) \times \llbracket X \rrbracket \right) \xrightarrow{\mathrm{id} \times T \tau \left( \llbracket I' \rrbracket \rrbracket \rrbracket \right)} & \llbracket I' \rrbracket \rrbracket \, \mathbbm{1} \times T \tau \left( T \tau' \llbracket \rrbracket Y \rrbracket \right) \\ & \xrightarrow{\llbracket \rrbracket^{H} \rrbracket \rrbracket \, \mathbbm{1} \times \mathrm{id}} \mathcal{H} \times T \tau \left( T \tau' \llbracket \rrbracket Y \rrbracket \right) \xrightarrow{\mathrm{non carry} \langle \chi\_{\llbracket \mathrm{I} \rrbracket \rrbracket, \tau, \tau' \rrbracket}} T \left( \tau + \tau' \right) \llbracket Y \rrbracket \end{split}$$

where we write rrHss for the point-wise interpretation of operation clauses

$$\{\llbracket\Gamma\rrbracket\rrbracket \: \xrightarrow{\langle\langle\mathrm{id}\rangle\_{\tau''\in\mathbb{N}}\rangle\_{\mathrm{op}\in\mathcal{O}}} \Pi\_{\mathrm{op}\in\mathcal{O}}\Pi\_{\tau''\in\mathbb{N}}\Big(\llbracket\Gamma\rrbracket\Vert\mathbb{1}\Big{)\xrightarrow{\Pi\_{\mathrm{op}\in\mathcal{O}}\,\Pi\_{\tau''\in\mathbb{N}}\Big{(}\mathrm{curry}\,\{\llbracket\mathrm{M\_{\mathrm{op}}\,\tau''\}\|\diamond\alpha^{-1}\}\Big{)}}\mathcal{H}$$

### 4.3 Renamings, Substitutions, and Soundness

We now show how syntactic renamings and substitutions relate to semantic morphism composition, using which we then prove the interpretation to be *sound*.

Proposition 3. *Given* ρ : Γ - Γ1 *and* Γ \$ J*, then* rrJrρsss " rrJss ˝ rrρss**1***, where the interpretation of renamings* rrρssA : rrΓ1 ssA Ñ rrΓssA *is defined by induction on the derivation of* ρ : Γ - Γ1 *, with the morphism* rrρssA *also natural in* A*.*

Proposition 4. *Given* Γ, x : X, Γ1 \$ J *and* Γ \$ W : X*, we have* rrJrW{xsss " rrJss ˝ ι ´1 Γ,x:X;Γ1;**1** ˝ rrΓ1 ss` xid,rrWssy˘ ˝ ιΓ;Γ1;**1***, where* pι, ι´1q *are discussed in §4.1.*

*Proof.* We prove both results by induction on the derivation of Γ \$ J. The proofs are unsurprising but require us to prove auxiliary lemmas about recursively defined renamings and semantic morphisms. For example, for Prop. 3, we show ηPRA ˝rrρss " xτ yprrρ´τ ssq˝ηPRA : rrΓ1 ssA Ñ xτ yprrΓ ´τ ssAq, and for Prop. 4, that ηPRA ˝ ι " xτ y ` ι ˘ ˝ ηPRA : rrΓ, Γ<sup>1</sup> ssA Ñ xτ y ` rrΓ1 ´ τ ssprrΓssAq ˘ , when τ ď time Γ1 .

Theorem 3. *Given* Γ \$ I " J *derived using the rules in §3.5, then* rrIss " rrJss*.*

*Proof.* The proof proceeds by induction on the derivation of Γ \$ I " J, using Prop. 3 and Prop. 4 to unfold the renamings and substitutions in the equations of §3.5, and using the properties of the abstract structure we required **C** to have.

## 5 Quotienting Delays

Observe that in λrτs the computations delay τ pdelay τ 1 Mq and delay pτ ` τ 1 q M cannot be proved equivalent, though in some situations this might be desired.

In order to deem the above two programs (and others alike) equivalent, we extend λrτs's equational theory with the following natural equations for delays:

$$\text{delay } 0 \, M \equiv M \qquad \text{delay } \tau \text{ (delay } \tau' \, M) \equiv \text{delay } (\tau + \tau') \, M$$

Theorem 4. *If the algebraic operations* delayT *of* T *satisfy analogous two equations, the interpretation of §4 is sound for this extended equational theory.*

For the concrete model in Setp**N**,ďq, we have to *quotient* T [36] by these two equations—the resulting graded monad is determined inductively by the cases

$$\frac{k \in (S \, \tau \, A)(t)}{\mathtt{comp} \, k \in (T \, \tau \, A)(t)} \quad \frac{\tau > 0 \qquad k \in [\tau](S \, \tau' \, A)(t)}{\mathtt{delay} \, \tau \, k \in (T \, (\tau + \tau') \, A)(t)}$$

$$\frac{a \in A(t)}{\mathtt{rect} \, a \in (S \, 0 \, A)(t)} \quad \frac{a \in [\|A\_{\textsf{op}}\|]^g(t)}{\mathtt{copy} \, a \in (S \, (\tau\_{\textsf{op}} + \tau) \, A)(t)} \quad \mathtt{if } a \, b \in (S \, (\tau\_{\textsf{op}} + \tau) \, A)(t)$$

where pTτAqptq and pSτAqptq are defined simultaneously in such a way that only non-zero, non-consecutive delays can appear in the tree structure.

## 6 Related and Future Work

#### 6.1 Related Work

We contribute to two prominent areas: (i) modal types and (ii) graded monads.

As noted in §2.1, *modal types* provide a mathematically natural means for capturing many aspects of programming. Adding to §2.1, types corresponding to the *eventually* and *always modalities* of temporal logics capture *functional reactive programming (FRP)* [18,32,42], including a combination with linearity and time-annotations to model resources [33], where *all* values are annotated with inhabitation times. Recently, FRP has also been studied in Fitch-style [6]. Starting with Nakano [55], modal types have also been used for *guarded recursion*, even in the dependently typed setting [5,14,47], including in Fitch-style [13].

We also note that λrτs's time grades τ and the Γ ´ τ operation are closely related to recent dependently typed Fitch-style frameworks. Namely, [28] develops a *multimodal type theory* (MTT) where types rμsX are indexed by 1-cells μ of a strict 2-category (a mode theory). The time grades τ of λrτs are an example of such mode theories, given by the delooping of **N**, i.e., by a single 0-cell, τ s as 1-cells, and τ ď τ 1 s as 2-cells. While ensuring the admissibility of and naturality under substitutions, MTT with its indirect elimination rule for rμsX is weaker than earlier systems (such as [13]). The direct-style elimination rule is recovered in [27] by observing that in addition to Γ, xμy being a left adjoint to rμsX, it should further form a *parametric right adjoint (PRA)* [17,71] to contexts of the form Γ{pr : μq, where r is a substitution ¨, xμy - Γ. The operation Γ ´ τ in λrτs is an instance of this: μ is a τ , r corresponds to the condition τ ď time Γ in Unbox, contexts Γ{pr : μq are given by Γ ´ τ , and the PRA situation is witnessed by renamings ppΓ ´ τ q, xτ yq - Γ, when τ ď time Γ, and Γ ppΓ, xτ yq ´ τ q.

*Graded monads* provide a uniform framework for different effect systems and effect-based analyses [22,35,36,50,51]. A major contribution of ours is showing that context modalities can inform continuations of preceding computations' effects. While the theory of graded monads can be instantiated with any ordered monoid, we focus on natural numbers to model time, but do not expect complications generalising λrτs to other structures with same properties as p**N**, 0, `, ´9 , ďq, and perhaps even to grading T and x´y, r´s with different structures, akin to [23].

Our use of rτ s X to restrict when resources are available is somewhat reminiscent of *coeffects* [16,24,57,58] and *quantitative type systems* [4,49,53]. In these works, variables are graded by (semi)ring-valued rs, as x :r X, counting how many times and in which ways x is used, enabling applications such as liveness and dataflow analyses [57]. Semantically, these systems often interpret x :r X using a graded comonad, as ˝rX, where one can access X only if r " 1. Of such works, the closest to ours is that of Gaboardi et al. [23], who combine coeffects with effectful programs via distributive laws between the grades of coeffects and effects, allowing coeffectful analyses to be propagated through effectful computations.

We also note that the type rτ s X can be intuitively also viewed as a temporallygraded variant of *promise types* [29,65], in that it expresses that a value of type X will be available in the future, but with additional time guarantees.

#### 6.2 Future Work

Currently, λrτs does not support *sub-effecting*: we cannot deduce from τ ď τ 1 and Γ \$ M : X ! τ that Γ \$ M : X ! τ 1 . Of course, we can simulate this by inserting τ 1 ´9 τ worth of explicit delays into M, but this is extremely intensional, fixing where delays happen. In particular, we cannot type equations such as let x " preturn V q in N " NrV {xs if return V was sub-effected to τ ą 0, with the xτ y in N's context the culprit. However, when considering sub-effecting as a *coercion* coerceτďτ1 M, we believe we can add it by considering equations stating that it will produce *all the possible ways* how τ 1 ´9 τ worth of delays could be inserted into M. Of course, this will require a more complex non-deterministic semantics.

It would be neat if λrτs also included *recursion* in a way that programs could make use of the temporal discipline. This is likely unattainable for general recursion, but we hope that *primitive recursion* (say, on natural numbers) can be added via *type-dependency* of time grades τ on the values being recursed on.

It would be interesting to combine λrτs with linear [25] and separation logics [34,64] to model *linear* and *spatial properties* of temporal resources. Another goal would be to add *concurrency*, e.g., using (multi)handlers [9,20,21]. We also plan to look into capturing *expiring* and *available-for-an-interval* style resources.

Further, we plan to study λrτs's *operational semantics*, namely, one that takes time seriously and does not model delays simply as uninterpreted operations [9], together with developing a *prototype*, and proving *normalisation* akin to [26,69].

We also plan to study the *completeness* of the denotational semantics of λrτs. For such semantic investigations, it could be beneficial to also study the general theory of the kinds of temporally aware graded algebraic effects used in this paper, by investigating their *algebras* and *equational presentations* [36,50].

## 7 Conclusion

We have shown how a temporal, time-graded variant of Fitch-style modal type systems, when combined with an effect system based on graded monads, provides a natural framework for safe programming with temporal resources. To this end, we developed a modally typed, effectful, equationally-presented core calculus, and equipped it with a sound denotational semantics based on strong monoidal functors (for modelling modalities) and graded monads (for modelling effects). The calculus also includes temporally aware graded algebraic effects and effect handlers, with the continuations of the former knowing that an operation's worth of additional time has passed before they start executing, and where the userdefined effect handlers are guaranteed to respect this temporal discipline.

*Acknowledgements* We thank Andrej Bauer, Juhan-Peep Ernits, Niccolò Veltri, and Niels Voorneveld for useful discussions. We also thank one of the reviewers for drawing our attention to the recent work on presenting Fitch-style modal types in terms of parametric right adjoints, and its relationship to the work presented in this paper. This material is based upon work supported by the Air Force Office of Scientific Research under award number FA9550-21-1-0024.

## References

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

## **Deciding Contextual Equivalence of** ν**-Calculus with Effectful Contexts**

Daniel Hirschkoff1, Guilhem Jaber2(), and Enguerrand Prebet1

1 Universit´e de Lyon, ENS de Lyon, UCB Lyon 1, CNRS, INRIA, LIP, France 2 Nantes Universit´e, LS2N, Inria, France<EMAIL_ADDRESS>
**Abstract.** We prove decidability for contextual equivalence of the λμνcalculus, that is the simply-typed call-by-value λμ-calculus equipped with booleans and fresh name creation, with contexts taken in λμref, that is λμν-calculus extended with higher-order references.

The proof exploits a labelled transition system capturing the interactions between λμν programs and λμref contexts. The induced bisimulation equivalence is characterized as equality of certain trees, inspired by the work of Lassen. Since these trees are computable and finite, decidability follows. Bisimulation coincides also with trace equivalence, which in turn coincides with contextual equivalence .

## **1 Introduction**

Dynamic allocation is central to many programming constructions. Many languages provide built-in support for dynamically-allocated resources, for example, objects in Java or references in ML. The creation of these resources is *local*, meaning that resources can be accessed only within their scope. They can also be passed around via function applications, in which case their scope is not static but evolves dynamically. When building semantics for such languages, one represents dynamic allocation as the creation of fresh locations, that can be seen as atoms or names.

In this paper, we study a paradigmatic language with dynamic allocation, namely the ν-calculus, a simply-typed call-by-value λ-calculus with fresh atom creation and equality test of atoms, as introduced by Pitts and Stark in [24]. For instance, the ν-calculus program new *n* in λ*x*.(*x* = *n*) allocates a new atom *n*, receives an atom *x* and returns the result of the comparison between *x* and *n*.

A central question while studying this language is to determine when two programs can be considered to be equivalent. The most studied approach to express behavioral equivalence between programs is contextual equivalence. Intuitively, two programs are deemed equivalent if and only if whenever they are run as part of an enclosing program called the *context*, it is not possible to distinguish one from the other. For instance, because the context has no way to guess the atom *n*, we expect the program above to be equivalent to λ*x*.false.

Reasoning on contextual equivalence for the ν-calculus has shown to be challenging, due to the interplay between the higher-order control flow and the scope

O. Kupferman and P. Sobocinski (Eds.): FoSSaCS 2023, LNCS 13992, pp. https://doi.org/10.1007/978-3-031-30829-1 2 24–45, 2023.

extrusion of atoms. A variety of frameworks has been introduced to do so, based on logical relations [24], environmental bisimulations [5], and game semantics [1].

However, the question of whether this equivalence is *decidable* remains open since the introduction of this language 30 years ago.

In this paper, we address this question by working in an asymmetric setting, giving contexts more discriminating power than just the mere creation of atoms. Indeed, contextual equivalence depends on two languages: the language for programs, and the language for contexts interacting with these programs. We take contexts in the λμref-calculus, an extension of the ν-calculus with both higherorder references and continuations. In this setting, atoms are simply references where only the unit value can be stored. Contextual equivalence is then coarser than for the symmetric setting when the contexts are also taken in the ν-calculus. For example, one of the standard examples of equivalence of the literature

$$\text{Then } n \text{ in new } n' \text{ in } \lambda f. (f \ n = f \ n') \approx\_{\text{ctx}} \lambda f. \text{true}$$

is not an equivalence anymore, since a λμref context can provide a function that stores its argument in a reference and use it to discriminate these programs.

The main result we establish in this paper is the decidability of contextual equivalence for terms of ν-calculus with contexts in the λμref-calculus. More generally, we establish this result for terms of the λμν-calculus, which corresponds to terms of the λμref-calculus that only use references storing the unit value.

To establish this result, we provide a B¨ohm-like tree representation [6,3] for the terms of the λμν-calculus. Being in call-by-value, equality of such trees coincides with Lassen's eager normal form bisimulations [16]. Moreover, since programs in the λμν-calculus are terminating, these trees, which we call *Lassen trees*, are finite. It is thus straightforward to check their equality. Then, we prove that Lassen trees equality is fully-abstract, that is it coincides with contextual equivalence with contexts in the λμref-calculus.

Proving this full-abstraction result is done through the introduction of an *operational game semantics* (OGS) for λμref by defining a Labelled Transition System (LTS) that distinguishes between internal operations, Proponent moves (originating in the program) and Opponent moves (originating in the context). Trace equivalence based on these labelled transitions is shown to coincide with the contextual equivalence of λμref.

The OGS also gives rise to a notion of *bipartite bisimulation*, describing a game between Proponent (the program in λμref) and Opponent (a context in λμref). Proponent reduces the program until it reaches a normal form, that triggers an interaction with the context. Along the game, knowledge is accumulated in configurations. When it is Opponent's turn to play, it chooses between answering a previous function call from Proponent, or generating a new function call, to which Proponent shall answer. Among this knowledge, we accumulate the atoms that have been disclosed by the two players, so that Opponent cannot use an atom private to Proponent.

The OGS LTS generates infinite trees since Opponent can interrogate an arbitrary number of times each value provided by Proponent. The Lassen trees used to decide contextual equivalence are generated using a *linearized* variant of the OGS LTS, called the *Prime Operational Game Semantics* (POGS) LTS. The POGS LTS enforces that Opponent interrogates only once each value provided by Proponent. For this linearization to be sound, one has to guess the disclosed status of atoms as soon as they are created. This can be illustrated by considering the following example of inequivalence

#### new *n* in λ*x*.*n* ctx λ*x*.new *n* in *n*.

Opponent must be able to interrogate at least twice each of these two programs to discriminate them. The first program would then return the same atom at each call, while the second program would return two different atoms. The Lassen tree of the first program would declare *n* to be disclosed when giving back the control to Opponent by providing the λ-abstraction, but this could not be matched by the second program, since *n* would not exist yet at that point of the interaction.

The main technical challenge at this point is to prove that this forecasting of the disclosure process is sound and complete. This is done by proving that the bipartite bisimilarities defined over the OGS LTS and the POGS LTS coincide. One direction is proven by lifting POGS bisimulations into OGS bisimulations via an *up-to* technique. The other direction is done by introducing a new *limit* construction of the disclosed set of atoms appearing in the OGS bisimulations, to transform it into a POGS bisimulation.

*Paper outline.* After introducing the λμref-calculus and the λμν-calculus in Section 2, we define the LTS for the OGS in Section 3. The induced trace equivalence coincides with contextual equivalence. We then move to Lassen trees in Section 4, and show that they yield an equivalence that coincides with bipartite bisimilarity in the OGS in Section 5. We discuss related work in Section 6, and present concluding remarks in Section 7. For lack of space, several technical developments are given in [9].

# **2 The** λμref**-calculus and the** λμν**-calculus**

The syntax of the λμref-calculus is given by the following grammar:

Values V, W *x* | () | λ*x*.M | true | false | Terms M, N - V | let *x* = M in N | VW | if V then N1 else N2 | V = W | new *x* = V in M | V := W |!V | μc.M | [c]M Contexts C, C- - •|[c]C | let *x* = C in M | let *x* = M in C | λ*x*.C | μc.C | if V then C else M | if V then M else C | new *x* = V in C Evaluation Contexts E, E- - [c]• | E[let *x* = • in M] Types σ, τ -Unit | Bool | σ → τ | **ref** σ | ⊥

with *x* ∈ Vars (variables), c ∈ Covars (continution variables), ∈ Locs (locations). We write supp(M) for the set of locations appearing in M, and **FV**(M) for

**Fig. 1.** λμref: typing rules for terms and evaluation contexts

the *free variables* of M. This language has two binders, the standard λ-abstraction, and the μ binder for *continuation variables* c, *d* [22].

A store, ranged over by S, T, is a finite mapping from locations to values. S() stands for the value associated to in S. We use notation S · [ → V] for the extension of S with a mapping for , which is only defined if is not defined in S. S[ → V] denotes the store S in which the value associated to is updated.

The operational semantics →op of the λμref-calculus is defined over *configurations*, which are pairs (M, S) formed by a term and a store. It is given by the following rules:

The typing system for terms is given by the rules in Figure 1. We chose here a typing judgement with a single typing context Γ, so that continuation variables are given types of the shape ¬σ. Such negated types are also used to type evaluation contexts, as specified by the two last rules in Figure 1. While we cannot store a continuation variable c in a reference, we can always store its associated function λ*x*.[c]*x*. Typing rules force terms of type ⊥ to be of the shape [*d*]M, following Parigot's original presentation of the λμ-calculus [22].

We also consider a typing judgement of the shape Σ C : (Γ; σ) - (Δ; τ), for contexts C that take terms M of type Σ; Γ M : σ and produce terms of type Σ; Δ C[M] : τ. The typing rules defining this judgement are standard and not recalled here.

In the following, we consider the λμν-calculus, the fragment of the λμrefcalculus that only handles references of type **ref** Unit. That is, for any reference type **ref** σ appearing in the typing derivation, we have σ = Unit.

We use a, b,... to range over locations of type **ref** Unit, also called atoms, and introduce the slightly shorter notation new *n* in M to stand for new *n* = () in M in λμν. The syntax for values and terms of the λμν-calculus is thus:

Values V, W *x* | () | λ*x*.N | true | false | a Terms M, N V | let *x* = M in N | VW | if V then N1 else N2 | V = W | new *n* in M | μc.M

In this setting, we see stores S directly as sets of atoms, all mapping to the unit value (). For L a set of atoms. we write -L for the store that maps atoms in L to the unit value ().

We consider the following extension of the typing judgement respectively to stores S and value-mapping substitutions γ:

> ∀ ∈ dom(S), Σ; S() : Σ() dom(S) = dom(Σ) S : Σ ∀*x* ∈ dom(Γ), Σ; Δ γ(*x*) : Γ(*x*) dom(γ) = dom(Γ) Σ; Δ γ : Γ

**Definition 1.** *A* normal form (M, S) *is a configuration that is irreducible for the reduction relation* →op*. We write* (M, S) ⇓ N *when there exists a store* T *such that* (M; S) →∗ op (N; T) *and that* (N; T) *is a normal form.*

We call the types Bool, Unit and **ref** σ *positive* types, while σ → τ and ¬σ are called *negative* types. By only allowing free variables of negative types, we can provide a sharp characterization of normal forms.

**Theorem 2.** *Taking a term* M *such that* Σ; Γ M : ⊥ *with* Γ *a typing context mapping variables to negative types, if* (M, S) *is in normal form with respect to* →op*, then* M *is either a named value* [c]V *or a neutral term* E[*x*V]*.*

*Moreover, for any configuration* (M, S) *such that* M *is in* λμν*,* Σ; Γ M : ⊥ *and* S : Σ*, there exists* N *such that* (M, S) ⇓ N*.*

**Definition 3.** *Taking two terms* M, N *such that* Σ; Γ M : σ *and* Σ; Γ N : σ*, we say that they are* contextually equivalent*, written* Σ; Γ M ctx N : σ*, when for all* *continuation variable* c *and context* C *such that* Σ - C : (Γ; σ) - (c : ¬Unit; ⊥)*, and for all store* S *such that* - S : Σ *, we have* (C[M], S)⇓ [c]() *if and only if* (C[N], S)⇓ [c]()*.*

In the definition above, we use λμref contexts to observe λμν terms. Such contexts can use higher-order references, and lead to divergent computations. For this reason, testing for convergence to () is enough when defining ctx.

## **3 Operational Game Semantics**

We now introduce a fully-abstract trace semantics for λμref programs. We follow a modular presentation, inspired by the one provided by Laird in [15], where the semantics is built from a synchronization product of three LTS:

#### **3.1 Abstract values**

To represent the interaction between the program and its environment, we distinguish between values that we can observe and values that we can interact with. The two players only exchange observable values, called *abstract values* in this paper. They are defined by the following grammar:

$$\mathsf{A}, \mathsf{B} \triangleq \mathsf{f} \mid \mathsf{a} \mid \mathsf{true} \mid \mathsf{false} \mid \mathsf{false} \mid ()$$

with f a *function name*, that is a variable used to represent functions exchanged between the two players. These correspond to the positive part of values, and are also called *ultimate patterns* in [17]. Like for terms, supp(A) stands for the set of atoms occurring in A. We consider the typing judgement Δ A : σ for abstract values, with σ a positive type, that is defined similarly as done for terms.

Then we introduce the abstraction relation that transforms a value V into a pair (A, γ) formed by an abstract value and a substitution, such that A{γ} = V:

f, g function names f -(g, [g → f]) () -((), ε) b ∈ {true, false} b -(b, ε) a an atom a -(a, ε) λ*x*.M -(f, [f → λ*x*.M])

### **3.2 Labelled Transition Systems**

The two players, Opponent and Proponent, exchange moves, which are in one of six forms:

We use **m** to range over moves, and **p** (resp. **o**) to range over Proponent (resp. Opponent) moves. Initial questions are the introductory moves. In contrast with other moves, they can introduce multiple abstract values in a row, which is useful to instantiate all the variables of a typing context Γ. They use a distinguished function name ?.

Traces **t** are sequences of moves. We write **m** for the corresponding move with reversed polarity (input switched to output, and vice-versa). We extend this definition to switch traces, written **t**.

The three labelled transition systems we define are instances of the following definition:

**Definition 4.** A labelled transition system (LTS) L is a triple of the form (Confs, Actions, −→). Confs is a set of configurations C, D. Actions is a set of actions **a**, formed by the moves **m**, together with a silent action op, corresponding to internal computations. Relation →⊆ − Confs×Actions×Confs is the labelled transition relation. We write C **a** −→ D for (C, **a**, D) ∈−→.

Taking C a configuration of an LTS L, we write **Tr**L(C) for the set of traces, as sequences of moves generated by this LTS over C (so with op actions removed). We write C tr D for the trace equivalence relation, which equates configurations C, D when both have the same set of traces.

#### **3.3 Interactive LTS**

We consider interactive configurations I;J ∈ IConfs which are either passive of the shape S; γ, or active of the shape M; S; γ with M a term, S a store, and γ a substitution. The Interactive LTS LI is then defined as the triple (IConfs, Actions, −→I) with relation −→I defined in Figure 2.

The two rules for Proponent moves describe transitions performed by normal forms and make use of the abstraction relation. In the two rules for Opponent, the notation S [supp -(A)] stands for S extended with a binding a → () in the case when A = a and a is fresh for Proponent, and simply S otherwise: Proponent extends its store when a new atom is received.

#### **3.4 Typing LTS**

We consider type-context configurations S, T ∈ ConfsTy which are either active of the shape ΔO | ⊥; ΔP or passive of the shape ΔO | ΔP, with ΔO, ΔP two disjoint typing contexts that map variables to negative types.

$$\mathsf{op}\,\,\frac{\left(\mathsf{N};\mathsf{S}\right)\longmapsto\_{\mathsf{op}}\left(\mathsf{N};\mathsf{T}\right)}{\left(\mathsf{N};\mathsf{S};\mathsf{y}\right)\stackrel{\mathsf{op}}{\longrightarrow}\_{\mathsf{I}}\left(\mathsf{N};\mathsf{T};\mathsf{y}\right)}$$

$$\text{PO}\xrightarrow[\underbrace{\langle\mathsf{E}[\mathsf{f}\mathsf{V}];\mathsf{S};\gamma\rangle\\_{\x}\stackrel{\mathsf{F}(\mathsf{A};\mathsf{c})}{\longrightarrow}\!\rangle\langle\mathsf{S};\gamma\cdot\gamma'\cdot[\mathsf{c}\mapsto\mathsf{E}]\rangle}\_{\text{I}}\qquad\qquad\qquad\qquad\dfrac{\mathsf{V}\not\supset\!\langle\mathsf{A};\gamma'\rangle}{\langle[\mathsf{c}]\mathsf{V};\mathsf{S};\gamma\rangle\\_{\x}\stackrel{\mathsf{E}(\mathsf{A})}{\longrightarrow}\!\rangle\langle\mathsf{S};\gamma\cdot\gamma'\rangle}\;\mathsf{PA}$$

**Fig. 2.** Definition of LI, the Interactive LTS: transitions of interactive configurations

PQ ΔO(f) = σ → τ Δ - A : σ ΔO | ⊥; ΔP f(A,c) −−−−→Ty ΔO | ΔP, Δ, c : ¬τ ΔO(c) = ¬σ Δ - A : σ ΔO | ⊥; ΔP c(A) −−−→Ty ΔO | ΔP, Δ PA OQ ΔP(f) = σ → τ Δ - A : σ ΔO | ΔP f (A,c) −−−−−→Ty ΔO, Δ, c : ¬τ | ⊥; ΔP ΔP(c) = ¬σ Δ - A : σ ΔO | ΔP c(A) −−−→Ty ΔO, Δ | ⊥; ΔP OA

**Fig. 3.** Definition of LTy, the typing LTS: transitions of type-context configurations

The Interactive LTS LI is then defined as the triple (ConfsTy, Actions, −→Ty) with relation −→Ty defined in Figure 3. Notice that the type of the active term is ⊥ since the reduction relation -→op is well-defined only on terms of this type.

Typing configurations can be used to specify interactive configurations, via the following validity judgement.

**Definition 5.** *An interactive configuration* I *is said to be validated by a typing configuration* S*, written* I S*, when:*

## **3.5 Disclosing LTS**

In order to enforce a *non-omniscient* condition on Opponent transitions, we introduce a Disclosing LTS LDi (DConfs, Actions, −→Di) whose configurations DConfs are pairs of sets of locations L; D with D a set of atoms contained in L. The transition relation −→Di is defined in Figure 4. The condition L∩supp(**o**) ⊆ D corresponds to the fact that Opponent cannot play Proponent atoms that have not been disclosed yet, i.e. not in D.

32 D. Hirschkoff et al.

$$\stackrel{\mathsf{op}}{\mathsf{op}} \xrightarrow[\mathsf{T}]{\mathsf{op}} \stackrel{\mathsf{op}}{\longrightarrow}\_{\mathsf{Di}} \langle \mathsf{L} \cup \mathsf{L}'; \mathsf{D} \rangle$$

PQ/PA -L; D **p** −→Di -L; D ∪ supp(**p**) L ∩ supp(**o**) ⊆ D -L; D **o** −→Di -L ∪ supp(**o**); D ∪ supp(**o**) OQ/OA

**Fig. 4.** Definition of LDi, the Disclosing LTS

**Definition 6.** *An interactive configuration* I *is said to be validated by a disclosing configuration* D = -L; D*, written* I - D*, if when writing* S *for the store component of* I*, we have* dom(S) = L*.*

#### **3.6 Operational Game Semantics: LTS and Trace Equivalence**

The *Operational Game Semantics* (OGS) LTS LOGS - (Confsogs, Actions, **a** −→ogs) is defined over configurations G, H ∈ Confsogs of the shape (I, S, D), with I - S and I - D, or over initial configurations -Σ; Γ M : σ for Proponent and c : ¬Unit (S; δ) : (Σ; Γ) for Opponent. Its transition relation is defined by the following rules:

I **a** −→I J S **a** −→Ty T D **a** −→Di E J - T J - E (I, S, D) **a** −→ogs (J, T, E) Γ = −−−−−−→ (*x*i : σi) −−−−−−−−−−→ Δi Ai : σi L = (∪isupp(Ai)) ∪ dom(Σ) -Σ; Γ M : ⊥ ?( −→Ai) −−−→ogs - -M −−−−−−−−→ {*x*i := Ai };L; ε, - −→Δi |⊥;, -L; L Γ = −−−−−−→ (*x*i : σi) −−−−−−−−−−−−−→ δ(*x*i) -(Ai; γi) −−−−−−−−−→ Δi A : σi L = Σ−1(**ref** Unit) c : ¬Unit (S; δ) : (Σ; Γ) ?( −→Ai) −−−→ogs - -S; −→γi, c : ¬Unit| −→Δi, -L; L

The initial question generated by -Σ; Γ M : σ provides a way for Opponent to instantiate variables of Γ with abstract values. In this setting Σ only contains atoms since M is a term of λμν. The transition for c : ¬Unit (S; δ) : (Σ; Γ) represents this behavior from the point of view of Opponent. Since contexts belong to λμref, these initial configurations come equipped with an initial store S of type Σ, but only the locations of type **ref** Unit are considered to be disclosed, since the other ones cannot be used by Proponent. The continuation name c is used for Opponent to provide its final answer, which is of type Unit, following the notion of observation used to define contextual equivalence.

We use notation **p** ⇒= ogs to denote a **p** transition preceded by a possibly empty sequence of op transitions. Trace equivalence according to LOGS and contextual equivalence coincide.

$$\begin{array}{l} \text{Decding Conxentual Equivalence of } \mathsf{v}\text{-Calculus with Effectful Conxats} \\\\ \text{op} \xrightarrow{\begin{subarray}{l} \mathsf{(\mathsf{N};\widehat{\mathsf{L}}) \rightarrow \mathsf{op} \ \langle\mathsf{N};\widehat{\mathsf{L}}^{\mathsf{T}}\rangle \end{subarray}} \mathsf{P}\mathsf{Q} \xrightarrow{\begin{subarray}{l} \mathsf{V}\ \mathsf{J}^{\mathsf{P}}(\mathsf{A};\mathsf{y}) \end{subarray}} \frac{\mathsf{V}\ \mathsf{J}^{\mathsf{P}}(\mathsf{A};\mathsf{y})}{\langle\mathsf{E}[\mathsf{f}\mathsf{V}];\mathsf{L}\rangle \xrightarrow{\overline{\mathsf{f}}(\mathsf{A};\mathsf{c})} \mathsf{P}\mathsf{N}} \xrightarrow{\begin{subarray}{l} \mathsf{V}\ \mathsf{J}^{\mathsf{P}}(\mathsf{A};\mathsf{y}) \end{subarray}} \frac{\mathsf{V}\ \mathsf{J}^{\mathsf{P}}(\mathsf{A};\mathsf{y})}{\langle\mathsf{C}[\mathsf{f};\mathsf{L}\rangle \xrightarrow{\overline{\mathsf{E}}(\mathsf{A})} \mathsf{P}\mathsf{N}} \mathsf{P}\mathsf{N} \end{array} \\\\ \begin{array}{l} \mathsf{V}\ \mathsf{J}^{\mathsf{P}}(\mathsf{A};\mathsf{y}) \\\ \langle\mathsf{C}[\mathsf{v}]\mathsf{V};\mathsf{L}\rangle \xrightarrow{\mathsf{E}(\mathsf{A})} \mathsf{P}\mathsf{N} \end{array} \\ \begin{array}{l} \mathsf{V}\ \mathsf{J}^{\mathsf{P}}(\mathsf{A};\mathsf{y}) \\\ \langle\mathsf{C}[\mathsf{v}]\mathsf{V};\mathsf{L}\rangle \xrightarrow{\mathsf{E}(\mathsf{A})} \mathsf{P}\mathsf{N} \end{array} \\\\ \begin{array}{l} \mathsf{V}\ \mathsf{J}^{\mathsf{P}}(\mathsf{A};\mathsf{y}) \\\ \langle\mathsf{C}[\mathsf{v}]\mathsf{V},\mathsf{L}\rangle \$$

**Fig. 5.** Definition of LPI: transitions of prime interactive configurations

## **Theorem 7.** *Consider two terms* M, N *such that* Σ; Γ M, N : σ*. We have* Σ; Γ M : σ tr Σ; Γ N : σ *if and only if* Σ; Γ M ctx N : σ*.*

Such a full-abstraction theorem was proven in [13] for *RefML*, that is the intuitionistic fragment of λμref-calculus, without control operators. It was also proven in [10] for *HOSC*, a variant of the λμref-calculus, with the call/cc operator, but without atom disclosure. Such a full-abstraction result being rather standard, we have chosen to present its proof in [9].

In the remainder of the paper, we focus on the λμν-calculus. In particular, we only consider OGS configurations corresponding to λμν from now on.

## **4 Lassen Trees for the** λμν**-calculus**

#### **4.1** POGS **and** POGS **bipartite bisimulation**

We introduce Lassen trees for terms of the λμν-calculus, as a form of *linearized* version of LOGS, where Opponent can interrogate a name provided by Proponent only once, immediately after it has been introduced. So we consider *prime interactive configurations* which are either passive of the shape L; γ, or active of the shape M; L with M a term, L a set of atoms, and γ a substitution. Compared to interactive configurations, the active configurations do not carry an environment γ. Furthermore, we have a set of atoms rather than a full store, since this LTS is defined only for the λμν-calculus and not for the whole λμref-calculus.

The Prime Interactive LTS, LPI, is then defined as (ConfsPI, Actions, −→PI), with −→PI defined in Figure 5.

The corresponding Typing LTS is defined using the transitions given in Figure 6, which are very close in spirit to the transitions in Figure 3.

The transitions for the Disclosing LTS for POGS are presented on Figure 7. We compare these with the Disclosing LTS for OGS (Figure 4) below.

The Prime Operational Game Semantics LTS is introduced as a synchronization product, together with initial transitions, like for OGS. More precisely, the synchronization between the interactive and typing LTSs requires that active configurations M; L correspond to type-contexts of the shape ΔO | ⊥, with Σ; ΔO M : ⊥ and -L : Σ, for some store typing context Σ. Accordingly, for passive configurations L; γ, we synchronize with ΔO | ΔP, and check that Σ; ΔO γ : ΔP and -L : Σ, for some store typing context Σ.

$$\begin{array}{c} \mathsf{PQ} \xrightarrow{\scriptstyle \mathsf{A}\_{\mathsf{O}}(\mathsf{f}) = \sigma \rightarrow \tau \qquad \Delta \mathsf{I} \vdash \mathsf{A} : \sigma \\\\ \langle \mathsf{A}\_{\mathsf{O}} \mid \bot \rangle \xrightarrow{\widetilde{\mathsf{f}}(\mathsf{A}, \mathsf{c})} \mathsf{P} \mathrm{T}\_{\mathsf{Y}} \ \langle \mathsf{A}\_{\mathsf{O}} \mid \Delta, \mathsf{c} : \neg \tau \rangle \end{array} \qquad \begin{array}{c} \mathsf{A}\_{\mathsf{O}}(\mathsf{c}) = \neg \sigma \qquad \Delta \models \mathsf{A} : \sigma \\\\ \langle \mathsf{A}\_{\mathsf{O}} \mid \bot \rangle \xrightarrow{\widetilde{\mathsf{E}}(\mathsf{A})} \mathsf{P} \mathrm{T}\_{\mathsf{Y}} \ \langle \mathsf{A}\_{\mathsf{O}} \mid \Delta \rangle \end{array} \mathsf{P} \mathsf{A} $$

**Fig. 6.** Definition of LPTy: transitions of prime type-context configurations

$$\mathsf{op}\ \frac{\mathsf{D}' \subseteq \mathsf{L}'}{\langle \mathsf{L}, \mathsf{D} \rangle \xrightarrow{\mathsf{op}} \mathsf{p} \mathsf{d} \quad \langle \mathsf{L} \ \mathsf{u} \ \mathsf{L}'; \mathsf{D} \ \mathsf{u} \ \mathsf{D}' \rangle}$$

$$\mathsf{PQ}/\mathsf{P}\mathsf{A} \ \frac{\mathsf{supp}(\mathsf{p}) \subseteq \mathsf{D}}{\langle \mathsf{L}, \mathsf{D} \rangle \xrightarrow{\mathsf{p}} \mathsf{p}\_{\mathsf{p}d} \ \langle \mathsf{L}, \mathsf{D} \rangle} \qquad \qquad \frac{\mathsf{L} \cap \mathsf{supp}(\mathsf{o}) \subseteq \mathsf{D}}{\langle \mathsf{L}, \mathsf{D} \rangle \xrightarrow{\mathsf{o}} \mathsf{p}\_{\mathsf{p}d} \ \langle \mathsf{L} \cup \mathsf{supp}(\mathsf{o}); \mathsf{D} \cup \mathsf{supp}(\mathsf{o}) \rangle} \quad \mathsf{OQ}/\mathsf{O}\mathsf{A}$$

To synchronize with the Disclosing LTS, whose states are of the form L; D, we simply impose that the L component is the same in the state of LPI, both for active and passive configurations.

We call LPOGS the LTS obtained by synchronizing LPI, LPTy and LPDi. We write P, Q ∈ ConfsPOGS the configurations of LPOGS. The *Lassen tree* of a term is then defined as the unfolding of the LPOGS on the initial active configuration associated with this term.

*Example 8.* The Lassen trees (omitting the typing configurations) for [c]new *n* in λ .*n* and [c]λ .new *n* in *n* are given by:

[c]new *n* in λ .*n*; ∅, ∅; ∅ {a}; [f → λ .a], {a}, ∅ {a}; [f → λ .a], {a}, {a} [c ](λ .a)(), {a}, {a}, ∅ [c ](λ .a)(), {a}, {a}, {a} {a}; ε, {a}, {a} c(f) c(f) f((), c ) f((), c ) c (a) [c]λ .new *n* in *n*; ∅, ∅; ∅ ∅; [f → λ .new *n* in *n*], ∅, ∅ [c ](λ .new *n* in *n*)(), ∅, ∅, ∅ {a}; ε, {a}, {a} c(f) f((), c ) c (a)

Due to the condition supp(**p**) ⊆ D in **p** −→pd, some configurations with terms in normal form do not have a corresponding Proponent transition. The dashed arrows correspond to op transitions that lead to such stuck configurations.

#### **4.2 Bipartite Bisimulations for** OGS **and** POGS

We consider typed relations on passive and active configurations, that is, we require related configurations to have the same type. This means in particular that the environment components γ of the two configurations have the same domain. In addition to the typing, we also enforce that both sets of disclosed atoms are identical.

**Definition 9.** *A* bipartite bisimulation *is a pair of relations* (RAct, RPas) *respectively on active and passive configurations, such that:*

*An* OGS*-*bipartite bisimulation *is a bipartite bisimulation defined over* LOGS*, and a* POGS*-*bipartite bisimulation *is a bipartite bisimulation defined over* LPOGS*. We write* ogs *and* pogs *respectively for the greatest bipartite bisimulation respectively over* LOGS *and* LPOGS*.*

The following property follows from the fact that the transition relation is deterministic (up to the choice of fresh names).

#### **Lemma 10.** ogs *coincides with trace equivalence on* OGS *configurations.*

For op transitions, the difference between OGS and POGS shows up in the disclosing LTS: in op −−→pd, a D component can be chosen non-deterministically. This observation is related to the existential quantification in the second clause of Definition 13. Both in LOGS and LPOGS, there is only one possible next visible (Proponent) move. However, in pogs, the game involves choosing an appropriate set of atoms to be disclosed along op −−→pd transitions. For instance, when constructing a POGS bipartite bisimulation between terms new *n* in λ .*n* and λ .new *n* in *n* from Example 8, we have two choices for the second step:

$$\begin{array}{llll} \left( (\langle \{ \mathbf{a} \}; [\mathbf{f} \mapsto \lambda \Box \mathbf{a}] \rangle, (\{ \mathbf{a} \}, \varnothing) \rangle \right), & (\langle \varnothing \rangle; [\mathbf{f} \mapsto \lambda \Box \mathbf{a} \text{ new } n \text{ in } n] \rangle, (\varnothing, \varnothing)) \\\ ( (\langle \{ \mathbf{a} \}; [\mathbf{f} \mapsto \lambda \Box \mathbf{a}] \rangle, (\{ \mathbf{a} \}, \{ \mathbf{a} \}) ), & (\langle \varnothing \rangle; [\mathbf{f} \mapsto \lambda \Box \mathbf{a} \text{ in } n] \rangle, (\varnothing, \varnothing))) \end{array}$$

The latter does not satisfy the constraint on the disclosed set, since the sets are not the same in the two configurations. The former leads to a stuck configuration: ([c ](λ .a)(), {a} , {a}, ∅ ) cannot perform any Proponent move. Thus the two programs are not equivalent.

#### **4.3 Deciding** pogs

We now study how to decide when two POGS configurations are bisimilar. First, trees generated by LPOGS are of finite depth.

## **Lemma 11.** Taking a POGS configuration G, any trace in **Tr**POGS(G) is finite.

This lemma is proven using a biorthogonal logical predicate, following the use of biorthogonality to prove strong normalization of λμ-calculus [23], the computational metalanguage [18], and cut elimination for linear logic [8]. The proof can be found in [9].

Due to the non-determinism of atom generation in -→op, of function name generation in -, and of name picking in Opponent transitions, the trees generated by LPOGS are infinitely branching. To tame this infinite branching, we see the set of moves Moves and the set of configurations ConfsPOGS of LPOGS as nominal sets [7] over atoms, function and continuation variables. So taking π a finite permutation over these sets, we write π ∗ *X* for the action of permutation π over elements of nominal set *X*. The transition relation −→pogs of LPOGS preserves this action of permutation, i.e., it is equivariant: if P **m** −→pogs Q then for all finite permutation π, we have π ∗ P π∗**m** −−−→pogs π ∗ Q.

One can then consider a variant LDPOGS of the POGS LTS which uses the same set of configurations as LPOGS, but whose transition relation −→dpogs chooses fresh atoms and names deterministically. So −→dpogs is then deterministic on op and Proponent actions, and finitely branching on Opponent actions.

We remark at this point that the notion of bipartite bisimulation pogs introduced in Definition 13 is not suited for LDPOGS. Indeed, it requires equality of actions in the bisimulation game, and also that configurations related by bisimulation have the same type. So we relax the definition of pogs and work with ternary relations, adding a finite permutation of names and atoms in order to match the actions, rather than enforcing syntactic equality.

**Definition 12.** A relation R ⊆ ConfsPOGS × ConfsPOGS × Perm is said to be valid when, for all ((I, S, , D), (J, T, , D ), π)∈R, we have T = π ∗ S and D = π ∗ D.

**Definition 13.** A relaxed bipartite bisimulation is a pair of valid relations (RAct, RPas) respectively on active and passive configurations such that:

We write r pogs for the greatest relaxed bipartite bisimulation over LPOGS. From the fact that −→pogs is equivariant, we deduce that r pogs and ogs coincide. Since LDPOGS generates finite Lassen trees, we deduce that the bisimulation game can be decided.

**Theorem 14.** Taking two POGS configurations P, Q, we can decide if P pogs Q.

#### **4.4 Relating the Transitions in** OGS **and** POGS

To relate the transitions in the OGS and in the POGS, we need to introduce some relations and operations on OGS configurations.

**Definition 15.** *Let* G = (I, S, -L; D) *and* H = (I, S, -L; D ) *be two* OGS *configurations. We write* G ⊆Di H *when* D ⊆ D *.*

When G ⊆Di H, the configurations only differ by their set of disclosed atoms.

**Lemma 16.** *If* G ⊆Di H *and* G **a** −→ogs G *then* H **a** −→ogs H *and* G ⊆Di H *.*

**Lemma 17.** *Let* P *be an active prime configuration. We have the following:*

$$\begin{array}{l} \mathsf{I} \quad \mathit{if} \, \mathbb{P} \xrightarrow{\mathsf{op}} \mathsf{g} \, \mathbb{P}', \,\, then \,\mathbb{P} \xrightarrow{\mathsf{op}} \mathsf{p} \,\, \mathbb{P}',\\ \mathsf{I} \quad \mathit{if} \, \mathbb{P} \xrightarrow{\mathsf{op}} \mathsf{p} \, \mathbb{P}', \,\, then \,\mathbb{P} \xrightarrow{\mathsf{op}} \mathsf{g} \,\underline{\subseteq} \mathsf{Di} \,\, \mathbb{P}'. \end{array}$$

In POGS, the disclosed set increases in op transitions as seen above, but not in **p** transitions. In a sense, disclosing in OGS is done only when needed, whereas in POGS, disclosing must be declared as soon as the atom is created. This is ensured by the additional condition supp(**p**) ⊆ D in the rule for **p** −→pd.

**Lemma 18.** *When* P **p** −→pogs P *with* P *active, we also have* P **p** −→ogs P *.*

However, the converse does not always hold, specifically if an atom has been declared non-disclosed but still appears in the action **p**. Indeed, the transition (-[c]a;-L; ∅, S, -L; ∅) c(a) −−−→ogs (--L; ∅, S, -L; {a}) is valid for OGS, but has no counterpart in POGS, since -L; ∅ cannot make the transition c(a) −−−→pd.

Using the following notion of limit (on OGS configurations), we can intuitively replace D by its minimal extension, preventing this phenomenon from happening.

**Definition 19.** *Given a configuration* G = (I, S, -L; D)*, we define its* limit *as:*

$$\operatorname{lim}(\mathbb{G}) \triangleq (\mathbb{I}, \mathbb{G}, \langle \mathsf{L}; \bigcup\_{\mathsf{t} \in \mathsf{Trac.os}} (\mathsf{L} \cap \mathsf{D}') \rangle) \text{ with } \mathsf{G} \xrightarrow{\mathsf{t}} \mathsf{ogss} (\mathsf{\tau} \dashv \langle \mathsf{\tau}, \mathsf{D}' \rangle).$$

We have that G ⊆Di **lim**(G) and **lim** is idempotent.  Being a limit configuration is preserved by moves but not necessarily by op.

**Lemma 20.** *Let* P *be a limit configuration. If* P **p** −→ogs P *, then* P **p** −→pogs P *.*

For Opponent transitions, the situation is less simple since not all active OGS configurations are active POGS configurations. To circumvent that issue, we reuse the tensor product from [12]. For two OGS configurations where at least one is passive, we define the tensor product, written ⊗, as follows:

$$(\mathbb{T}, \mathbb{S}, \mathbb{D}) \otimes (\mathbb{J}, \mathbb{T}, \mathbb{E}) = (\mathbb{L} \otimes \mathbb{J}, \mathbb{S} \otimes \mathbb{T}, \mathbb{D} \otimes \mathbb{E})$$

$$\langle \mathbb{S}; \gamma \rangle \otimes \langle \mathbb{S}'; \gamma' \rangle = \langle \mathbb{S} \cup \mathbb{S}'; \gamma \cdot \gamma' \rangle \qquad \langle \mathbb{M}; \mathbb{S}; \gamma \rangle \otimes \langle \mathbb{S}'; \gamma' \rangle = \langle \mathbb{M}; \mathbb{S} \cup \mathbb{S}'; \gamma \cdot \gamma' \rangle$$

$$\langle \mathbb{L}; \mathbb{D} \rangle \otimes \langle \mathbb{L}'; \mathbb{D}' \rangle = \langle \mathbb{L} \cup \mathbb{L}'; \mathbb{D} \cup \mathbb{D}' \rangle \text{ when } \begin{array}{c} \mathbb{D}' \cap \mathbb{L} \subseteq \mathbb{D} \\ \mathbb{D} \cap \mathbb{L}' \subseteq \mathbb{D}' \end{array}$$

The side conditions for the L and D components ensure that no shared atom is disclosed on one configuration but not the other.

We can then describe an active OGS configuration as the tensor of two POGS configurations (where S = -L):

$$(\langle \mathbb{M}; \mathbb{S}; \gamma \rangle, \langle \Lambda\_O \vdash \bot; \Delta\_P \rangle, \langle \mathsf{L}, \mathsf{D} \rangle) = (\langle \mathbb{M}; \mathsf{L} \rangle, \langle \Delta\_O \vdash \bot \rangle, \langle \mathsf{L}, \mathsf{D} \rangle) \otimes (\langle \mathsf{L}; \gamma \rangle, \langle \Delta\_O \vdash \Delta\_P \rangle, \langle \mathsf{L}, \mathsf{D} \rangle)$$

Finally, we have the following property for opponent transitions:

**Lemma 21.** When P **o** −→pogs Q, we have P **o** −→ogs Q ⊗ P. When P **o** −→ogs G, we have P **o** −→pogs Q with G = Q ⊗ P.

# **5 Relating Bisimilarities in** OGS **and** POGS

In this section, we show that pogs can be used to characterize ogs for the limit configurations introduced above. We rely for that on up-to techniques for bipartite bisimulation in OGS, which we introduce first.

#### **5.1 Up-to techniques for** ogs

The proofs in this section use the theory of compatible functions [27,25]. More details can be found in [9].

**Definition 22 (Bipartite bisimulation up-to).** Given a function *f* , a bipartite bisimulation up to *f* is a pair (RAct, RPas) such that:

We then define hide(RAct, RPas) - (⊆DiRAct⊇Di, ⊆DiRPas⊇Di). Recall that we still require that hide(RAct, RPas) only contains pairs of configurations with the same disclosed set. The soundness of hide can be proved using Lemma 16.

**Lemma 23.** hide is a sound up-to technique, i.e. if (RAct, RPas) is a bisimulation up to hide, then (RAct, RPas) ⊆ogs.

Given a pair of relations (RAct, RPas) on active and passive OGS configurations respectively, we define the following functions:

$$\begin{array}{ll} \mathsf{t}\texttt{t}\texttt{t}\texttt{s}\texttt{r}(\mathscr{R}\_{Act},\mathscr{R}\_{Pas}) \triangleq \left( \{ (\mathbb{G}\_{1}\otimes\mathbb{G}\_{2},\mathbb{H}\_{1}\otimes\mathbb{H}\_{2}) \, \mathrm{s}.\mathrm{t}.\,(\mathbb{G}\_{1},\mathbb{H}\_{1}) \in \mathscr{R}\_{Act}, (\mathbb{G}\_{2},\mathbb{H}\_{2}) \in \mathscr{R}\_{Pas}\},\\ \qquad \{ (\mathbb{G}\_{1}\otimes\mathbb{G}\_{2},\mathbb{H}\_{1}\otimes\mathbb{H}\_{2}) \, \mathrm{s}.\,(\mathbb{G}\_{1},\mathbb{H}\_{1}), (\mathbb{G}\_{2},\mathbb{H}\_{2}) \in \mathscr{R}\_{Pas}\}\\ \texttt{s}\texttt{p}\texttt{1t}(\mathscr{R}\_{Act},\mathscr{R}\_{Pas}) \triangleq \left( \{ (\mathbb{G}\_{1},\mathbb{H}\_{1}) \qquad \mathrm{s}.\mathrm{t}.\,(\mathbb{G}\_{1}\otimes\mathbb{G}\_{2},\mathbb{H}\_{1}\otimes\mathbb{H}\_{2}) \in \mathscr{R}\_{Act} \},\\ \qquad \{ (\mathbb{G}\_{1},\mathbb{H}\_{1}) \qquad \mathrm{s}.\mathrm{t}.\,(\mathbb{G}\_{1}\otimes\mathbb{G}\_{2},\mathbb{H}\_{1}\otimes\mathbb{H}\_{2}) \in \mathscr{R}\_{Pas}\} \end{array} \right)$$

**Lemma 24.** split(ogs) ⊆ogs.

tensor is not a sound up-to technique. It is nevertheless useful to reason about POGS bipartite bisimilar configurations; see Theorem 30 below.

#### **5.2 Properties of the Limit (in** OGS**)**

**Lemma 25 (Monotonicity).** If G is passive and G **t** −→ogs H, then there exists G such that G ⊗ G ⊆Di H.

Lemma 25 shows that transitions can only increase the substitution and the store (corresponding to the G component), and the set of disclosed atoms (represented by the use of ⊆Di). More precisely, ⊆Di is required if some atoms from G are disclosed along the trace **t**, in which case new ones can appear in G .

Lemma 25 is language specific. It does not hold when the language allows the content of the store to be modified (like, e.g. in λμref). Additionally, LTSs enforcing some local restriction on the usage of function or continuation names usually have extra components that are modified along the transitions; we return to this point in Section 7.

In a limit configuration (Definition 19), all atoms that may be disclosed at some point are disclosed. By Lemma 25, these atoms can be disclosed using a single trace.

**Lemma 26.** Given a passive configuration G, there exists a trace **t** and a configuration H such that G **t** −→ogs **lim**(G) ⊗ H.

The limit is also useful to relate transitions in OGS and in POGS as follows.

**Lemma 27.** Take a POGS configuration P.

If P is active and P **a** −→ogs Q, then **lim**(P) **a** −→pogs **lim**(Q). If P is passive and P **o** −→ogs Q ⊗ P, then **lim**(P) **o** −→pogs **lim**(Q).

All in all, we obtain that ogs is a congruence for **lim**. For R a relation over configurations, we write **lim**(R) for the set {(**lim**(G), **lim**(H)) | (G, H) ∈ R}.

**Lemma 28.** ogs is closed by computing the limit: **lim**(ogs)⊆ ogs.

The case for passive configurations follows immediately from Lemmas 26 and 24.

40 D. Hirschkoff et al.

The property of the limit might make us think that the disclosure process of an atom could be decided statically, by annotating new syntactically. The following example shows that it is not the case:

### λ*b*.new *n*, *m* in λ .if *b* then *n* else *m*

Either *n* or *m* will be disclosed depending on the boolean *b* given by Opponent, but never both. So this term is indeed contextually equivalent to λ*b*.new *n* in λ .*n*.

#### **5.3 Correspondence Between** ogs **and** pogs

**Theorem 29 (From** ogs **to** pogs**).** *Consider two* POGS *configurations* P *and* Q*. If* P ogs Q *are both limit configurations, then* P pogs Q*.*

To reason about bisimilar POGS configurations, we use the closure of tensor, written tensor -. Intuitively, tensor -(RAct) contains the pairs (G1 ⊗ G2, H1 ⊗ H2) with (G1, H1)∈RAct, (G2, H2) ∈ tensor -(RPas), and tensor -(RPas) contains the pairs (G1 ⊗ G2, H1 ⊗ H2) with (G1, H1)∈RPas, (G2, H2) ∈ tensor -(RPas). *tion. Then* tensor -

**Theorem 30 (From** pogs **to** ogs**).** *Suppose* R *is a* POGS *bipartite bisimula-*(R)*is a* OGS *bipartite bisimulation up-to hiding.*

By Lemma 23, Theorem 30 means that if P pogs Q, then P ogs Q.

The correspondence between ogs and pogs is restricted to prime configurations as pogs can only relate those. Having the additional conditions of configurations being limits is enough for our decidability result.

## **6 Related Work**

The ν-calculus was introduced in [24], together with logical relations to reason over contextual equivalence for this language. These logical relations use a Kripke-style definition, worlds being defined as spans of atoms to keep track of the disclosed atoms, similar to the permutation we use in our relaxed bipartite bisimulations. They capture contextual equivalence for programs of *first order* type, but are an incomplete technique for higher-order programs. This entails a decidability result for the first-order fragment of the ν-calculus, since logical relations only quantify over finite objects at first-order types.

Categorical models of the ν-calculus were provided in [29,30], using a representation of name creation via a strong monad. Two examples of such models were given: (i) the functor category *Set*I with *I* the category of finite sets and injection; (ii) the category **B***G* of continuous *G*-sets, with *G* the topological group of automorphisms over N. None of these models are fully-abstract, since they distinguish new *n* in λ*x*.*x* = *n* from λ*x*.false.

These models were later refined using nominal sets [7], so that types are interpreted via *Fraenkel-Mostowski* sets [28] or domains [14]. Both of these works are continuation models; they might be used to provide a semantics for the λμνcalculus studied in this paper, a direction we wish to explore in future work. Such use of continuations was justified in [28] to provide a model for an extension of the ν-calculus with recursion. More recently, *proof-relevant* logical relations were introduced to deal with recursion in the presence of name generation [4].

In [26], a model of the ν-calculus is given in quasi-Borel spaces, showing a correspondence between random sampling and fresh name generation. This model is shown to be fully-abstract for terms of first-order types.

In [5], environmental bisimulations for the ν-calculus are defined and shown to be fully abstract. Nevertheless, it does not seem possible to extract a decision procedure from that result, since environmental bisimulations are played over a higher-order LTS, that is, an LTS whose actions contain λ-terms. So this LTS is infinitely branching at higher-order types.

Eager normal-form bisimulations have been introduced by Lassen for the callby-value λ-calculus [16] and λμ-calculus. In [31], a notion of bisimulation similar to ogs is introduced and shown to be fully abstract for an untyped version of λμref. Compared to the standard notion of eager normal form bisimulations, the configurations in the bisimulations in [31] contain an environment similar to the environment component γ of the OGS LTS in Section 3.

In [1], a fully-abstract game model is provided for the ν-calculus. However, this model requires an extensional collapse, that is not directly computable at higher-order type. So that model could only be used to prove the decidability of contextual equivalence for terms of first-order types. Enforcing a well-bracketed and visible behavior for Opponent in the OGS model, we believe that our trace model would coincide with the intentional game model of [1]. Nominal game semantics was developed for languages with nominal references and exceptions in [32]. In that setting, algorithmic presentations of game semantics make it possible to provide a classification of decidability of call-by-value languages with (bounded) integer references [19], and ground references [21]. In this setting, the undecidability of contextual equivalence originates from the use of integer references by Proponent. A detailed survey on the literature on contextual equivalence for the ν-calculus is available in [33].

## **7 Conclusion**

To decide the contextual equivalence between two λμν typed terms M and N with contexts in the λμref-calculus, we first construct the corresponding initial configurations, and we can decide by Thm. 14 if they are POGS-bisimilar. This decidability result comes from the fact that the POGS LTS generates finite trees.

Then, we prove in Thm. 29 and Thm. 30 that two initial active configurations are POGS-bisimilar iff they are OGS-bisimilar. This is possible because initial configurations are prime (they are active and γ is empty) and are also limit configurations (their disclosed sets contain all the atoms of the store). In Thm. 7 and Lemma 10, we prove that M and N are contextually equivalent iff the corresponding initial configurations are OGS-bisimilar, which yields decidability.

We now examine the obstacles that remain to prove the decidability of contextual equivalence with contexts in the ν-calculus.