Dieses Kapitel stellt einen bedeutenden Fortschritt bei der Darstellung und Argumentation von Programmiersprachen innerhalb von Korrekturassistenten dar, wobei der Schwerpunkt auf der Erweiterung von Guarded Interaction Trees (GITrees) zur Unterstützung kontextabhängiger Effekte liegt. Die Autoren stellen einen neuartigen Ansatz vor, der die Modellierung übergeordneter Programme höherer Ordnung mit kontextabhängigen Effekten wie Call / cc und begrenzten Fortsetzungen innerhalb des Coq-Korrekturassistenten ermöglicht. Diese Erweiterung ist konservativ und erhält das ursprüngliche GITrees-Rahmenwerk bei gleichzeitiger Verbesserung seiner Fähigkeiten. Das Kapitel bietet einen detaillierten Überblick über die technische Entwicklung und die wichtigsten Herausforderungen dieser Erweiterung, einschließlich der Definition von GITrees als geschützte rekursive Typen und der Verwendung von Irisfunktionen wie Trennlogik und Iris Proof Mode. Es untersucht auch die Anwendung dieser Erweiterung auf verschiedene Programmiersprachen und demonstriert ihre Modularität und Skalierbarkeit. Die Autoren stellen ein Typensystem für die Interoperabilität zwischen Sprachen mit abgegrenzten Fortsetzungen und Speichern höherer Ordnung vor, das die Typensicherheit und Rechenfähigkeit nachweist. Das Kapitel schließt mit einer Diskussion über verwandte Arbeiten und zukünftige Richtungen, die das Potenzial für weitere Forschung in diesem Bereich aufzeigt.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
Guarded Interaction Trees are a structure and a fully formalized framework for representing higher-order computations with higher-order effects in Coq. We present an extension of Guarded Interaction Trees to support formal reasoning about context-dependent effects. That is, effects whose behaviors depend on the evaluation context, e.g., call/cc, shift and reset. Using and reasoning about such effects is challenging since certain compositionality principles no longer hold in the presence of such effects. For example, the so-called “bind rule” in modern program logics (which allows one to reason modularly about a term inside a context) is no longer valid. The goal of our extension is to support representation and reasoning about context-dependent effects in the most painless way possible. To that end, our extension is conservative: the reasoning principles (and the Coq implementation) for context-independent effects remain the same. We show that our implementation of context-dependent effects is viable and powerful. We use it to give direct-style denotational semantics for higher-order programming languages with call/cc and with delimited continuations. We extend the program logic for Guarded Interaction Trees to account for context-dependent effects, and we use the program logic to prove that the denotational semantics is adequate with respect to the operational semantics. This is achieved by constructing logical relations between syntax and semantics inside the program logic. Additionally, we retain the ability to combine multiple effects in a modular way, which we demonstrate by showing type soundness for safe interoperability of a programming language with delimited continuations and a programming language with higher-order store.
1 Introduction
Despite a lot of recent progress, representing and reasoning about programming languages in proof assistants, such as Coq, is still considered a major challenge. The design space is wide and many approaches have been considered. Recently, research on a novel point in the design space was initiated with the introduction of Interaction Trees [34], or ITrees for short. ITrees were introduced to simplify representation and reasoning about possibly non-terminating programs with side effects in Coq. In a sense, ITrees provide a target for denotational semantics of programming languages, which allows one to abstract from syntactic details often found in models based on operational semantics. ITrees specifically allow one to easily represent and reason about various effects and their combinations in a modular way. A wide range of subsequent applications of ITrees (see, e.g., [18, 25, 35, 36], among others) show that they indeed work very well for representing and reasoning about first-order programs with first-order effects. As part of the trade-offs, ITrees could not support higher-order representations and higher-order effects. To address this challenge, Guarded Interaction Trees (or GITrees for short) were introduced [13].
While GITrees support higher-order effects, in particular, the challenging case of higher-order store, they are limited to effects that do not alter the control flow of the program (more specifically, the continuation). As a consequence, one cannot use GITrees to give direct-style denotational semantics of programming languages with context-dependent effects such as call/cc, exceptions, or delimited continuations. It is of course possible to give semantics to, e.g., call/cc using a CPS translation, but this would require a global transformation which complicates representation and reasoning, especially in combination with other effects present. In this paper we extend GITrees to support direct-style representation and reasoning about higher-order programs with higher-order context-dependent effects in Coq, and evaluate its modularity.
Anzeige
We want to stress that our extension to context-dependent effects is not only theoretically interesting, but also important for scalability, since many real mainstream programming languages include context-dependent effects. Indeed, exceptions are now a standard feature in many languages, and while other context-dependent effects such as delimited continuations are not as widespread in mainstream programming languages, they are present in the core calculi used for some such languages: for example, the Glasgow Haskell Compiler core language was recently extended with delimited continuations to support the introduction of effect systems, which can be efficiently developed on top of delimited continuations [16]. Moreover, effect handlers, which rely on control flow operators, have recently been introduced in OCaml 5.0, and as a design feature in Helium [7], Koka [20, 21], and other languages. Note that these languages do not only include forms of delimited continuations, but also other effects, which underscores the importance of considering delimited control in combination with other effects.
Overview of technical development and key challenges. Similarly to how ITrees are defined as a coinductive type in Coq, GITrees are defined as a guarded recursive type (this is to support function spaces in GITrees; in the presence of function spaces there are negative occurrences of the recursive type and hence one cannot simply define the type of GITrees using coinduction). Coq does not directly support guarded recursive types, so GITrees are defined using a fragment of guarded type theory implemented in Coq, as part of the Iris framework [14]. To work efficiently with GITrees we make use of other Iris features like separation logic and Iris Proof Mode [19], which we use to define custom program logics for different (combinations of) effects. This enables us to reason about GITrees smoothly in the Iris logic in Coq, in much the same way as one works directly in Coq. We recall the precise definition of GITrees in Section 2.
Broadly speaking, GITrees model effects in the following way. The type of GITrees is parameterized over a set of effectful operations. Each operation is given meaning by a reifier function, using a form of state monad. From this, we define the reduction relation of GITrees, which gives semantics to computations represented by GITrees.
To support context-dependent effects, we extend (Section 3) the notion of a reifier so that reification of effects can also depend on the context; technically, the reifier operation becomes parameterized by a suitable GITrees continuation. This extension allows us to give semantics to context-dependent effects, but it comes at a price. In particular, following the change in semantics, we need to reformulate the program logic for GITrees: in the presence of context-dependent effects (like call/cc), the so-called “bind”-rule becomes unsound. Of course, we do not want this reformulation to complicate reasoning about computations that do not include context-dependent effects. To that end, we parameterize the GITrees (and the program logic) by a flag, which allows us to recover the original proof rules and make sure that all of the original GITrees framework still works with our extension.
Anzeige
To motivate the extension to context-dependent effects, we give direct-style denotational semantics to a higher-order programming language \(\lambda _{\textsf{callcc}}\) with call/cc (Section 3). Furthermore, we use the derived program logic to construct a logical relation between the denotational and the operational semantics to prove computational adequacy of our model.
Our main interest, however, lies in the treatment of delimited continuations. In Section 4 we show how to represent delimited continuations as effects in GITrees, and we use them to define a novel denotational semantics for a programming language with shift and reset operators. We prove that our denotational semantics is sound with respect to the operational semantics (given by an extension of the CEK abstract machine). We additionally use the program logic to define a logical relation, and prove computational adequacy and semantic type soundness. We recall that semantic type soundness is interesting because it allows one to combine syntactically well-formed programs with syntactically ill-typed, but semantically well-behaved programs [30].
As we mentioned, it is important to consider delimited continuations not only on their own, but in combinations with other effects. And indeed, one of the key points of ITrees, and therefore also of GITrees, is that they support reasoning about effecting and language interoperability by establishing a common unifying semantic framework. In this paper, we consider (in Section 5) an example of such interaction: we show a type-safe embedding of \(\lambda _{\textsf{delim}}\) with delimited continuations into a language \(\lambda _{\textsf{embed}}\) with higher-order store. We allow \(\lambda _{\textsf{delim}}\) expressions to be embedded into \(\lambda _{\textsf{embed}}\) by surrounding them by simple glue code, and use a type system to ensure type safety of the combined language. To define the semantics of the combined language we rely on the modularity of GITrees, and combine reifers for delimited continuations with reifiers for higher-order store. We prove type safety of the combined language by constructing a logical relation and use the program logic both to define the logical relation and to verify the glue code between the two languages. The type system for the combined language naturally requires that the embedded code is well-typed according to the type system for \(\lambda _{\textsf{delim}}\) and thus we can rely on the type soundness of \(\lambda _{\textsf{delim}}\) (proved in the earlier Section 4) when proving type safety for the combined language. At the end of Section 5, we give an example of how to verify a more involved interaction of effects, albeit without the type system.
Summary of Contributions. In summary, we present:
A conservative (with respect to the old results) extension to GITrees for representing and reasoning about context-dependent effects (Section 3).
A sound and adequate model of a calculus with call/cc and throw, implemented in a direct style (Section 3.3).
A sound and adequate model of a calculus with delimited continuations, with operations shift and reset, implemented in a direct style (Section 4).
A type system for interoperability between a programming language with delimited continuations and a programming language with higher-order store, with a semantic type safety proof Section 5.
All results in the paper have been formalized in Coq as a modification to the GITrees library and the previously proved results have been ported to our extension. We conclude and discuss related work in Section 6. Before we go on with the main part of the paper, we recall some background material on GITrees.
2 Guarded Interaction Trees
In this section we provide an introduction to guarded interaction trees. Our treatment is brief, and we refer the reader to the original paper for details [13].
Iris and Guarded Type Theory. Guarded Interaction trees (GITrees ) are defined in Iris logic. Here we briefly touch Iris, and refer the reader to the literature on Iris [15] and guarded type theory [8] for more in-depth details. Iris is a separation logic framework built on top of a model of guarded type theory, the main use of which is to solve recursive equations and define guarded recursive types, such as the type of GITrees described below. Moreover, Iris has a specialized proof mode [19], implemented in Coq. This allows the users of Iris to carry out formal reasoning in separation logic as if they are proving things normally Coq, as we have done in the formalization of this work. For this reason, in the paper we will work with Iris and its type theory informally. Still, we need to say a few things about the foundations.
The syntax of Iris, shown in Figure 1, contains types, terms, and propositions. The grammar is standard for higher-order logic, with the exception of the guarded types fragment, and separation logic connectives. The type of propositions is denoted \(\textsf {iProp}\). The guarded part of guarded type theory is the “later” modality \(\mathord {\blacktriangleright }\). Intuitively, we view all types as indexed by a natural number, where \(\tau _{n}\) contains elements of \(\tau \) “at time” n. Then \(\mathord {\blacktriangleright }\tau \) contains elements of \(\tau \) at a later time; that is, \((\mathord {\blacktriangleright }\tau )_{n}=\tau _{n-1}\). There is an embedding \(\textsf {next}: \tau \rightarrow \mathord {\blacktriangleright }\tau \), and there is a guarded fixed point combinator \(\textit{fix}_{\tau }: (\mathord {\blacktriangleright }\tau \rightarrow \tau ) \rightarrow \tau \), similar to the unguarded version in PCF. We can also lift functions to \(\mathord {\blacktriangleright }\): given \(f : A \rightarrow B\), we have \(\mathord {\blacktriangleright }f : \mathord {\blacktriangleright }A \rightarrow \mathord {\blacktriangleright }B\).
For the proposition, Iris contains the usual separation logic connectives, and the two modalities: “later” \(\mathop {\triangleright }\) and “persistently” \(\Box \). The propositional \(\mathop {\triangleright }\) modality reflects the type-level later modality \(\mathord {\blacktriangleright }\) on the level of propositions, as justified by the following rule: \(\mathop {\triangleright }(\alpha =_\tau \beta ) \dashv \vdash \textsf {next}(\alpha ) =_{\mathord {\blacktriangleright }\tau } \textsf {next}(\beta )\). The persistence modality \(\Box P\) states that the proposition P is available without claiming any resources (as it normally is the case in separation logic); crucially it makes the proposition duplicable: \(\Box P \vdash (\Box P)*(\Box P)\). An example of a persistent proposition is the invariant proposition
, which satisfies
.
Fig. 1.
Grammar for the Iris base logic.
Fig. 2.
Guarded datatype of interaction trees.
Guarded recursive datatypes are datatypes obtained from recursive equations of the form \(X = F(\mathord {\blacktriangleright }X)\). In other words, guarded recursive datatypes are similar to the regular datatypes you see in normal programming languages, but every recursive occurrence of the type must be guarded by the \(\mathord {\blacktriangleright }\) modality. The datatype we are concerned with here is the type of GITrees, shown in Figure 2. It is parameterized over two types: the ground type A and the effect signature E (more on it below).
Guarded Interaction Trees represent computational trees in which the leaves are of the ground type (\(\textsf{Ret}(a)\)), error states (\(\textsf{Err}(e)\)), and functions (\(\textsf{Fun}(f)\)). The leaves \(\textsf{Ret}(a)\) and \(\textsf{Fun}(f)\) are also called values, and we write \(\textbf{IT}^v_{E}(A)\) for the type of \(\textbf{IT}_{E}(A)\)-values.
The nodes of the computation trees are of the two kinds. The first one is a “silent step” constructor \(\textsf{Tau}(\alpha )\). It represents an unobservable internal step of the computation. For convenience, we use the function \(\textsf{Tick}\triangleq \textsf{Tau}\circ \textsf {next}\mathrel {:}\textbf{IT}_E(A) \rightarrow \textbf{IT}_E(A)\) that “delays” its argument. This function satisfies the following equation: \(\textsf{Tick}(\alpha ) = \textsf{Tick}(\beta ) \dashv \vdash \mathop {\triangleright }(\alpha = \beta )\).
The second kind of nodes are effects given by \(\textsf{Vis}_{i}(x,k)\). The parameters I, \( Ins \) and \( Outs \) are part of the effect signature E. The set I is the set of names of operations. The arities of an operation \(i\in I\) are given by functors \( Ins _{i}\) and \( Outs _{i}\). Let us give an example.
Consider the following signature for store effects. The signature \(E_{\textsf{state}}\) consists of effects \(\{\texttt{write}, \texttt{read}, \texttt{alloc}\}\) with the following input/output arities:
For example, \(\texttt{write}\) expect a location and a new GITree as its input, and simply returns the unit value as an output. We write \(\textsf{Vis}_{\texttt{write}}((\ell , \alpha ), \lambda \_.\, \beta )\) for the computation that invokes the \(\texttt{write}\) effect with arguments \(\ell \) and \(\alpha \), waits for it to return, and proceeds as \(\beta \). Thus, the first argument for \(\textsf{Vis}_{i}\) is the input, and the second one is the continuation dependent on the output. This continuation determines the branching in (G)Itrees.
For effects like above, it is usually convenient to provide wrappers:
When the signature and the return type are clear from the context, we simply write \(\textbf{IT}\) and \(\textbf{IT}^v\) for the GITrees and GITree-values. Equational theory. GITrees come with a number of operations (defined using the recursion principle) that are used for writing and composing computations. Here we list some of those operations which we will be using.
Fig. 3.
Example function on Guarded Interaction Trees.
The function \(\mathsf {get\_val}(\alpha , f : \textbf{IT}^v\rightarrow \textbf{IT})\) are used for sequencing computations, and its corresponding equations are shown in Figure 3. Intuitively, \(\mathsf {get\_val}(\alpha , f)\) first tries to compute \(\alpha \) to a value (a \(\textsf{Ret}(a)\) or a \(\textsf{Fun}(g)\)), and then calls f on that value. Similarly, \(\mathsf {get\_fun}(\alpha : \textbf{IT}, f : \mathord {\blacktriangleright }(\textbf{IT}\rightarrow \textbf{IT}) \rightarrow \textbf{IT})\) and \(\mathsf {get\_ret}(\alpha \mathrel {:}\textbf{IT}_E(A), f : A \rightarrow \textbf{IT}_E(A))\) first compute \(\alpha \) to a value; if that value is a function \(\textsf{Fun}(g)\) (resp., \(\textsf{Ret}(a)\)), then it proceeds with f(g) (resp., f(a)). Otherwise it results in an runtime error.
Crucially, to work with higher-order computations, GITrees provide the “call-by-value” application \(\alpha \mathrel {\bullet } \beta \) satisfying the following equations:
where \(- \mathrel {(\mathord {\blacktriangleright }\bullet )} -\) is defined as the lifting of \(- \mathrel {\bullet } -\) to \(\mathord {\blacktriangleright }\textbf{IT}_{E}(A) \rightarrow \mathord {\blacktriangleright }\textbf{IT}_{E}(A) \rightarrow \mathord {\blacktriangleright }\textbf{IT}_{E}(A)\), and \(\beta _v \in \textbf{IT}^v_{E}(A)\) is either \(\textsf{Ret}(a)\) or \(\textsf{Fun}(g)\).
The application function \(\alpha \mathrel {\bullet } \beta \) simulates strict function application. It first tries to evaluate \(\beta \) to a value \(\beta _{v}\). Then it tires to evaluate \(\alpha \) to a function f. If it succeeds, then it invokes \(f(\beta _{v})\). If at any point it fails, application results in a runtime error.
For the often-used case of GITrees where the ground type includes natural numbers, we use the function \(\textsf{NatOp}: (\mathbb {N} \rightarrow \mathbb {N} \rightarrow \mathbb {N}) \rightarrow IT \rightarrow IT \rightarrow IT\) which lifts binary functions on natural numbers to binary functions on GITrees. That is, \(\textsf{NatOp}_{f}(\alpha , \beta )\) first evaluate GITrees \(\beta \) and \(\alpha \) to values. If those values are natural numbers, then it computes f of those numbers and returns the result as a GITree. Otherwise, it returns a runtime error \(\textsf{Err}( RunTime )\).
Reification and reduction relation. The semantics for effects are given in terms of reifiers. A reifier for the signature E is a tuple \((\textit{State}, r)\), where \(\textit{State}\) is a type representing the internal state needed to reify the effects, and r is a reifier function of the type given in Figure 4. The idea is that \(r_{i}\) uses the internal state \(\textit{State}\) to compute the output of the effect i based on its input.
Fig. 4.
Signature of reifiers and the reification function
For example, for the store effects we take \(\textit{State}\) to be a map from locations to \(\mathord {\blacktriangleright }\textbf{IT}\) (representing the heap); and we define the following reifier functions:
Given reifiers for all the effects, we define a function \(\textsf{reify}: \textbf{IT}\times State \rightarrow \textbf{IT}\times State \) (as in Figure 4) that, given \((\alpha , \sigma )\) reifies the top-level effect in \(\alpha \) using the state \(\sigma \), and returns the reified GITree and the updated state.
The \(\textsf{reify}\) function is then used to give reduction semantics for GITrees . We write \((\alpha ,\sigma ) \rightsquigarrow (\beta , \sigma ')\) for such a reduction step. The definition of \(\rightsquigarrow \) is given internally in the logic:
That is, either \(\alpha \) is a “delayed” computation \(\textsf{Tick}(\beta )\), which then reduces to \(\beta \); or it is an effect that can be reified. Recall that we write \(\textsf{Tick}\) for the composition \(\textsf{Tau}\circ \textsf {next}\).
Note that the \(\textsf{reify}\) function operates on the top-level effect of the GITree. But what if the top-level constructor is not \(\textsf{Vis}\), e.g. if we have an effect inside an “evaluation context”? The role of evaluation contexts in GITrees is played by homomorphisms, which also allow us to bubble up necessary effects to the top of the GITree.
Definition 1 (Homomorphism)
A map \(f : \textbf{IT}\rightarrow \textbf{IT}\) is a homomorphism, written \(f \in Hom \), if it satisfies:
For example, \(\lambda x.\, \alpha \mathrel {\bullet } x\) is a homomorphism, and so is \(\lambda x.\, \mathsf {get\_val}(x, f)\). On the other hand, \(\lambda x.\, \textsf{Vis}_{\texttt{alloc}}(\textsf {next}(x), k)\) (for some fixed k) is not a homomorphism.
Program logic. In order to reason about GITrees, we employ the full power of the Iris separation logic framework. The program logic operates on the propositions of the form
. This weakest precondition proposition intuitively states that the GITree \(\alpha \) is safe to reduce, and when it fully reduces, the resulting value satisfies the predicate \(\varPhi \). Another important predicate is \(\mathsf {has\_state}(\sigma )\), which signifies ownership of the current state \(\sigma \).
Fig. 5.
Selected weakest precondition rules.
In Figure 5 we show the rules, on which we focus in this work. Let us describe their meaning. The rule wp-reify allows us to symbolically execute effects in GITrees . It is given in a general form, and is used to derive domain-specific rules for concrete effects. Another important rule is wp-hom which allows one to separate the reasoning about the computation from the reasoning about the context. The reason why wp-hom is sound (this is going to be important in the next section when we make it unsound), is because the reduction \(\rightsquigarrow \) of GITrees satisfies the following properties which allow one disentangle a homomorphism from the GITree it’s applied to:
If \((f(\alpha ), \sigma )\rightsquigarrow (\beta ',\sigma ')\) then either \(\alpha \) is a GITree-value, or there exists \(\beta \) such that \((\alpha ,\sigma )\rightsquigarrow (\beta ,\sigma ')\) and \(\mathop {\triangleright }(f(\beta ) = \beta ')\).
Finally, as usual in Iris, the program logic satisfies an adequacy property, which allows one to relate propositions proved in the logic to the actual semantics:
Theorem 1
Let \(\alpha \) be an interaction tree and \(\sigma \) be a state such that
is derivable for some meta-level predicate \(\varPhi \) (containing only intuitionistic logic connectives). Then for any \(\beta \) and \(\sigma '\) such that \((\alpha , \sigma ) \rightsquigarrow ^{*} (\beta ,\sigma ')\), one of the following two things hold:
(adequacy) either \(\beta \in \textbf{IT}^v\), and \(\varPhi (\beta )\) holds in the meta-logic;
(safety) or there are \(\beta _1\) and \(\sigma _1\) such that \((\beta ,\sigma ')\rightsquigarrow (\beta _1,\sigma _1)\)
In particular, safety implies that \(\beta \ne \textsf{Err}(e)\) for any error \(e \in \texttt{Error}\).
The role of meta-logic is played by the Coq system; thus, the adequacy theorem allows us to relate proofs inside the program logic (Iris) to the proofs on the level of Coq. This aspect is important in Iris and GITrees in general, but it is orthogonal to the work that we present in this paper. See [13] for more details.
3 Context-Dependent Reification
In this section we extend reification to handle context-dependent effects, using a language \(\lambda _{\textsf{callcc}}\) with call/cc as a concrete example. In Section 3.1 we present \(\lambda _{\textsf{callcc}}\)’s syntax and operational semantics (in the usual style with evaluation contexts). We then show why the current GITrees framework cannot be used as a denotational model for \(\lambda _{\textsf{callcc}}\) directly. In Section 3.2 we introduce our generalization of reification for context-dependent effects and corresponding extensions to the GITrees program logic. In Section 3.3 we demonstrate that our extension works as intended: we give a denotational semantics for \(\lambda _{\textsf{callcc}}\), and we show how the general program logic for GITrees specializes to a logic for reasoning about call/cc. We prove soundness and computational adequacy of denotational semantics using a logical relation defined within our program logic.
3.1 Operational Semantics and Type System for \(\lambda _{\textsf{callcc}}\)
By \(\lambda _{\textsf{callcc}}\) we denote a simply-typed \(\lambda \)-calculus with natural numbers, recursive functions, and call/cc. The relevant pieces of syntax, the type system and the operational semantics are given in Figure 6. The type system includes natural numbers, function types, and the type \( cont ({\tau })\) of continuations. The
expression takes the current evaluation context and binds it to \(x\) in \(e\). The
expression evaluates passes the first argument (value) to the second argument (continuation, represented as an evaluation context).
The operational semantics of \(\lambda _{\textsf{callcc}}\) is separated into two layers. The first layer consists of local reductions of primitive expressions (\({e}\mapsto _{K}{e'}\)), and the second layer lifts local reductions to reductions among complete programs (\({{K}[{e}]}\mapsto {{K'}[{e'}]}\)). The local reductions are parameterized by an evaluation context K, which allows
to capture the evaluation context.
Fig. 6.
Syntax and fragments of type system and operational semantics of \(\lambda _{\textsf{callcc}}\).
Let us now consider what happens if we try to give a direct-style denotational semantics of \(\lambda _{\textsf{callcc}}\) into GITrees. By direct we mean that we wish to give a direct interpretation of types and expressions, rather than going through a global CPS conversion. To define the semantics, we first need to provide an effect signature, state, and reifiers for each effect, and then we can define the interpretation of the expressions of the language.
The effect signature, shown in Figure 7, contains two effects \(\texttt{callcc}\) and \(\texttt{throw}\). Since call/cc binds a continuation, it is natural to let the input arity for \(\texttt{callcc}\) be a callback \((\mathord {\blacktriangleright }\textbf{IT}\rightarrow \mathord {\blacktriangleright }\textbf{IT}) \rightarrow \mathord {\blacktriangleright }\textbf{IT}\). The output arity is simply \(\mathord {\blacktriangleright }\textbf{IT}\).
The input arity for \(\texttt{throw}\) signifies that throw takes as input an expression and a continuation, which are represented respectively as \(\mathord {\blacktriangleright }\textbf{IT}\) and \(\mathord {\blacktriangleright }(\textbf{IT}\rightarrow \textbf{IT})\). The output arity of \(\texttt{throw}\) is simply the empty type 0, because throw never returns.
Note that the input types of \(\texttt{callcc}\) and \(\texttt{throw}\) have slightly different arities. However, we can always transform \(f \mathrel {:}(\mathord {\blacktriangleright }X \rightarrow \mathord {\blacktriangleright }X)\) into an element of type \(\mathord {\blacktriangleright }(X \rightarrow X)\) by performing a silent step in the function’s body: \(f' \triangleq \textsf {next}(\lambda x.\, \textsf{Tau}(f (\textsf {next}(x))))\). And we can always transform \(f \mathrel {:}\mathord {\blacktriangleright }(X \rightarrow X)\) into an element of type \(\mathord {\blacktriangleright }X \rightarrow \mathord {\blacktriangleright }X\) using the applicative structure of the later modality.
For convenience, we will use the abbreviations
and \(\textrm{Throw}(e)\), defined in Figure 7, for representing denotations of throw and call/cc as effects in GITrees.
Fig. 7.
Signatures and operations on GITrees with call/cc.
To complete all the ingredients for the denotational semantics, we need reifiers for the \(\texttt{callcc}\) and \(\texttt{throw}\) effects. Given our operational understanding of continuations, the natural choice for the local state type \(\textit{State}\) is \(\textbf{1}\) (since we do not have any state). However, the current reifier signature (Figure 4) poses a problem. Reifiers, as they are now, cannot access their current continuation, which is essential for both effects.
needs to pass the current continuation to f, while \(\textrm{Throw}\) must redirect control to a provided continuation instead of returning normally. The current reifiers lacks this capability, and in the next subsection we show how to generalize the notion of reification to context-dependent effects.
3.2 Context-dependent Reifiers
This section presents our extension to context-dependent reification, and the limitations it imposes on the program logic. In order to allow reifiers to manage continuations, we change the type of reifiers to accept continuations as an extra parameter, as shown in Figure 8. Continuations for a given effect are functions from the effect’s outputs to GITrees : \( Outs _i(\textbf{IT}_E) \rightarrow \mathord {\blacktriangleright }\textbf{IT}_E\).
Fig. 8.
Type of context-dependent reifiers and the context-dependent reify function
Given a set of context-dependent reifiers, we define a context-dependent \(\texttt{reify}\) function, also shown in Figure 8. As before, \(\texttt{reify}\) dispatches to the correct individual reifier for the effect. Note that now it is the user’s responsibility to pass the output of an effect to the given continuation if the control flow is not supposed to be interrupted. For example, since the evaluation of a
expression does not modify the control flow itself, but simply passes the current continuation to its body, the context-dependent reifier for \(\texttt{callcc}\) is simply \(r_{\texttt{callcc}} (x, \sigma , \kappa ) = \textsf{Some}(\kappa ~(x~\kappa ), \sigma )\).
Before we move on to discussing the consequences of this for program logic, we would like to note that our treatment of continuation (with top-level reifiers dispatching them) parallels Cartwright and Felleisen’s “extensible direct models” [9], which also aimed to support extensible denotational semantics in classical domain theory. We discuss this more in Section 6.
Program logic for GITrees in the presence of context-dependent reifiers. To reflect the generalization to context-dependent reifiers in the program logic, we replace the proof rule wp-reify by wp-reify-ctx-dep, shown in Figure 9. This is, however, not the only change we need to make. In the presence of context-dependent effects, wp-hom is not sound! (A similar observation was also made by [28] in their development of a program logic for call/cc.) The reason is that context-dependent reification invalidates Lemma 1. Now, since wp-hom is not sound anymore, one might expect that we need to adapt all the other program logic rules to include a homomorphism similarly to how the rules of [28] were adapted to include an evaluation context. However, this is not necessary, because our program logic is defined on denotations on which we have a non-trivial equational theory, which can be used to reason about ‘pure’ GITrees. Only for effectful operations, the proof rules will now have to include a surrounding homomorphism. E.g., wp-write from [13] is generalized to wp-write-ctx-dep, and considers ambient homomorphisms explicitly.
Fig. 9.
Program logic in the presence of context-dependent reifiers.
Our context-dependent reification extension, though simple, allows us to build sound and adequate denotational models for languages with control-flow operators, including \(\lambda _{\textsf{callcc}}\) (shown in the next subsection). Moreover, our extension is conservative, and we recover previous case studies (computational adequacy of \(\lambda _{\textsf{rec},\textsf{io}}\) and type safety for \(\lambda _{\mathsf {\multimap },\textsf{ref}}\) [13]) with minimal modifications; see the accompanying Coq formalization.
3.3 Denotational Semantics of \(\lambda _{\textsf{callcc}}\)
In this section we show that context-dependent reifiers are sufficient for providing a sound and adequate semantic model of \(\lambda _{\textsf{callcc}}\). We define context-dependent reifiers for \(\texttt{callcc}\) and \(\texttt{throw}\), then prove that this gives a sound interpretation w.r.t. operational semantics. To show adequacy, we define a logical relation, which relates the denotational and operational semantics. The logical relation is defined in the (updated) program logic for GITrees (following the approach in [13]), and validates the utility of the program logic.
Fig. 10.
Denotational semantics of \(\lambda _{\textsf{callcc}}\) (selected clauses).
Interpretation of\(\lambda _{\textsf{callcc}}\). The denotational semantics of \(\lambda _{\textsf{callcc}}\) is shown in Figure 10 (selected clauses only; see Coq formalization for the complete definition). The interpretation is split into three parts: \(\textbf{E}\llbracket {-}\rrbracket \) for expressions, \(\textbf{V}\llbracket {-}\rrbracket \) for values, and \(\textbf{K}\llbracket {-}\rrbracket \) for contexts. For the interpretation of
, the left-to-right evaluation order is enforced by the functions \(\mathsf {get\_val}\) and \(\mathsf {get\_fun}\). They first evaluate their argument to a GITree value, and then pass it on (c.f. Figure 3).
The context-dependent reifiers for the effects \(\texttt{callcc}\) and \(\texttt{throw}\) are defined as follows:
To show that the denotational semantics is sound, we need the following lemma that shows that interpretations of expressions in evaluation contexts are decomposed into applications of homomorphisms.
Lemma 2
For any context K and an environment \(\rho \), we have \(\textbf{K}\llbracket {K}\rrbracket _\rho \in Hom \). For any context K, expression \(e\), and an environment \(\rho \), \(\textbf{E}\llbracket {{K}[{e}]}\rrbracket _\rho = \textbf{K}\llbracket {K}\rrbracket _\rho (\textbf{E}\llbracket {e}\rrbracket _\rho )\).
With these results at hand, we can show soundness of our interpretation:
Lemma 3
Soundness. Suppose \({e_1}\mapsto {e_2}\). Then \((\textbf{E}\llbracket {e_1}\rrbracket _\rho , ()) \rightsquigarrow ^* (\textbf{E}\llbracket {e_2}\rrbracket _\rho , ())\), where \(() \mathrel {:}\textbf{1}\) is the unique element of the unit type, representing the (lack of) state.
Program logic for\(\lambda _{\textsf{callcc}}\). We now specialize the general program logic rule wp-reify-ctx-dep using the reifiers for \(\texttt{callcc}\) and \(\texttt{throw}\) to obtain the following program logic rules:
where \(\kappa \) is a homomorphism representing the current evaluation context on the level of GITrees. The reader may wonder why these rules include the \(\mathsf {has\_state}{(\sigma )}\) predicates, since it is just ’threaded around’. The reason is that these rules also apply when there are other effects around and the state is composed of different substates for different effects, cf. the discussion of modularity in Section 2.
Adequacy and logical relation. Having established soundness, we now turn our attention to adequacy, which is usually much more complicated to prove.
Lemma 4
Adequacy. Suppose that \({\emptyset }\vdash {e}\mathrel {:}{\mathbb {N}}\) and \((\textbf{E}\llbracket {e}\rrbracket _{\emptyset }, \sigma _1) \rightsquigarrow ^* (\textsf{Ret}(n), \sigma _2)\), for a natural number n. Then \({e}\mapsto ^{*}{n}\).
To prove Lemma 4, we define a logical relation between syntax (\(\lambda _{\textsf{callcc}}\) programs) and semantics (GITrees denotations) using the program logic from Figure 11. To handle control effects, we use a biorthogonal logical relation [23], adapted from [28] for adequacy, following the Iris approach [30].
The core observational refinement \(\mathcal {O}(\alpha , e)\) ensures that if \(\alpha \) reduces to a GITree value \(\textbf{IT}^v\), then this value is a natural number, and \(e\) also reduces to the same number. The evaluation context relation \(\mathcal {K}(P)(\kappa , K)\) relates homomorphisms and evaluation contexts when they map related arguments to expressions satisfying \(\mathcal {O}\). The expression relation \(\mathcal {E}(P)(\alpha , e)\) connects related \(\textbf{IT}\)’s and expressions in related evaluation contexts. Types are inductively interpreted: functions relate if they map related arguments to related results, and continuations relate via the context relation. For open terms, the validity judgment \(\varGamma \vDash e\mathrel {:}\tau \) uses closing substitutions, with \(e[\gamma ]\) denoting applying a substitution \(\gamma \) to \(e\).
Fig. 11.
Logical relation for \(\lambda _{\textsf{callcc}}\).
The proof of adequacy relies on the fact that the interpretation of evaluation contexts are homomorphisms, which allows us to use a limited version of the bind rule:
Lemma 5
Limited bind rule. If \(\mathcal {E}(P)(\alpha , e)\) and \(\mathcal {K}(P)(\kappa , K)\), then \(\mathcal {O}({\kappa }\;{\alpha }, {K}[{e}])\).
With this in mind we show the fundamental lemma, stating that every well-typed expression is related to its own interpretation:
Lemma 6
Fundamental lemma. Let \({\varGamma }\vdash {e}\mathrel {:}{\tau }\) then \(\varGamma \vDash e\mathrel {:}\tau \).
Computational adequacy now follows easily from the fundamental lemma.
Proof
(of Lemma 4). By Lemma 6, we have that \({\emptyset }\vdash {e}\mathrel {:}{\mathbb {N}}\) implies that \(\emptyset \vDash e\mathrel {:}\mathbb {N}\). Now, the statement follows from Theorem 1 and the assumption that \(\textbf{E}\llbracket {e}\rrbracket _{\emptyset }, \sigma _1 \rightsquigarrow ^* \textsf{Ret}~n, \sigma _2\).
4 Modeling Delimited Continuations
In this section we scale our approach to delimited continuations, which is a challenging example of context-dependent effects. We provide a denotational semantics for a programming language \(\lambda _{\textsf{delim}}\) with shift/reset, and prove its soundness and adequacy relative to an abstract machine semantics [6]. The semantics and proofs are more complex than for \(\lambda _{\textsf{callcc}}\) due to the nature of delimited continuations and associated type system. To the best of our knowledge, this represents the first formalized sound and adequate direct-style denotational semantics for delimited continuations.
Fig. 12.
Syntax and typing rules of \(\lambda _{\textsf{delim}}\).
Fig. 13.
Operational semantics of \(\lambda _{\textsf{delim}}\) (excerpt).
4.1 Syntax and Operational Semantics of \(\lambda _{\textsf{delim}}\)
The syntax and the type system of \(\lambda _{\textsf{delim}}\) is given in Figure 12. It is similar to \(\lambda _{\textsf{callcc}}\), but instead of
there are operators
(delimit the current evaluation context, also known as reset) and
(grab the current delimited continuation, and bind it to \(x\) in \(e\), also known as shift).
The type system follows Danvy and Filinski [10], extending simply-typed \(\lambda \)-calculus with answer types \(\alpha \), \(\beta \). The main typing judgment \({\varGamma }; {\alpha } \vdash {e} \mathrel {:}{\tau }; {\beta }\) means: under the typing context \(\varGamma \), expression \(e\) can be plugged into a context expecting a value of type \(\tau \) and producing a value of type \(\alpha \); in that case the resulting program will have the type \(\beta \). You can think of it a computation \(\varGamma \rightarrow (\tau \rightarrow \alpha ) \rightarrow \beta \) under the CPS translation. Thus, the type of the (delimited) continuation corresponds to \(\tau \rightarrow \alpha \), while the type of the overall expression is \(\beta \). The pure typing judgment \({\varGamma } \vdash _{\textsf{pure}} {e} \mathrel {:}{\tau }\) indicates \(e\) does not depend on the surrounded context, and is context-independent for any answer types. Expressions can change their context’s answer type, as seen in the
typing rule.
For example, suppose we extend the type system with booleans, \(\mathbb {B}\), and add a primitive function \(\textsf{isprime}\) that does not modify answer types. That is \({\emptyset }; {\alpha } \vdash {\textsf{isprime}} \mathrel {:}{{\mathbb {N}/\beta }\mathop {{\mathsf {\rightarrow }}}{\mathbb {B}/\beta }}; {\alpha }\). The expression
is well-typed in this type system as a \(\mathbb {N}\), even though it changes the answer type from \(\mathbb {B}\) to \(\mathbb {N}\).
Answer types appear in both judgments and type constructors. Continuation type
represents contexts expecting something of the type \(\tau \) and producing something of the type \(\alpha \). Function type \({\sigma /\alpha }\mathop {{\mathsf {\rightarrow }}}{\tau /\beta }\), in addition to the input type \(\sigma \) and the output type \(\tau \), record the typing of the surrounding context at the point of the function call. See [10] for details.
The operational semantics for \(\lambda _{\textsf{delim}}\) uses a CEK machine, following [5, 6, 12]. Selected reduction rules appear in Figure 13 (see Coq formalization for the full set of rules). The abstract machine operates on various configurations, which can be of several forms. The first one is the initial configuration \({\langle e \rangle }_{\textsf{term}}\), which is just a starting state for evaluating expressions. Similarly, there is a terminal configuration \({\langle v \rangle }_{\textsf{ret}}\) signifying that the program has terminated with the value \(v\).
From the initial configuration, we go on to \({\langle e,\ K,\ mk \rangle }_{\textsf{eval}}\), which signifies that we are evaluating an expression \(e\) inside the current delimited context K, with the metacontinuation mk (a stack of continuations based on different delimiters). It is this configuration type which takes care of delimited control operations. The
operator saves the current continuation on top of the metacontinuation, limiting the scope of
. The
operation behaves similarly to
, except that it prevents later control operators from capturing its evaluation context.
The last two configuration types are for dealing with continuations and metacontinuations. A configuration \({\langle K,\ v,\ mk \rangle }_{\textsf{cont}}\) signifies that we are trying to plug in the value \(v\) into the context K, with the metacontinuation mk. A configuration \({\langle mk,\ v \rangle }_{\textsf{mcont}}\) signifies that we are done with the current continuation (ending with the value v), but we still have to unwind the continuation stack mk.
Fig. 14.
Effects for \(\lambda _{\textsf{delim}}\).
4.2 Denotational Semantics of \(\lambda _{\textsf{delim}}\)
Our model represents delimited continuations with effects mimicking an abstract machine, operating on semantic rather than syntactic components. The effect signature and reifiers (Figure 14) define a state with a stack of continuations, manipulated explicitly. The effect signature \(E_{\lambda _{\textsf{delim}}}\) includes four operators: \( \{\texttt{reset}, \texttt{shift}, \texttt{pop}, \texttt{appcont}\}. \) The signature of \(\texttt{reset}\) simply tells us that the corresponding effect does not directly modify its argument. The auxiliary effect \(\texttt{pop}\), which does not have an equivalent in the surface syntax, is used to enforce unwinding of the continuation stack. As the output arity of \(\texttt{pop}\) signifies, it does not return. We describe the importance of that below. The rest of the signature is more straightforward: \(\texttt{shift}\) and \(\texttt{appcont}\) are defined exactly as \(\texttt{callcc}\) and \(\texttt{throw}\). The semantics of these effects, in terms of reification, is more intricate. As we mentioned, the state for reification is \(\textit{State}= List (\mathord {\blacktriangleright }\textbf{IT}\rightarrow \mathord {\blacktriangleright }\textbf{IT})\).
In comparison with
, the control operator
does not necessarily continue from the same continuation; hence, the corresponding reifier passes the current continuation to the body, but does not return control back. The reifier for \(\texttt{reset}\) simply saves the current continuation \(\kappa \) onto the stack \(\sigma \). It is then the job of the \(\texttt{pop}\) operation to restore the continuation from the stack. The reifier for \(\texttt{shift}\) is similar to that of \(\texttt{callcc}\), except that it removes the current continuation entirely. The reifier for \(\texttt{appcont}\), in comparison with \(\texttt{throw}\), does not simply pass control, but also saves the current continuation on the stack. This corresponds to the fact that whenever a delimited continuation is invoked, the result is wrapped in a reset; that is done to prevent the continuation from escaping the delimiter.
Fig. 15.
Weakest precondition rules for delimited continuations.
As part of instantiating GITrees with these effects, we obtain the specialized program logic rules shown in Figure 15. We will use those rules later for defining a logical relation between the syntax and the semantics of \(\lambda _{\textsf{delim}}\).
Fig. 16.
Denotational semantics for a calculus with delimited control (selected clauses).
As mentioned above, we will use \(\textsf{Pop}\) to unwind the continuation stack and restore the continuation after finishing with a \(\texttt{reset}\). This means that we will need to insert explicit calls to \(\textsf{Pop}\) in the interpretation of \(\lambda _{\textsf{delim}}\). For these purposes, we use an abbreviation \(\textbf{P}(\beta )\), which first evaluates \(\beta \) to a value, and then executes the \(\texttt{pop}\) operation.
The interpretation of \(\lambda _{\textsf{delim}}\) uses this auxiliary function and is given in Figure 16. Similarly to the operational semantics, the interpretation is divided into five categories. First, we have \(\textbf{E}\llbracket {-}\rrbracket \) and \(\textbf{V}\llbracket {-}\rrbracket \) for the interpretation of expressions and values, which is what we need for the surface syntax. All of those interpretations return GITrees . Note that in the interpretation of
we insert explicit calls to \(\textbf{P}\), and similarly in the interpretation of continuations.
The other group of interpretations, \(\textbf{K}\llbracket {-}\rrbracket \), \(\textbf{M}\llbracket {-}\rrbracket \) and \(\textbf{S}\llbracket {-}\rrbracket \), are for interpreting continuations, metacontinuations, and other configurations; these are used for showing soundness (preservation of operational semantics by the interpretation). The interpretation \(\textbf{K}\llbracket {-}\rrbracket \) of continuations returns a semantic continuation (a function \(\textbf{IT}\rightarrow \textbf{IT}\)). Similarly, the interpretations \(\textbf{M}\llbracket {-}\rrbracket \) (resp. \(\textbf{S}\llbracket {-}\rrbracket \)) of metacontinuations (resp. configurations) returns a stack of semantic continuations (resp. a semantic configuration).
We now show that our interpretation is sound w.r.t. the abstract machine semantics. For this we prove lemmas similar to Lemma 2, and put them to use in the soundness theorem:
Theorem 2
Soundness. Let \(c_0, c_1 \in Config \) and suppose \({c_0}\mapsto {c_1}\). Then \(\textbf{S}\llbracket {c_{0}}\rrbracket \rightsquigarrow ^* \textbf{S}\llbracket {c_{1}}\rrbracket \).
4.3 Logical Relation and Adequacy
We now show that our denotational semantics is adequate with regards to the abstract machine semantics. Specifically, we show the following result:
Theorem 3
Adequacy. Suppose \({\emptyset }; {\mathbb {N}} \vdash {e} \mathrel {:}{\mathbb {N}}; {\mathbb {N}}\) is a well-typed term, and that \(\left( \textbf{P}(\textbf{E}\llbracket {e}\rrbracket _{\emptyset }), []\right) \rightsquigarrow ^* \left( \textsf{Ret}(n), \sigma \right) \) for a natural number n and a metacontinuation \(\sigma \). Then \({{\langle e \rangle }_{\textsf{term}}}\mapsto ^{*}{{\langle n \rangle }_{\textsf{ret}}}\).
Fig. 17.
Logical relation for \(\lambda _{\textsf{delim}}\).
We prove adequacy using a logical relation. It relates expressions to their interpretations and also connects syntactic and semantic configurations. The logical relation is shown in Figure 17. It is again a form of biorthogonal logical relation, with the main focus being the observational refinement \(\mathcal {O}\): two configurations are related if they reduce to the same natural number. This coincides with what we want to show in Theorem 3. To facilitate this we then lift \(\mathcal {O}\) to the levels of metacontinuations, continuations and expressions. The relation \(\mathcal {M}(P)\), where \(P : \textrm{VRel}\) is a relation on values, states that two metacontinuations are related if, whenever we plug in P-related values, the resulting configurations become \(\mathcal {O}\)-related. Both \(\mathcal {M}\) and \(\mathcal {O}\) are then used to define the relation between semantic and syntactic continuations. The relation \(\mathcal {K}(Q, P)\), where \(P, Q : \textrm{VRel}\) are relations on values, states that two continuations are related if, whenever we plug them into Q-related metacontinuations with P-related values, the resulting configurations become \(\mathcal {O}\)-related. Finally, we use \(\mathcal {K}, \mathcal {M}\), and \(\mathcal {O}\) to define the relation between GITrees and \(\lambda _{\textsf{delim}}\) terms. The relation \(\mathcal {E}(P, Q, R)\), where \(P, Q, R : \textrm{VRel}\) are relations on values, states that \(\beta \) is related to e if, whenever we plug them into (P, Q)-related continuations and an R-related metacontinuation, the resulting configurations become \(\mathcal {O}\)-related.
The relations \(\mathcal {E}\) and \(\mathcal {K}\) are used to give semantics \(\llbracket {\tau }\rrbracket \) to types. The idea is that \(\mathcal {E}{(\llbracket {\tau }\rrbracket , \llbracket {\alpha }\rrbracket , \llbracket {\beta }\rrbracket )}\) relates terms \(\emptyset ; \alpha \vdash e : \tau ; \beta \) to their semantic counterparts. This is then used, as expected for logical relations, for defining the logical relation for function types and for open terms. The relation \(\llbracket {\varGamma }\rrbracket (\rho , \gamma )\) relates the semantic environment \(\rho : \textit{Var}\rightarrow \textbf{IT}\) to the syntactic substitution \(\gamma : \textit{Var}\rightarrow \textit{Expr}\); they are related if they map the same variables to related GITrees/expressions. Then we say that an expression e is semantically valid, \(\varGamma ; \alpha \vdash e : \tau ; \beta \), if its interpretation \(\textbf{E}\llbracket {e}\rrbracket _{\rho }\) is related to \(e[\gamma ]\) under related substitutions \(\rho , \gamma \). Note that if we ignore the answer types we can see that the logical relation exhibits a lot of similarities to the logical relation we gave in Section 3.3, and follows the same roadmap.
For this logical relation we obtain the fundamental property, which we will use for the proof of adequacy.
Lemma 7
Fundamental lemma. Let \({\varGamma }; {\alpha } \vdash {e} \mathrel {:}{\tau }; {\beta }\) then \(\varGamma ; \alpha \vDash e\mathrel {:}\tau ; \beta \); and if \({\varGamma } \vdash _{\textsf{pure}} {e} \mathrel {:}{\tau }\) then \(\varGamma \vDash _{\textsf{pure}} e\mathrel {:}\tau \).
Proof
(of Theorem 3). Note that the empty (meta)continuation is related to its denotation: \(\mathcal {K}(P, P)(\textsf{id}, \square )\) and \(\mathcal {M}(P)([], [])\) hold for any relation P.
With this, we instantiate \(\emptyset ; \mathbb {N} \models e : \mathbb {N}; \mathbb {N}\) (that we get from Lemma 7) with the empty continuation/metacontinuation, and get the observational refinement between e and \(\textbf{E}\llbracket {e}\rrbracket \). \(\square \)
This completes our treatment of denotational semantics of \(\lambda _{\textsf{delim}}\). The next section examines interoperability of delimited continuations and other effects.
5 Modeling Interoperability Between Languages
A key advantage of using (G)Itrees for semantics is that they can provide a common framework for multi-language interaction. This section presents a case study on the interaction between the languages \(\lambda _{\textsf{embed}}\) (with higher-order store effects) and \(\lambda _{\textsf{delim}}\) (with delimited continuations). Specifically, we allow embedding closed \(\lambda _{\textsf{delim}}\) programs into \(\lambda _{\textsf{embed}}\), and equip \(\lambda _{\textsf{embed}}\) with a type system that guarantees safe interoperability.
The embedding we provide is restrictive, preventing programs with delimited continuations from accessing outer-language continuations. We leave developing a more permissive type system for future work. At the end of the section we give an example of how to verify a more involved interaction of effects, albeit without the type system.
In this section we reuse the semantics of \(\lambda _{\textsf{delim}}\) from the previous section and higher-order store effects from Section 2. For \(\lambda _{\textsf{delim}}\), we reuse the semantics from the previous section and higher-order store reifiers from [13] In this section, we use
to explicitly highlight programs written in \(\lambda _{\textsf{delim}}\), and for the interpretation functions of the denotational model of \(\lambda _{\textsf{delim}}\).
Language\(\lambda _{\textsf{embed}}\).
Fig. 18.
Syntax and the new typing rule of the \(\lambda _{\textsf{embed}}\).
\(\lambda _{\textsf{embed}}\) is a \(\lambda \)-calculus with base types \(\mathbb {N}\) and \(\textbf{1}\), references types \(\textsf{ref}(\tau )\) and function types \({\tau }\mathop {{\mathsf {\rightarrow }}}{\sigma }\), with syntax given in Figure 18. Additionally, it includes a construct
for embedding \(\lambda _{\textsf{delim}}\) programs. The typing rules are all standard, except for the new typing rule for the embedding.
The idea behind the rule is that we can embed an expression from \(\lambda _{\textsf{delim}}\) if it is a “pure” expression that can evaluate to a natural number. The use of pure typing judgment for the embedded program ensures that it does not to alter the answer type. This means that we can treat an embedded expression as a “complete” program, that does not require outer continuation delimiters, even though it may rely on delimited continuations internally. Those restrictions are crucial for the type safety of the embedding. The typing guarantees that \(e\) does not expect any additional delimiters, but it does not, by itself guarantee that any continuations in \(e\) escape the embedding boundary. To prevent that we enforce the continuation delimiter along the embedding boundary in the interpretation of embedded expressions.
Denotational model of\(\lambda _{\textsf{embed}}\). For denotational semantics of \(\lambda _{\textsf{embed}}\), we start by defining reifiers for the effect signature, which includes higher-order store operations (allocating, reading, and storing references) as \(E_{\texttt {state}}\), and effects related to delimited continuations (\(E_{\lambda _{\textsf{delim}}}\)). Then the combined effect signature is \(E_{\lambda _{\textsf{delim}}} \times E_{\texttt {state}}\), and thus we also let \(\textit{State}\triangleq \textit{State}_{\texttt {delim}} \times \textit{State}_{\texttt {state}}\), and reifiers are defined component-wise.
Fig. 19.
Denotational semantics (selected clauses) and logical relation for \(\lambda _{\textsf{embed}}\).
Figure 19 shows the key parts of the denotational semantics. For most of the syntactic constructs we give the standard interpretation. For
we use the interpretation
for \(\lambda _{\textsf{delim}}\) from Section 4.2, and explicitly wrap the resulting GITree in a \(\textsf{Reset}\). This continuation delimiter acts as a sort of glue code to protect the rest of the program from being captured by control operators from the embedded \(\lambda _{\textsf{delim}}\) program.
To show type safety of \(\lambda _{\textsf{embed}}\), we construct a logical relation (shown in Figure 19), which is similar to the other logical relations we considered in this paper, mainly different in the observation relation \(\mathcal {O}\). Given that the type system for \(\lambda _{\textsf{embed}}\) effectively prevents expressions of \(\lambda _{\textsf{delim}}\) to access contexts from \(\lambda _{\textsf{embed}}\), we refine the observation relation to get access to a version of the wp-hom rule for expression interpretations of well-typed programs of \(\lambda _{\textsf{embed}}\), which we do not have in general, as discussed in Section 3.
Instead of the standard weakest precondition \(\textsf {wp}\), we utilize a context-local weakest precondition\(\textsf {clwpre}\) which bakes-in the bind rules [28].
Definition 2
Context-local weakest precondition (\(\textsf {clwp}\)) is defined as follows:
Note that \(\textsf {clwp}\) always implies \(\textsf {wp}\) and validates a form of the bind rule:
for any homomorphism \(\kappa \). We use the \(\textsf {clwp}\) in the definition of observational refinement in the model. Observational refinement asserts that if the evaluation of a top-level expression of \(\lambda _{\textsf{embed}}\) starts with an empty continuation stack, then the evaluation does not introduce new elements into the continuation stack. By using \(\textsf {clwp}\) we get a semantical bind lemma, which can be seen as a version of wp-hom for semantically valid expressions of \(\lambda _{\textsf{embed}}\). As before, we then obtain fundamental lemma and denotational type soundness.
Lemma 8
Semantical bind. \(\mathcal {E}(\lambda x \mathrel {:}\textbf{IT}^v.\, \mathcal {E}(P)({\kappa }\;{x}))(\beta )\) implies \(\mathcal {E}(P)({\kappa }\;{\beta })\) for any homomorphism \(\kappa \).
Lemma 9
Fundamental lemma. Let \({\varGamma }\vdash {e}\mathrel {:}{\tau }\) then \(\varGamma \vDash e \mathrel {:}\tau \).
Lemma 10
Denotational type soundness. Let \({\emptyset }\vdash {e}\mathrel {:}{\tau }\) and \((\textbf{E}\llbracket {e}\rrbracket _{\emptyset }, []) \rightsquigarrow ^* (\alpha , \sigma )\), then \((\exists \beta \; \sigma '.\, (\alpha , \sigma ) \rightsquigarrow (\beta , \sigma ')) \vee (\alpha \in \textbf{IT}^v)\).
Unrestricted interaction of delimited continuations and higher-order state. Even though the type system we considered here is restrictive, we can still reason about unrestricted interactions of events in the “untyped” setting. Here we show an example of such an unrestricted interaction, and demonstrate how to reason about context-dependent and context-independent effects at the same time. While this kind of interactions is forbidden by our type system, we can still write and prove meaningful specifications for such programs.
Fig. 20.
Example program with delimited continuations and state and its specification.
Consider the program in Figure 20, written in GITrees directly. The function prog utilizes both delimited continuations and state. It takes a reference y as its argument and begins by allocating the value 1 in the store at reference x. Then it captures the continuation \( \mathsf {get\_ret}(y, (\lambda l. \textsf{Let} \,p \mathrel {=} \textsf{NatOp}_+ (\textsf{Read}(l), \dots ) \,\textsf{in} \, \textsf{Write}(l,~\hbox {p)))} \) as k. Invoking the continuation k with a number n increments the current value of y by n. The program then invokes this continuation twice. First with the original value of x. Then, with an incremented value of x. Since the starting value of x is 1, the reference y is incremented first by 1 and then by 2. We capture this behavior in the specification for prog stated in Figure 20.
It is important to note that this program features a bidirectional interaction between state and continuations. Specifically, the body of \(\textsf{Shift}\) involves state operations, while the result of \(\textsf{Shift}\) is subsequently used to increment a value in the heap. As we have seen, while this type of interaction is not allowed in the type system, we can still reason about them in program logic. We stipulate that our proposed type system could potentially be extended to support embedding “pure” functions, allowing for bi-directional interaction between the two languages. We believe that such an extension would require implementing answer-type polymorphism, following the approach of Asai and Kameyama [2].
6 Discussion and Related Work
We conclude the paper by discussing related work and future directions.
This paper extends GITrees to handle context-dependent effects, which allows us to model higher-order languages with control operators like
and
. We showed this extension supports interoperability between languages with different context-dependent effects, while preserving reasoning about context-independent effects. Our approach leverages the native support for higher-order functions and effects in GITrees. This differs from the first-order effect representation of effects in ITrees [34], which would require explicitly first-order representation of functions and continuations, if we want to model first-class continuation. Such model would mix syntactic and semantic concerns, which is part of what we are trying to avoid by working with (G)ITrees.
Another difference with ITrees is our approach to reasoning. While ITrees use bisimulation-based equational theory, we follow GITrees in using tailored program logics and defining refinements. Our logic are expressive enough to define logical relations and carry out computational adequacy proofs. In future work, it would be interesting to develop techniques for reasoning about weaker notions of equality than the basic equational theory that GITrees comes equipped with, see the more extensive discussion of this point in [13].
The “classical” domain theory remains an important source of inspiration and ideas for our development, and we want to mention some of the related work along those lines. Cartwright and Felleisen [9] introduced a framework of extensible direct models for constructing modular denotational semantics of programming languages. Their framework centers on an abstract notion of resources for representing effects (such as store or continuations) and a central admin function that manages these resources. Each language extension defines both the types (domains) of additional values and resources, and specifies the actions that the admin function can perform on these resources. Building on this framework, Sitaram and Felleisen [26] demonstrated that such models can provide direct-style fully abstract semantics for control operators. Their approach interprets effects, including continuations, by delegating them to a top-level handler. Our work adopts several key ideas from this line of research but reformulates them in the context of GITrees rather than classical domain theory. In our framework, effect signatures define resources, reifiers specify actions, and the reduction relation serves as the central authority dispatching the effects. The transition to GITrees enables us to formalize the extensibility of this approach in a practical manner, and it allows us to develop program logics where “resources” (as above) become resources in separation logic.
Compared to other programming languages paradigms and effects, type systems and logical relations for delimited continuations have not been studied as comprehensively. The original type system for shift/reset is due to Danvy and Filinski [10], where they employ answer-type modification. Materzok and Biernacki [22] generalized this type system to account for more involved control operators shift\(_{0}\)/reset\(_0\); an alternative substructural type system for these operators was designed by Kiselyov and Shan [17]. Dyvbig, Peyton Jones, and Sabry [11] provide a typed monadic account of CPS for delimited continuations with dynamic prompt generation. Asai and Kameyama [2] present a polymorphic variant of the Danvy and Filinski’s type system.
Biernacka and Biernacki [5] prove termination for a language with
and
(but without recursion) using logical relations based on abstract machine semantics. The shape of their logical relation is similar to our logical relation used for showing adequacy in that they also have relations for configurations, metacontinuations, etc. Asai [1] uses type-directed logical relations to verify a direct-style specializer (partial evaluator) for a language with
and
, proving correctness against evaluation-context based operational semantics. In contrast with those works, we define our logical relations on denotations, using the semantics of GITrees and the derived program logics.
In our interoperability example we showed type safety of a combined language, with respect to denotational semantics. In future work we would like to examine other properties: for example, that \(\lambda _{\textsf{delim}}\) expressions cannot disrupt \(\lambda _{\textsf{embed}}\)’s control flow, perhaps establishing some form of well-bracketedness as in [29].
We would also like to study other context-dependent effects like exceptions, handlers, and algebraic effects [3, 4, 24, 31, 33]. In particular, it would be interesting to give a denotational semantics to a language with handlers, derive program logic rules for it, and compare the resulting program logic to the one in [32].
Acknowledgments
This work was co-funded by the European Union (ERC, CHORDS, 101096090). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them. This work was supported in part by a Villum Investigator grant (no.25804), Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.
Data-Availability Statement
The formalisation associated with this paper, which covers all the main results, is available online [27].
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.