ABSTRACT. We introduce an illfounded sequent calculus for the constructive µ-calculus, the logic constructed by adding least and greatest fixed points to constructive modal logic. In addition to providing the Kripke-style and game semantics from the literature, we adapt a recent cut elimination argument by Curzi and Leigh, and based on Tait's and Girard's reducibility candidates for this logic. With this, we contribute to a general cut elimination procedure for illfounded proof systems by showcasing this proof method on a logic with modalities and without interdefinability between its connectives.

ABSTRACT. The modal μ-calculus μML is the logic obtained by adding least and greatest fixed point quantifiers to modal logic. It subsumes many temporal and dynamic logics such as PDL, LTL, CTL and CTL*. It is a classical logic, but intuitionistic variants have recently been proposed. In this talk, we present an ongoing project on formalising a variant of the modal μ-calculus inside Agda, a proof assistant based on dependent type theory. We use the machinery of indexed containers to handle the fixed points. The result is a proof-relevant, constructive Kripke semantics, where the semantics of a formula P assigns to a world w a "type of witnesses" that P holds at w. Currently, we have a semantics for the strictly positive fragment of μML (i.e., the fragment without negation and implication); adding implication is still a work in progress, but we believe this can be accomplished using the Cartesian closed structure of the category of containers. The next step is to develop a proof theory for this semantics.

ABSTRACT. PDL is a modal logic where modalities are indexed by programs which come equipped with operations, namely the * operation, which iterates a program an infinite number of times. We explore an intuitionistic variant of PDL and propose a cut-free proof system making use of non-wellfounded proofs.

ABSTRACT. We introduce the semantically-defined constructive logics with master modality CK* and WK*, extending the basic constructive modal logic CK and the Wijesekera-style logic WK obtained by imposing infallibility. Using translations between our logics and fragments of PDL, we show that both CK* and WK* are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celani, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed CS4 and WS4 into the master-modality logics, showing that their validity problems are in EXPTIME.

ABSTRACT. MetaML-style metaprogramming languages allow programmers to construct, manipulate and run code. In the presence of higher-order references for code, ensuring type safety is challenging, as free variables can escape their binders. In this paper, we present Contextual Modal MetaML, \textit{the first metaprogramming language that supports storing and running open code under a strong type safety guarantee}. The type system utilises contextual modal types to track and reason about free variables in code explicitly. A crucial concern in metaprogramming-based program optimisations is whether the optimised program preserves the meaning of the original program. Addressing this question requires a notion of program equivalence and techniques to reason about it. In this paper, we provide a semantic model that captures contextual equivalence for Contextual MetaML, establishing \textit{the first full abstraction result for an imperative MetaML-style language}. Our model is based on traces derived via operational game semantics, where the meaning of a program is modelled by its possible interactions with the environment. Modal types can be introduced as box names and queried by running.

ABSTRACT. \section*{Background on Effectful Contextual Modal Type Theory} In 2021, N. Zyuzin and A. Nanevski proposed a calculus for the theory of algebraic effects, where effectful signature is treated as a \emph{variable context}, and effects are tracked via \emph{indexed modalities} inherited from Contextual Modal Type Theory (CMTT). In the resulting calculus, named ECMTT (Effectful Contextual Modal Type Theory), effect information is encoded in the \emph{modal type} $\boxt{\Psi}{A}$, classifying computations of type $A$ that may invoke exactly the operations declared in the algebraic theory $\Psi$. \paragraph{On Contextual Modal Type Theory.} CMTT is a contextual variant of constructive modal S4. Its typing judgments are of the form $\Delta;\Gamma \vdash e : A$, where $\Gamma$ holds ordinary \emph{value variables} $x:A$ (intuitively, making the assumption that $A$ is \emph{contingently} true at the given world) and $\Delta$ holds \emph{modal variables} $u \mathrel{::} A[\Psi]$, annotated with a context $\Psi$ of variables saying that $A$ is \emph{valid relative to} $\Psi$ (i.e.,~true in every world in which every $B$ in $\Psi$ is true). Two of the main rules of CMTT are the following. \begin{center} \AXC{$\Delta; \Psi \vdash e: A$} \LL{$\Box I$} \UIC{$\Delta;\Gamma \vdash \mathrm{box }\ \Psi.e: [\Psi]A$} \DP \quad \AXC{$\Delta;\Gamma \vdash e_1: [\Psi] A$} \AXC{$\Delta, u::A[\Psi]; \Gamma \vdash e_2: B$} \RL{$\Box E$} \BIC{$\Delta; \Gamma \vdash \mathrm{let\ box} \ u = e_1\ \mathrm{in}\ e_2: B$} \DP \end{center} The \emph{introduction form} $\boxe{\Psi}{e}$ binds all variables of $\Psi$ in the scope of $e$, simultaneously removing the outside context $\Gamma$ from $e$'s premise (reading the rule $\square I$ from the bottom up). The \emph{elimination form} $\mathbf{let}\;\mathbf{box}\;u = e_1\;\mathbf{in}\;e_2$ (rule $\square E$) binds the unboxed body of $e_1$ to the modal variable $u$; occurrences of $u$ in $e_2$ must be guarded by \emph{explicit substitutions} $u\langle\sigma\rangle$ that supply definitions for the variables in $\Psi$. ECMTT adopts and readapts the aforementioned concepts: contexts $\Psi$ become algebraic theories and explicit substitutions become effect handlers. \paragraph{Accomodating algebraic effects.} Consider, as an example, the operation $get$ that reads the current state and the operation $set$ that updates it. An algebraic theory, e.g.\ the state theory \[St \triangleq \mathit{get} \div \mathit{unit} \Rightarrow \mathit{int},\; \mathit{set} \div \mathit{int} \Rightarrow \mathit{unit},\] is treated as a variable context locally bound by the $\mathbf{box}$ constructor. The term \[\mathit{incr} \triangleq \boxe{St}{x \leftarrow \mathit{get}();\; \_ \leftarrow \mathit{set}(x+1);\; \mathbf{ret}\;x}\] has type $\boxt{St}{\mathit{int}}$, and the boxed term is a pure (i.e.~not effectful) expression. As mentioned above, context reachability in CMTT is witnessed by \emph{explicit substitutions}; in ECMTT it is witnessed by \emph{effect handlers}. Consider the following \[handlerSt \triangleq (get(x,k,z) \rightarrow \mathrm{cont}\ k\ z\ z,\ set(x,k,z) \rightarrow \mathrm{cont}\ k\ ()\ x,\ return(x,z) \rightarrow \textbf{ret}(x,y)).\] A handler such as $\mathit{handlerSt}$ specifies how each operation of $St$ is interpreted, thereby transforming a computation in theory $St$ into one in the empty theory. %The handler is used through the elimination form %$\mathbf{let}\;\mathbf{box}\;u = \mathit{incr}\;\mathbf{in}\;\mathbf{handle}\;u\;\mathit{handlerSt}\;0$, %which binds $u$ to the unboxed body of $\mathit{incr}$ and runs it under the handler with initial %state~$0$. \iffalse The operational semantics of ECMTT is determined solely by $\beta$-reduction (plus $\eta$-expansion for local completeness), in direct analogy with other logic-based calculi. This is in sharp contrast to monad-based designs, where the bound computation executes eagerly. The paper also situates ECMTT as a first step towards a Curry--Howard correspondence for algebraic effects and modal logic, anticipating transfers of results (Kripke semantics, normalisation by evaluation, dependent types, etc.) between the two fields. \fi ECMTT uses four variable judgments ($x:A$, $u::A[\Psi]$, operations $\mathrm{op}\div A\Rightarrow B$, continuation variables $k\sim\!\!\!:\,A\stackrel{S}{\Rightarrow}B$) and five term judgments (expressions, computations, statements, handlers, handling sequences). By design, the operational semantics of ECMTT is determined solely by $\beta$-reduction, as customary in other logic-based calculi (but not in other systems for algebraic effects). The new syntactic category of (effectful) \emph{computations} sequences bindings of algebraic operations and continuation calls in monadic-style notation $x \leftarrow s;\;c$, and terminates with $\mathbf{ret}\;e$. The category of \emph{expressions} remains purely functional. In contrast with the CMTT setting, the modal type $\boxt{\Psi}{A}$ now classifies computations, not expressions. The context $\Gamma$ (formerly holding value variables) now holds \emph{algebraic operations} $\mathit{op} \div A \Rightarrow B$ and \emph{continuation variables} $k \sim\!\!\!:\, A \stackrel{S}{\Rightarrow} B$. The context $\Psi$ (used in $\boxt{\Psi}{A}$) ranges only over operation-only subsets (algebraic theories). Value variables $x:A$ migrate to $\Delta$, reflecting the fact that values are computations in the empty theory. This allows values to survive boxing, enabling parametric computations such as $\mathit{incr}_n \triangleq \lambda n:\mathit{int}.\;\boxe{St}{x \leftarrow \mathit{get}();\;y \leftarrow \mathit{set}(x+n);\;\mathbf{ret}\;x}$. \section*{In search for a logical interpretation of Algebraic Effects} In the case of the constructive modal logic S4, we already have a relational Kripke-style, algebraic, and categorical semantics; all of these are well-known and have been successfully used to study the metaproperties of the logic for which they are complete. At present, however, there is no known semantic characterization of the logic defined by the ECMTT calculus, nor is there a known Hilbert-style axiomatization of it. Our task is to find such a characterization to identify for the first time a correspondence, in the style of Curry-Howard, targeting algebraic effects.\footnote{As far as the authors are aware, this would count as the first instance of a Curry-Howard-style correspondence where the computational system is developed before its logical interpretation.} The following is a list of relevant, non-interderivable theorems of ECMTT, which currently constitute an initial attempt at axiomatization within a Hilbert-style proof system. \begin{enumerate} \item \label{item1} $\vdash [\Psi]A \wedge [\Psi]B \rightarrow [\Psi](A \wedge B)$, for every $\Psi$; \item \label{item2} $\vdash A \rightarrow [\Psi]A$, for every $\Psi$; \item \label{item3} $\vdash [\Psi][\Psi]A \rightarrow [\Psi]A$, for every $\Psi$; \item \label{item4} $\vdash [\Psi]A \rightarrow [\Psi']A$, given $\Psi \subseteq \Psi'$; \item \label{item5} $\vdash A \rightarrow [\Psi]B$, whenever $\mathrm{op}\div A\Rightarrow B$ is in $\Psi$; \item \label{item6} $\vdash [\Psi]C \rightarrow((A_1\rightarrow B_1) \rightarrow\cdots\rightarrow(A_n \rightarrow B_n) \rightarrow \Box C)$, where $\Psi = \{\mathrm{op}_i\div A_i \Rightarrow B_i\}_{i=1}^{n}$. \end{enumerate} The first three theorems listed above correspond exactly to a multimodal version of propositional Lax logic. It is known that multimodal propositional Lax logic is sound and complete with respect to multirelational CL-Kripke models. The latter are defined as a tuple $(W, \leq, V, \{R_\Psi \mid \Psi \text{ is an algebraic signature}\}, \models)$, where $W$ is a non-empty set of possible worlds partially ordered by $\leq$; $V$ is a map which assigns to every propositional variable $p$ an upset $V(p) \subseteq W$; each $R_\Psi$ is a partial order on $W$; finally $\models$ is a relation between worlds and formulae recursively defined as in the intuitionistic case, where \[w \models [\Psi]A \text{ iff forall } w' \geq w \text{ there exists } w'' \text{ such that } w'R_\Psi w'' \text{ and } w'' \models A.\] We also require every $R_\Psi$ to be hereditary, namely if $w \models A$ and $wR_\Psi v$, then $v \models A$. It can be shown that the validity of Theorems \ref{item4}, \ref{item5}, and \ref{item6}, in the context of the multirelational CL-Kripke models defined above, is equivalent to the following conditions imposed on the accessibility relations $R_\Psi$ and the valuation function $V$. \begin{enumerate} \addtocounter{enumi}{3} \item $\vdash R_\Psi \subseteq R_{\Psi'}$, whenever $\Psi \subseteq \Psi'$; \item whenever $\mathrm{op} \div A \Rightarrow B \in \Psi$ and $w \models A$, there exists $v \in W$ such that $wR_\Psi v$ and $v \models B$; \item whenever $w \models [\Psi]C$ and $w \models A_i \rightarrow B_i$ for every $\mathrm{op} \div A_i \Rightarrow B_i \in \Psi$, there exists $v \in W$ such that $wR_\emptyset v$ and $v \models C$. \end{enumerate} Intuitively, Theorem \ref{item4} states that whenever an algebraic signature is contained within another, it is possible to use every operation present in the first one within the second. Theorem \ref{item5}, on the other hand, states that it is possible to perform $\mathrm{op}\div A \Rightarrow B$ (in the context of an appropriate algebraic signature $\Psi$ containing the aforementioned operation) whenever an input of type $A$ is available. Finally, Theorem \ref{item6} captures the concept of operation handling: every $\mathrm{op}\div A \Rightarrow B$ in $\Psi$ is handled via the corresponding function of type $A \rightarrow B$.

ABSTRACT. Modal type systems are a powerful tool for tracking properties in programming languages. They have long been used to track properties of computations, such as mobility, co-effects or erasability. In recent years, several authors have used them to track properties of values, such as stack location, linearity, purity or acyclicity. However, to support the latter applications, one needs to restrict modal type systems appropriately. In this abstract, we identify the value trick as a unifying principle connecting several approaches from the literature.

ABSTRACT. Fitch-style natural deduction for intuitionistic modal logics have found a variety of applications in computer science, notably in the design of modal type systems in programming languages. In this work, we propose a Beth-Kripke-Joyal-style cover semantics à la Goldblatt for Fitch-style modal natural deduction with the overarching motivation of 1) explaining the seemingly ad hoc proof rules in the Fitch-style approach and 2) implementing Normalisation by Evaluation for corresponding modal lambda calculi.

ABSTRACT. What the appropriate intuitionistic analogue of the normal modal logics should be, is question without a simple answer. In the intuitionistic setting, $\Box$ and $\Diamond$ are no longer defined as dual to each other and as a result, it is not so immediate as to what the correct rules for intuitionistic $\Box$ and $\Diamond$ should be. Most commonly, as in~\cite{degroot2025semanticalanalysisintuitionisticmodal,StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics,simpson1994Thesis}, one finds Intuitionisic Modal Logics (IMLs) defined as taking any axiomatisation of IPL and adding the following five axioms and rule of inference: \vspace{-1.2cm} \begin{center} \[ \begin{array}{ccccc} k_1: & \Box(\varphi\to\psi) \to \Box\varphi \to \Box\psi & \qquad & k_3: & \Diamond\bot\to\bot \\ k_2: & \Box(\varphi\to\psi) \to \Diamond\varphi \to \Diamond\psi & \qquad & k_4: & \Diamond(\varphi\lor\psi)\to (\Diamond\varphi\lor\Diamond\psi) \end{array} \] \vspace{-0.5cm} \[ \begin{array}{cc} k_5: & (\Diamond\varphi\to\Box\psi)\to\Box(\varphi\to\psi) \end{array} \] \vspace{-0.5cm} \[ \infer[\text{Nec}]{\Gamma\vdash\Box\varphi}{\vdash\varphi} \] \end{center} possibly with additional axioms (such as intuitionistic variants of the T or 4 axioms). We call the logic with just the axiomatisation above, IK, as, in analogy with K, it forms the base of the IMLs. Simpson, in his thesis~\cite{simpson1994Thesis}, argues that the IMLs should be considered the real intuitionistic analogue to the normal modal logics and, as part of his argument for this position, shows he can obtain a normalising natural deduction system for the IMLs, using labelled formulae. However, from the perspective of constructive reasoning, axioms $k_3$ to $k_5$ are troublesome. This begs the question, if we remove axioms $k_3$ to $k_5$, can we obtain a constructively reasonable logic with a normalising natural deduction system with introduction and elimination rules for the modalities, as in the case of IK? The logic obtained by removing axioms $k_3$ to $k_5$, called ``Constructive K'' (CK), in fact, admits a non-labelled, normalising, natural deduction system, as discussed in~\cite{BellinDePaivaRitterCurryHowardForCK}. However, this system has an unfortunate and somewhat undesirable property\footnote{Undesirable, from the definitional point of view of the inference rules.} that the modalities each have only one inference rule that acts as both an introduction and an elimination rule. Not satisfied with this system, we instead propose a labelled, normalising, natural deduction system for CK, that can be considered a modification of Simpson's for IK, where $\Box$ and $\Diamond$ both have introduction and elimination rules. We do this by starting from Simpson's system for IK and, by combining the techniques of Strassberger, Das and Arisaka~\cite{StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics} and Masini~\cite{Masini2NatDed}, surgically removing features of the natural deduction system to make it sound and complete for CK. The methodology used is completely proof-theoretically motivated but certain interesting properties, obvious in the semantics, such as the upward closure condition for $\bot$ (c.f.~\cite{BellinDePaivaRitterCurryHowardForCK,degroot2025semanticalanalysisintuitionisticmodal}) come to the forefront in this calculus. We use Strassberger, Das and Arisaka~\cite{StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics} as a starting point, as they have a nested sequent calculus for CK that retains cut elimination. Nested calculi~\cite{Bruennler2009,StrassbergerDasArisakaNestedSequentsForConstructiveModalLogics} allow for strict tree-like reasoning where formulae can be considered as residing in ``branches'' of a tree. This tree-like reasoning is a core aspect of the proof system we develop. When eschewing ourselves of the explicitly nested structure of nested sequents, instead appealing to a labelling system, we have two choices of how to assign labels to formulae such that we preserve the tree-like reasoning structure: Firstly, one can label formulae by the sequence of nodes required to reach the ``position'' it is at, as used by Martini, Masini and Zorzi~\cite{MartiniMasiniMargheritaFrom2SequentsAndLinearToNatDed}. Whilst perfectly reasonable, doing so seems somewhat syntactically heavy. Furthermore, extending this approach to the rest of the cube seems somewhat unwieldy. Alternatively, one can use a simple labelling scheme, akin to that of Simpson's calculus for IK, instead demanding globally that the underlying graph of the consequence relation always remains a tree. This is the approach we take, though this restriction alone is not enough. To fully capture the ``nested-like'' reasoning, we also need to introduce the concept of context restrictions to rules. The restriction says that the derivation of hypothesis cannot occur using open assumptions holding at certain worlds. We observe that context restrictions are not completely novel, for they are present in Massini's 2-Natural Deduction~\cite{Masini2NatDed} for Deontic logic, albeit in a slightly different form. It turns out, these two modifications suffice to develop a normalising natural deduction system for CK and in fact, extending this calculus to the rest of the constructive modal cube is as trivial as in the case of IK, except in the case of logics with the ``B'' axiom, where the approach presented seems to break down.