Computation First: Rebuilding Constructivism with Effects

The Axiom of Choice (AC), in one of its many formulations, states that every total relation has a corresponding function exhibiting that relation.

While originating from set theory, AC also has various formulations in constructive theories. Whereas the intensional formulation of AC is trivially modelled by many constructive type theories through the standard interpretations of the quantifiers, the extensional formulation is essentially inconsistent with them. This is because the extensional AC implies the (non-constructive) Law of Excluded Middle (LEM) [26]. This is but one of many famous unexpected consequences of (extensional) AC. So while constructive theories cannot implement the full (extensional) AC, one can constructively approach AC. That is, we can provide computational models of variants of the axiom that are equivalent to AC only in the presence of LEM.

One important such variant is that of Countable Choice (CC), in which one restricts attention to relations over, say, the natural numbers (taking $A:=\mathbb{N})$. CC is a fundamental principle in constructive real analysis as it is used to unify the different formalizations of the reals. Cauchy reals (of converging sequences of rational numbers) are not, in fact, Cauchy complete in constructive real analysis. The Dedekind reals are, but there is no way to convert a Dedekind real to a Cauchy real [54]: while for any given degree of precision one can demonstrate that there exists a rational number that approximates the Dedekind real up to that precision, there is no way to construct an infinite sequence of increasingly precise approximations. For this, one needs to use CC.¹¹1In fact, weak CC, in which choice is possible if there is at most one choice to be made across all the countable inputs, is sufficient.

Now, CC is generally accepted as constructively valid as it holds true in traditional realizability models (stemming from PCAs). But this fact relies on the determinacy of the internal computational system, and, in fact, the proof fails in the presence of non-determinism because the realizer for the totality of the relation no longer necessarily behaves like a deterministic function. Nonetheless, the addition of stateful computation can then restore CC [12]. The introduction of mutable (monotonic) shared state allows for the memoization of the non-deterministic realizer, thereby ensuring that repeated queries for the same input would produce the same output. This memoization process is enabled due to the fact that for the natural numbers one can compare a given input with prior inputs for equivalence, a property which does not hold for more general types.

There are a number of systems implementing notions of choice for various classical settings, e.g., [40, 57, 7, 10]. Interestingly, despite the difference in goals, these systems use techniques like coinduction, lazy evaluation, and infinite terms in a manner similar to memoization, suggesting that it is, somehow, a more robust interpretation of CC. Whereas in the constructive setting the challenges lie in dealing with impredicativity and non-determinism, in all these systems the challenge lies in being compatible with the complex control constructs used to give constructive interpretations of classical logic [25, 3, 59]. In particular, [40] shows that a mixed-strength existential quantifier can simultaneously be compatible with classical logic while also providing a constructive interpretation of weak Dependent (and Countable) Choice. [57] refines this work and proves strong normalization (and therefore also soundness) of a sequent-style variant of [40]’s logic dPA^ω. [7] implement a negative translation of AC by using a bar-recursion-like operator.

Beyond CC, Dependent Choice (DC), which allows for the construction of sequences where each element depends on the previous one, can also be realized using state.

As noted, Herbelin developed a calculus, dPA^ω, in which constructive proofs of CC and DC can be derived via the memoization of choice functions (in a way that would be impossible in a stateless model [58]). The specifics of such computational interpretations have meaningful practical implications for constructive systems. To see why, consider again the example of the reals. Both Countable and Dependent Choice can be implemented using mutable state and are sufficient for constructing the infinite sequences needed for Cauchy reals to be Cauchy-complete (so, logically, one could choose either one); however, they have different implementation characteristics. The implementation of CC uses an (infinite) array to “remember” non-unique choices as they are made on demand. Each entry in the array is computed independently, resulting in a significant amount of redundant computation and requiring a less efficient choice policy to ensure that the sequence converges. With DC, each entry in the array is computed using the value of the previous entry, avoiding this redundancy and permitting a much more efficient choice policy (e.g. choose something at least twice as precise as the previous entry). In fact, [47] uses a stronger (effectfully computable) principle of non-deterministic DC to mechanically verify and extract efficient computations approximating real numbers up to arbitrary precision.

Classical logic, characterized by principles such as the Law of Excluded Middle (LEM) and Pierce’s Law, has traditionally been considered incompatible with constructivism due to its reliance on non-constructive proof techniques. However, a rich line of research has demonstrated that classical logic can, in fact, be constructively interpreted by introducing continuations, a concept originating from programming languages, and the control operator call/cc (call with current continuation) [38, 25, 3, 59]. Roughly speaking, a continuation is a higher-order function that represents the “rest of the computation” at any given point, effectively capturing the control state of the program. When a continuation is captured (e.g., using call/cc), it can be stored, passed around, or invoked multiple times, providing direct control over the execution flow in a manner typically outside the scope of pure functional computation. This mechanism is extremely powerful because it allows for non-local exits from a computation, essentially allowing for the representations of many other effects [32].

The idea of using call/cc to interpret classical logic was developed into a robust and highly influential framework by Krivine [52], known as classical or Krivine realizability. Krivine’s framework is based on the ${\lambda }_c$-calculus, an extension of the $\lambda$-calculus with a $\mathrm{𝚌𝚊𝚕𝚕}/\mathrm{𝚌𝚌}$ instruction that enables the manipulation of control flow. The Curry–Howard correspondence directly relates $\mathrm{𝚌𝚊𝚕𝚕}/\mathrm{𝚌𝚌}$ to Peirce’s law, effectively transforming the computational model into a setting where classical logic can be directly realized. This ability of control operators like call/cc to dynamically explore and resolve cases is the computational essence of classical reasoning.

The original presentation of Krivine’s realizability uses control operators in a direct-style fashion in which $\mathrm{𝚌𝚊𝚕𝚕}/\mathrm{𝚌𝚌}$ instructions can be compiled to the pure $\lambda$-calculus using a continuation-passing style (CPS) translation. Later, Oliva and Streicher demonstrated that Krivine realizability can be obtained by combining a standard intuitionistic realizability interpretation with a CPS translation [63, 56, 35]. Beyond $\mathrm{𝚌𝚊𝚕𝚕}/\mathrm{𝚌𝚌}$, Krivine further expanded his framework by introducing the quote instruction, which computes a natural number associated with the code of a program in a way that allows comparing programs based on their codes [51]. This can be seen as enabling the dynamic generation of choices based on the evolving state of computation, which, in turn, permits the constructive interpretation of principles like DC, where the evolving state of computation can influence the generation of choices.

Markov’s Principle (MP) is a central principle in (Russian) constructive mathematics nowadays most commonly stated as follows:

Essentially, it states that ${\mathrm{\Sigma }}_1^0$ propositions, i.e. existential quantifications over decidable predicates, are stable under double negation [24, 68, 27].

In Krivine realizability, where control operators such as call/cc are available, MP can be realized constructively. Indeed, since continuations provide a form of non-linear control flow, they allow the system to search for an element without requiring a fully constructive witness. Alternatively, Pédrot used exceptions to realize MP within the Calculus of Inductive Constructions (CIC) [65]. Concretely, by extending the type theory with a form of statically-bound exception mechanism, one can extract an existential witness from a proof of its double negation [39].

The subtle additional structure offered by effectful computation opens another critical avenue for constructivism by allowing for differentiating variants of constructive principles. Many key principles, such as MP, have various formalizations that are classically equivalent, but not necessarily in constructive foundations. However, while this is well-known, it is often overlooked, leading to false claims in the constructive discourse. For example, the various non-constructively-equivalent definitions of decidable predicates lead to non-equivalent MPs, resulting in mistakes about the status of MP, e.g., in [65]. A recent work [14] clarified the status of three MP variants: ${\mathrm{𝖬𝖯}}_{\mathbb{P}}$ (for propositional decidability), ${\mathrm{𝖬𝖯}}_{𝔹}$ (for Boolean decidability), and ${\mathrm{𝖬𝖯}}_{\mathbb{P}ℝ}$ (for primitive recursive functions). The separation of the variants, in the spirit of [24, 68], was done using ${\mathrm{𝖳𝖳}}_C^{\mathrm{\square }}$ [18, 20], a generic family of effectful, extensional type theories with a forcing interpretation parameterized by modalities.

The separation of the MP variants is achieved by instantiating the choice operator $C$, primarily using choice sequences of Booleans or propositions (building on ideas going back to [49, 48, 76]). For example, to refute ${\mathrm{𝖬𝖯}}_{𝔹}$, the authors construct a model based on sequences of Boolean choices. In this model, a statement like $\neg \neg \exists n.f(n)=\mathrm{𝗍𝗋𝗎𝖾}$ can hold, since it is always possible to make the choice “true” eventually, while $\exists n.f(n)=\mathrm{𝗍𝗋𝗎𝖾}$ does not hold because one can construct a path where “true” is never chosen. Similarly, using propositional choices allows for the falsification of ${\mathrm{𝖬𝖯}}_{\mathbb{P}}$. Crucially, using the ${\mathrm{𝖳𝖳}}_C^{\mathrm{\square }}$ framework one can show that in these same models, variants for effect-free functions or functions with limited effects do hold. This distinction reveals how effect-free or limited-effect computations maintain consistent behavior across different possible future worlds (states of choice sequences), unlike general effectful computations.

Continuity is a fundamental concept in constructive mathematics, traditionally defined as the property that a function from ${\mathbb{N}}^{\mathbb{N}}\to \mathbb{N}$ requires only a finite prefix of the input to determine its output.

Continuity is typically justified through semantic arguments (often forcing-based), where functions are shown to respect this finite-dependence property in a model, e.g., [22, 23, 30, 81, 73, 5]. However, recent advancements have demonstrated that continuity can be directly internalized within constructive type theory through the use of various computational effects [19, 13].

One of the most direct methods for realizing continuity within type theory is through the use of stateful computations, particularly by leveraging reference cells. In this framework, continuity is not an external property but a constructively enforced behavior: as a function is evaluated, the type theory dynamically tracks the length of the input segment necessary to determine the output. Specifically, a reference cell is used to maintain a record of the smallest initial segment of the input sequence that has been read so far. This mechanism allows the system to efficiently compute the modulus of continuity of a function. Functions defined in this manner are constructively continuous by design, and their modulus of continuity is an internal component of their evaluation [19].

An alternative method of realizing continuity is achieved using inductive dialogue trees. In this approach, the continuity of a function is represented by the structure of a dynamically generated tree, where the paths of the tree encode information about how much input (an initial segment of a sequence in the Baire space) is needed to determine the output, and the leaves contain the computed values [13]. These dialogue trees are dynamic and evolve based on the function’s interactions with its input, providing a general and flexible model for continuity. At each step, the tree structure captures the minimal interaction necessary for the function to produce a value.

The significance of these computational methods lies in their ability to directly enforce and witness continuity within the type theory itself. Rather than appealing to external semantic models, these systems constructively guarantee continuity through their internal effectful mechanisms. This means that the modulus of continuity (the $m$) is not merely a logical construct but an actively computed value, directly linked to the computational structure of the function. Moreover, the methods are efficient, as they avoid redundant recomputation by dynamically tracking input dependencies.

Paul Cohen’s method of forcing is traditionally used to construct models of set theory where specific statements hold or fail. Forcing constructs new models of set theory by adding “generic” elements, allowing for the exploration of various set-theoretic possibilities. One approach to adapting forcing in constructive settings involves simulating the structure of forcing using monotonic memory, i.e., a memory model where the state can only grow or remain the same over time, never decreasing. Avigad demonstrated that this monotonic accumulation of conditions can simulate the behavior of forcing, thereby constructing models where certain propositions hold [4].

Another use of monotonic memory arises in the context of nonstandard analysis, which introduces infinitesimals and infinite numbers to analysis. In constructive mathematics, Dinis and Miquey have shown how realizability interpretations using monotonic memory can provide a constructive framework for nonstandard principles [28]. By extending the $\lambda$-calculus with a memory cell that contains an integer (the state), they indicate in which slice of the ultrapower the computation is being done. This stateful realizability interpretation mimics the structure of the ultraproduct by allowing formulas to be interpreted as sets of terms with states, where each state corresponds to a slice. The effectful interpretation is then used to provide realizers for nonstandard reasoning principles, for instance, the idealization principle is realized by a program whose computational behavior involves a diagonalization process that increases the value stored in the state/reference.

The notion of parameterized realizability, introduced by Bauer and Hanson in [6], extends traditional pure realizability by building on a notion of computations that has access to external oracles. Using this framework, the authors constructed a topos in which the Dedekind reals are internally countable. The core idea involves using parameterized partial combinatory algebras where the application of a realizer depends on a parameter from a specified set $\mathbb{P}$. In the specific topos that yields countable reals, this parameter set $\mathbb{P}$ consists of oracles representing non-diagonalizable sequences. The realizers themselves are partial maps that are computable relative to these oracles. Thus, the dependence of computation on an external parameter or oracle allows the chosen non-diagonalizable sequence to serve as an internal enumeration of the reals within the constructed topos.

Computational reflection is another powerful effect used to internalize logical principles. Pédrot has explored the relationship between Church’s Thesis (CT) and dependent type theory, particularly Martin-Löf Type Theory (MLTT) [66]. For this, MLTT was extended with quote primitives that relate to execution step counts and validating computation traces, essentially internalizing the runtime behavior of programs within the system. Using this, MLTT can internally realize CT because the new terms yield that for every function, there exists a code, and for every input to that function, there exists a step count and a proof that running the code for that many steps yields the correct result.

Realizability originated from Kleene’s interpretation of intuitionistic number theory in the 1940s [46] and has since developed into a large body of work in logic and theoretical computer science where it is used both as a model-theoretic tool and as a method for extracting computational insight. The key idea of realizability is to replace the standard Traskian truth values interpretation of formulas with an interpretation that assigns a set of computational elements called realizers (or evidence) to each formula, with the intuition that the formula dictates the computational behavior of these realizers. In essence, realizability consists of three components: formulas (or types) in some logical framework (e.g., HOL or ZF), a computational system such as the $\lambda$-calculus or some combinators algebra, and an interpretation of formulas that connects the former two elements by providing a “truth value” assignment to formulas based on the elements in the computational system. Thus, a realizability model specifies what it means for a proposition to be “realized” or made true by computational objects, and the salient feature of realizability is that these realizers are always computable and that truth values are saturated w.r.t. computational evaluation.

In the original Kleene’s realizability, the realizers are natural numbers, and a number $r$ realizes a formula $\phi$ if $r$ can be interpreted as a program that computes a witness for $\phi$. The realizability relation $r⊩\phi$ is defined as follows:

• $\mathrm{■}$

  $r⊩(\phi \wedge \psi )$ if $r$ is a pair $(r_1,r_2)$ where $r_1⊩\phi$ and $r_2⊩\psi$.

• $\mathrm{■}$

  $r⊩(\phi \vee \psi )$ if $r$ is a pair $(i,r_1)$, where $i=0$ and $r_1⊩\phi$ or $i=1$ and $r_1⊩\psi$.

• $\mathrm{■}$

  $r⊩(\phi \to \psi )$ if $r$ is a program that, given any realizer $s⊩\phi$, produces a realizer $r\cdot s⊩\psi$.

• $\mathrm{■}$

  $r⊩\forall x.\phi (x)$ if $r$ is a program such that for any $n\in \mathbb{N}$, $r\cdot n⊩\phi (n)$.

• $\mathrm{■}$

  $r⊩\exists x.\phi (x)$ if $r$ is a pair $(n,r_1)$ where $n\in \mathbb{N}$ and $r_1⊩\phi (n)$.

In this realizability model, logical connectives are interpreted in terms of computational processes: conjunction is realized by a pair of realizers for each conjunct, disjunction is realized by a pair where the first element indicates which disjunct is true, implication is realized by a function that transforms realizers, universal quantification is realized by a program that produces realizers for each instance, and existential quantification is realized by a pair of a witness and a realizer that the witness satisfies the formula.

But while Kleene’s original realizability was based on arithmetical realizers, the modern realizability models rely on a computational system of a Partial Combinatory Algebra (PCA) [31, 41, 78, 34]. PCAs offer an algebraic model for the untyped $\lambda$-calculus, thereby providing an abstract interface that ensures computability (i.e., Turing completeness) without committing to the details of any specific programming language. Concretely, given a set of codes $𝔸$, a PCA is defined via a (partial) application function $\cdot :𝔸\times 𝔸\rightharpoonup 𝔸$ satisfying some completeness conditions that ensure they can support general computation, i.e., be at least as computationally powerful as the $\lambda$-calculus(often formalized via the definability of the $S$ and $K$ combinators). From a PCA one can obtain a realizability tripos (i.e., a model of HOL, or more generally a higher-order fibration over a cartesian-closed category) by modeling predicates as indexed subsets of codes (i.e. a predicate on a set $I$ specifies for each element $i\in I$ which codes (if any) “realize” that the predicate holds for $i$) and defining entailment between two predicates to hold whenever there is a uniform code that, for any index, can convert any realizer of the input predicate into a realizer of the output predicate. In turn, via the tripos-to-topos construction [72], from a realizability tripos one can construct a realizability topos, which form the general realizability model of a highly expressive (extensional, impredicative) dependent type theory (and set theory) [43].

However, PCAs are themselves limited in their computational capabilities. In particular, the only computational effect they support internally is non-termination through the partiality of the application. PCAs do offer ways in which various effects can be modeled indirectly, usually by incorporating additional structures or operations into the underlying algebraic framework. Notable examples include PCAs with errors, choice, exceptions, and parameters, e.g.,  [12, 17, 6]. However, the ability to uniformly and internally support a wide range of computational effects within the algebraic structure is crucial for the development of robust and expressive constructive theories and for reasoning about them collectively.

An immediate manner in which to enrich realizability models with effects is simply to generalize the PCA structure in a way that allows capturing arbitrary effects. For this, the notion of Monadic Combinatory Algebras (MCAs) was introduced, generalizing PCAs but encapsulating a broader spectrum of computational effects by being constructed over some underlying monad [15]. Monads are a common categorical device for analyzing computational effects in the study of programming languages [60, 79]. Concretely, monads are a special kind of functors that allow the composition of Kleisli morphisms, i.e., morphisms where the target is an object in the image of the functor. Using monads, a procedure that takes a value of type $A$ to a value of type $B$, while possibly invoking some computational effect, can be modeled by a morphism from $A$ to $MB$, where $M$ is some monad that embodies the effect.

Given a (Set) monad $M$, a Monadic Combinatory Algebra (MCA) over $M$ is a set of “codes” $𝔸$ with an application Kleisli function: $(-)\cdot (-):𝔸\times 𝔸\to M𝔸$ satisfying some completeness conditions. The key to MCAs lies in that whereas the PCA application function can only return a code (if anything at all), the MCA application Kleisli function returns a computation, and so it can produce any computational effect describable by a monad. Indeed, PCA is a special case of an MCA by instantiating the monad with the subsingleton monad, $M𝔸={𝒫}_1(𝔸)$, i.e. $M𝔸$ is the set of subsets of $𝔸$ in which all elements are equal.

Leveraging the monadic structure enables MCAs to internalize various computational effects. For example, non-deterministic computation corresponds to an MCA with $M$ being the powerset monad, $M𝔸=𝒫\left(A\right)$, which considers the subset of possible results. Stateful computation corresponds to an MCA with $M$ being the powerset state monad, $M𝔸=\mathrm{\Sigma }\to 𝒫\left(\mathrm{\Sigma }\times 𝔸\right)$, which takes a code in a given state and returns a set of all possible pairs of results in new states. CPS continuations correspond to a monad that represents a computation with direct access to the call stack, allowing the manipulation of the control flow of the programs in non-trivial ways $M𝔸=\left(𝔸\to R\right)\to R$. Other, more “logical” effects, such as parametric realizability wherein computation has access to an external oracle [6], can be captured via the subsingleton reader monad, $M𝔸=\mathbb{P}\to {𝒫}_1(𝔸)$, where $\mathbb{P}$ is a set of some external parameters.

However, while the generalization to MCAs smoothly internalizes effects into the algebra, it also introduces a complexity in the standard pipeline for generating realizability models. This is because, to define a tripos from an MCA one has to define entailment. In traditional realizability, evidence of entailment between two formulas, $\phi ⊢\psi$, is some code $e$ that, when applied to any realizer of $\phi$ produces a realizer for $\psi$. That is, by brutal abuse of notation: $\forall c_a.c_a⊩\phi \Rightarrow e\cdot c_a⊩\psi$. This is well-defined in traditional realizability since when an application is defined, it is deterministic, but this is no longer the case in MCA-based realizability. Thus, for an arbitrary monad $M$, $e\cdot c_a\in M𝔸$ and it is unclear how to relate it to $\psi$ because $e\cdot c_a$ is now a computation and realizability is defined for codes, not computations. Thus, one needs to provide an additional structure that converts formulas on codes $𝔸$ to formulas on computation $M𝔸$ in a way that respects the monad’s structure. This is given by the notion of a $M$-modality, which intuitively describes a post-condition over the result of a (possibly effectful) computation. Roughly speaking, an $M$-modality $\diamond$ is a natural transformation that takes predicates on a set $X$ (defined by functions from $X$ to some Heyting prealgebras $\mathrm{\Omega }$) and extends them to a function in $M(X)\to \mathrm{\Omega }$, intuitively thought of as predicates on $M(X)$. Using the modality we can write $⟨\diamond x\leftarrow m\diamond ⟩\varphi \left(x\right)$ stating that after the computation $m$ yields a value $x$ (in case it does), then $\varphi \left(x\right)$ holds. To obtain a sound logical framework, an $M$-modality has to satisfy certain properties to ensure it is well-behaved with respect to the computational operators of the monad and the logical operators of the underlying complete Heyting prealgebra. For example, ensuring that properties held before a computation continue to hold afterwards.

As shown in [15], from a “monadic core”, which essentially combines a monad with a non-trivial modality, one can construct a realizability tripos by defining entailment between two predicates $\phi ⊢\psi$ whenever there is a uniform code $e$ (in some combinatory complete subset of the codes) that for every realizer $c$ for $\phi$, the result of the possibly effectful computation $e\cdot c$ realizes $\psi$, that is, $⟨\diamond r\leftarrow e\cdot c\diamond ⟩\psi \left(r\right)$ holds. This shows that the generalized computational system of an MCA still allows for the standard pipeline construction of realizability models while accommodating a wider range of computational effects.

Despite the extensive discourse on realizability, even in its traditional setting, the literature does not offer a universally agreed-upon definition of the general notion of realizability structures. This absence leaves open the question of what exactly constitutes a realizability framework in the most general sense. This section reviews a general and highly abstract structure that pinpoints the common structure of realizability interpretations called Evidenced Frames. Evidenced frames aim to capture the common structural elements of realizability without being restricted to a specific algebraic or computational model. They offer a minimal realizability framework that is flexible enough to allow for internalization of computational effects, even beyond monadic ones [17]. Rather than being a complete framework, an evidenced frame can be understood as a minimal specification that various realizability structures can instantiate, providing a unifying perspective on the relationship between propositions, computation, and logical validity.

Roughly speaking, an evidenced frame is a triple $(\mathrm{\Phi },E,{\varphi }_1\stackrel{𝑒}{\to }{\varphi }_2)$ that captures precisely the three key components of realizability: $\mathrm{\Phi }$ is a set of of propositions, $E$ is a set of evidence, and ${\varphi }_1\stackrel{𝑒}{\to }{\varphi }_2$ is an (evidence) relation. To form an evidenced frame, these three components need to satisfy the requirements described in Fig. 1, guaranteeing the existence of basic computational and logical constructs.

While the standard pipeline toward realizability models traditionally stems from a PCA, there is a uniform construction generating a realizability tripos from any given evidenced frame. Moreover, evidenced frames are complete with respect to Set-based triposes. One way to look at this is that realizability triposes are evidenced frames that have forgotten their evidence. Given the fact that a PCA is a simple instance of an evidenced frame, evidenced frames provide an alternative, powerful and flexible foundation for realizability theory. What is more, evidenced frames can uniformly encompass a broad spectrum of computational effects since their level of abstraction generalizes beyond the specific details of any particular model of computation. That is, the evidence can be any computational entities, functions, stateful computations, or non-deterministic procedures, depending on the computational model under consideration.

In particular, the simple and unified nature of evidenced frames makes them a powerful tool for systematic exploration of general metatheorems that link computational capabilities and logical principles. For instance, one can ask, following the examples discussed in Sec. 2.1, whether all realizability structures that support memoization also validate CC. This question becomes concrete within the framework of evidenced frames, where one can identify the minimal set of properties required to support memoization and investigate whether they universally satisfy CC in the resulting tripos. Similarly, evidenced frames provide a natural setting for comparing different methods that validate CC across various computational settings. By examining whether all known approaches, despite their technical differences, can be uniformly captured by an evidenced frame structure, one can uncover a deeper structural connection between them. This connects to the notion of “robust validity”, where one aims to show that a logical principle holds across a wide range of computational models that preserve a specific computational structure. Evidenced frames make this notion precise, allowing one to rigorously identify the conditions under which a principle like CC is robustly valid.

The syntactic approach to realizability, pioneered by Gödel [37] and further developed in Kreisel’s modified realizability [50], abstracts away many of the complex semantic machinery otherwise required for constructing realizability models for rich languages. By restricting to the syntax and abstracting away the details of any particular semantic structure, it allows for a broader spectrum of possible interpretations, each yielding its own realizability interpretation by virtue of being a model of the target language, without having to tailor the realizability construction to some particular structure. Roughly speaking, the syntactic approach is based on handling realizability as a syntactic translation of logical propositions, i.e., statements about mathematical structures, into program specifications, i.e., statements about computational behavior, in a target program logic describing what it means to realize the input formula. This can be seen as an internalization of the notion of realizability of the source language into the target language. Recent works adopting the syntactic approach include, e.g., [77, 53, 33, 8]. However, here again, works on syntactic realizability focus on the traditional notion of realizability, which does not offer support for computational effects.

To develop a framework for syntactic effectful realizability one can consider a target language that supports effectful programs as realizers for a higher-order source language. Effectful Higher-Order Logic ($\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$) provides a concrete, syntactic framework for effectful realizability, where propositions in higher-order logic (HOL) are translated into an effectful target language [16]. Within $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$, propositions can be interpreted as specifications for effectful programs, and realizers can be typed computational entities capable of interacting with various effects.

To provide internal support for standard programming language features, $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$ combines components of three languages: Higher-Order Logic to model higher-order structure, Girard’s System $F_{\omega }$ [36] to model higher-kinded polymorphism, and Evaluation Logic [71] to model computational types and modalities. The computational term language enables reasoning about effectful programs, where here too, as is the case for MCAs, the effectful aspect of the language is captured through monads. This provides a uniform language parameterized intuitively by a monad that carries the computational behavior of the language. Concretely, the type system explicitly includes a type $M(\tau )$ denoting computations of type $\tau$. To describe specifications of effectful programs, $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$ features a modality $⟨\diamond x\leftarrow p\diamond ⟩\phi$, which intuitively states that property $\phi$ holds when $x$ is the result of running the program $p$. This modality, just like in MCAs, is the core source of effectful computations within $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$. The higher-kinded polymorphic type system allows for typed realizers of higher-order propositions.

The syntax of $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$ is divided into six distinct components, reflecting its dual nature of handling both computation (programs) and logic (specifications). On the computational side, kinds and types are used to provide the types of realizers associated with typed programs. On the logical side, indices, expressions and specifications hold the logical counterpart of the realizability interpretation by describing the properties of these programs. This clear division between computational and logical components allows $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$ to maintain a robust, expressive syntax that can seamlessly integrate rich computational effects within a logically sound framework.

The syntactic realizability translation of $\mathrm{𝗛𝗢𝗟}$ to $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$ yields a realizability model of $\mathrm{𝗛𝗢𝗟}$ from any instance of $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$ for a concrete choice of underlying monad (and an evaluation strategy). Since our target language includes typed realizers, the realizability translation will assign to an $\mathrm{𝗛𝗢𝗟}$ proposition the type of its realizers in $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$, along with a specification describing which programs of the corresponding type are realizers of that proposition. The soundness of this translation implies that there is an algorithm that converts any provable $\mathrm{𝗛𝗢𝗟}$ sequent to an $\mathrm{𝗘𝗳𝗳𝗛𝗢𝗟}$ proof of its translation, which, in turn, contains a computable realizer. These extracted realizers are effectful programs, allowing for the synthesis of such programs from proofs of propositions potentially unprovable in pure $\mathrm{𝗛𝗢𝗟}$.