# Temporal Refinements for Guarded Recursive Types

Guilhem Jaber, Colin Riba

► To cite this version:

Guilhem Jaber, Colin Riba. Temporal Refinements for Guarded Recursive Types. ESOP 2021 - 30th European Symposium on Programming, Mar 2021, Luxembourg, Luxembourg. pp.548-578, 10.1007/978-3-030-72019-3_20. hal-03517430

HAL Id: hal-03517430

https://hal.science/hal-03517430

Submitted on 24 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Temporal Refinements for Guarded Recursive Types

Guilhem Jaber, Colin Riba

► To cite this version:

Guilhem Jaber, Colin Riba. Temporal Refinements for Guarded Recursive Types. ESOP 2021 - 30th European Symposium on Programming, Mar 2021, Luxembourg, Luxembourg. pp.548-578, 10.1007/978-3-030-72019-3_20. hal-03517430

HAL Id: hal-03517430

https://hal.science/hal-03517430v1

Submitted on 24 May 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
<figure><img src="image_2.png" /></figure>

# Temporal Refinements for Guarded Recursive Types*

Guilhem Jaber¹ and Colin Riba² (✉)

Université de Nantes, LS2N CNRS, Inria, Nantes, France

guilhem.jaber@univ-nantes.fr

Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, Lyon Cedex 07, France

colin.riba@ens-lyon.fr

**Abstract.** We propose a logic for temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, represented via coinductive types. Specifications of programs use safety and liveness properties. Programs can then be proven to satisfy their specification in a compositional way, our logic being based on a type system. The logic is presented as a refinement type system over the guarded λ-calculus, a λ-calculus with guarded recursive types. The refinements are formulae of a modal μ-calculus which embeds usual temporal modal logics such as LTL and CTL. The semantics of our system is given within a rich structure, the topos of trees, in which we build a realizability model of the temporal refinement type system.

**Keywords:** coinductive types, guarded recursive types, μ-calculus, refinement types, topos of trees.

## 1 Introduction

Functional programming is by now well established to handle infinite data, thanks to declarative definitions and equational reasoning on high-level abstractions, in particular when infinite objects are represented with coinductive types. In such settings, programs in general do not terminate, but are expected to compute a part of their output in finite time. For example, a program expected to generate a stream should produce the next element in finite time: it is *productive*.

Our goal is to prove input-output temporal properties of higher-order programs that handle coinductive types. Logics like LTL, CTL or the modal μ-calculus are widely used to formulate, on infinite objects, safety and liveness properties. Safety properties state that some “bad” event will not occur, while liveness properties specify that “something good” will happen (see e.g. [9]). Typically, modalities like □ (*always*) or ◇ (*eventually*) are used to write properties of streams or infinite trees and specifications of programs over such data.

We consider temporal refinement types {$A \mid \varphi$}, where A is a standard type of our programming language, and $\varphi$ is a formula of the modal μ-calculus. Using

<footnote>* This work was partially supported by the ANR-14-CE25-0007 - RAPIDO and by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon.</footnote>
<figure><img src="image_2.png" /></figure>

# Temporal Refinements for Guarded Recursive Types*

Guilhem Jaber¹ and Colin Riba² (✉)

Université de Nantes, LS2N CNRS, Inria, Nantes, France

guilhem.jaber@univ-nantes.fr

Univ Lyon, EnsL, UCBL, CNRS, LIP, F-69342, Lyon Cedex 07, France

colin.riba@ens-lyon.fr

**Abstract.** We propose a logic for temporal properties of higher-order programs that handle infinite objects like streams or infinite trees, represented via coinductive types. Specifications of programs use safety and liveness properties. Programs can then be proven to satisfy their specification in a compositional way, our logic being based on a type system. The logic is presented as a refinement type system over the guarded λ-calculus, a λ-calculus with guarded recursive types. The refinements are formulae of a modal μ-calculus which embeds usual temporal modal logics such as LTL and CTL. The semantics of our system is given within a rich structure, the topos of trees, in which we build a realizability model of the temporal refinement type system.

**Keywords:** coinductive types, guarded recursive types, μ-calculus, refinement types, topos of trees.

## 1 Introduction

Functional programming is by now well established to handle infinite data, thanks to declarative definitions and equational reasoning on high-level abstractions, in particular when infinite objects are represented with coinductive types. In such settings, programs in general do not terminate, but are expected to compute a part of their output in finite time. For example, a program expected to generate a stream should produce the next element in finite time: it is *productive*.

Our goal is to prove input-output temporal properties of higher-order programs that handle coinductive types. Logics like LTL, CTL or the modal μ-calculus are widely used to formulate, on infinite objects, safety and liveness properties. Safety properties state that some “bad” event will not occur, while liveness properties specify that “something good” will happen (see e.g. [9]). Typically, modalities like □ (*always*) or ◇ (*eventually*) are used to write properties of streams or infinite trees and specifications of programs over such data.

We consider temporal refinement types {$A \mid \varphi$}, where A is a standard type of our programming language, and $\varphi$ is a formula of the modal μ-calculus. Using

<footnote>* This work was partially supported by the ANR-14-CE25-0007 - RAPIDO and by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon.</footnote>
refinement types [22], temporal connectives are not reflected in the programming language, and programs are formally independent from the shape of their temporal specifications. One can thus give different refinement types to the same program. For example, the following two types can be given to the same map function on streams:

$$ \begin{aligned} \text{map} : (&\{B | \psi\} \to \{A | \varphi\}) \to \{\text{Str } B | \Box\Box[\text{hd}]\psi\} \to \{\text{Str } A | \Box\Box[\text{hd}]\varphi\} \\ \text{map} : (&\{B | \psi\} \to \{A | \varphi\}) \to \{\text{Str } B | \Diamond\Box[\text{hd}]\psi\} \to \{\text{Str } A | \Diamond\Box[\text{hd}]\varphi\} \end{aligned} \tag{\star} $$

These types mean that given $f : B \to A$ s.t. $f(b)$ satisfies $\varphi$ if $b$ satisfies $\psi$, the function (map $f$) takes a stream with infinitely many (resp. ultimately all) elements satisfying $\psi$ to one with infinitely many (resp. ultimately all) elements satisfying $\varphi$. For $\varphi$ a formula over $A$, $[hd]\varphi$ is a formula over streams of $A$'s which holds on a given stream if $\varphi$ holds on its head element.

It is undecidable whether a given higher-order program satisfies a given input-output temporal property written with formulae of the modal $\mu$-calculus [41]. Having a type system is a partial workaround to this obstacle, which moreover enables to reason compositionally on programs, by decomposing a specification to the various components of a program in order to prove its global specification.

Our system is built on top of the guarded $\lambda$-calculus [18], a higher-order programming language with guarded recursion [52]. Guarded recursion is a simple device to control and reason about unfoldings of fixpoints. It can represent coinductive types [50] and provides a syntactic compositional productivity check [5].

Safety properties (e.g. $\Box[hd]\varphi$) can be correctly represented with guarded fixpoints, but not liveness properties (e.g. $\Diamond[hd]\varphi$, $\Diamond\Box[hd]\varphi$, $\Box\Box[hd]\varphi$). Combining liveness with guarded recursion is a challenging problem since guarded fixpoints tend to have unique solutions. Existing approaches to handle temporal types in presence of guarded recursion face similar difficulties. Functional reactive programming (FRP) [21] provides a Curry-Howard correspondence for temporal logics [32,33,17] in which logical connectives are reflected as programming constructs. When combining FRP with guarded recursion [44,7], and in particular to handle liveness properties [8], uniqueness of guarded fixpoints is tempered by specific recursors for temporal types.

Our approach is different from [8], as we wish as much as possible the logical level not to impact the program level. We propose a two level system, with the lower or *internal* level, which interacts with guarded recursion and at which only safety properties are correctly represented, and the higher or *external* one, at which liveness properties are correctly handled, but without direct access to guarded recursion. By restricting to the alternation-free modal $\mu$-calculus, in which fixpoints can always be computed in $\omega$-steps, one can syntactically reason on finite unfoldings of liveness properties, thus allowing for crossing down the safety barrier. Soundness is proved by a realizability interpretation based on the semantics of guarded recursion in the topos of trees [13], which correctly represents the usual set-theoretic final coalgebras of polynomial coinductive types [50].

We provide example programs involving linear structures (colists, streams, fair streams [17,8]) and branching structures (resumptions à la [44]), for which
refinement types [22], temporal connectives are not reflected in the programming language, and programs are formally independent from the shape of their temporal specifications. One can thus give different refinement types to the same program. For example, the following two types can be given to the same map function on streams:

$$ \begin{aligned} \mathit{map} : (&\{B \mid \psi\} \to \{A \mid \varphi\}) \to \{\mathit{Str} B \mid \Box\diamond[\mathit{hd}]\psi\} \to \{\mathit{Str} A \mid \Box\diamond[\mathit{hd}]\varphi\} \\ \mathit{map} : (&\{B \mid \psi\} \to \{A \mid \varphi\}) \to \{\mathit{Str} B \mid \Diamond\Box[\mathit{hd}]\psi\} \to \{\mathit{Str} A \mid \Diamond\Box[\mathit{hd}]\varphi\} \end{aligned} \tag{\star} $$

These types mean that given $f: B \to A$ s.t. $f(b)$ satisfies $\varphi$ if $b$ satisfies $\psi$, the function ($\mathit{map} f$) takes a stream with infinitely many (resp. ultimately all) elements satisfying $\psi$ to one with infinitely many (resp. ultimately all) elements satisfying $\varphi$. For $\varphi$ a formula over $A$, $[hd]\varphi$ is a formula over streams of $A$'s which holds on a given stream if $\varphi$ holds on its head element.

It is undecidable whether a given higher-order program satisfies a given input-output temporal property written with formulae of the modal $\mu$-calculus [41]. Having a type system is a partial workaround to this obstacle, which moreover enables to reason compositionally on programs, by decomposing a specification to the various components of a program in order to prove its global specification.

Our system is built on top of the guarded $\lambda$-calculus [18], a higher-order programming language with guarded recursion [52]. Guarded recursion is a simple device to control and reason about unfoldings of fixpoints. It can represent coinductive types [50] and provides a syntactic compositional productivity check [5].

Safety properties (e.g. $\Box[hd]\varphi$) can be correctly represented with guarded fixpoints, but not liveness properties (e.g. $\Diamond[hd]\varphi$, $\Diamond\Box[hd]\varphi$, $\Box\diamond[hd]\varphi$). Combining liveness with guarded recursion is a challenging problem since guarded fixpoints tend to have unique solutions. Existing approaches to handle temporal types in presence of guarded recursion face similar difficulties. Functional reactive programming (FRP) [21] provides a Curry-Howard correspondence for temporal logics [32,33,17] in which logical connectives are reflected as programming constructs. When combining FRP with guarded recursion [44,7], and in particular to handle liveness properties [8], uniqueness of guarded fixpoints is tempered by specific recursors for temporal types.

Our approach is different from [8], as we wish as much as possible the logical level not to impact the program level. We propose a two level system, with the lower or *internal* level, which interacts with guarded recursion and at which only safety properties are correctly represented, and the higher or *external* one, at which liveness properties are correctly handled, but without direct access to guarded recursion. By restricting to the alternation-free modal $\mu$-calculus, in which fixpoints can always be computed in $\omega$-steps, one can syntactically reason on finite unfoldings of liveness properties, thus allowing for crossing down the safety barrier. Soundness is proved by a realizability interpretation based on the semantics of guarded recursion in the topos of trees [13], which correctly represents the usual set-theoretic final coalgebras of polynomial coinductive types [50].

We provide example programs involving linear structures (colists, streams, fair streams [17,8]) and branching structures (resumptions à la [44]), for which
$$ \mathrm{Cons}^g := \lambda x. \lambda s. \mathrm{fold}(\langle x, s \rangle) : A \to \mathrm{Str}^g A \to \mathrm{Str}^g A $$

$$ \mathrm{hd}^g := \lambda s. \pi_0(\mathrm{unfold} s) : \mathrm{Str}^g A \to A $$

$$ \mathrm{tl}^g := \lambda s. \pi_1(\mathrm{unfold} s) : \mathrm{Str}^g A \to \mathrm{Str}^g A $$

$$ \mathrm{map}^g := \lambda f. \mathrm{fix}(g). \lambda s. \mathrm{Cons}^g (f(\mathrm{hd}^g s)) (g \circled{\scriptstyle (\mathrm{tl}^g s)}) : (B \to A) \to \mathrm{Str}^g B \to \mathrm{Str}^g A $$

<caption>**Fig. 1.** Constructor, Destructors and Map on Guarded Streams.</caption>

we prove liveness properties similar to (⋆) above. Our system also handles safety properties on breadth-first (infinite) tree traversals à la [35] and [10].

**Organization of the paper.** We give an overview of our approach in §2. Then §3 presents the syntax of the guarded λ-calculus. Our base temporal logic (without liveness) is introduced in §4, and is used to define our refinement type system in §5. Liveness properties are handled in §6. The semantics is given in §7, and §8 presents examples. Finally, we discuss related work in §9 and future work in §10. Table 4 (§8) gathers the main refinement types we can give to example functions, most of them defined in Table 3. Omitted material is available in [28].

## 2 Outline

**Overview of the Guarded λ-Calculus.** Guarded recursion enforces productivity of programs using a type system equipped with a type modality ▶, in order to indicate that one has access to a value not right now but only “later”. One can define guarded streams Strg A over a type A via the guarded recursive definition Strg A = A × ▶ Strg A. Streams that inhabit this type have their head available now, but their tail only one step in the future. The type modality ▶ is reflected in programs with the next operation. One also has a fixpoint constructor on terms fix(x).M for guarded recursive definitions. They are typed with

$$ \frac{\mathcal{E} \vdash M : A}{\mathcal{E} \vdash \mathrm{next}(M) : \mathrm{▶} A} $$

$$ \frac{\mathcal{E}, x : \mathrm{▶} A \vdash M : A}{\mathcal{E} \vdash \mathrm{fix}(x).M : A} $$

This allows for the constructor and basic destructors on guarded streams to be defined as in Fig. 1, where fold(-) and unfold(-) are explicit operations for folding and unfolding guarded recursive types. In the following, we use the infix notation a ::= s for Consg a s. Using the fact that the type modality ▶ is an applicative functor [49], we can distribute ▶ over the arrow type. This is represented in the programming language by the infix applicative operator ⊗. With it, one can define the usual map function on guarded streams as in Fig. 1.

**Compositional Safety Reasoning on Streams.** Given a property φ on a type A, we would like to consider a subtype of Strg A that selects those streams whose elements all satisfy φ. To do so, we use a temporal modal formula □[hd]φ,
$$ \mathrm{Cons}^g := \lambda x. \lambda s. \mathrm{fold}(\langle x, s \rangle) : A \to \mathrm{Str}^g A \to \mathrm{Str}^g A $$

$$ \mathrm{hd}^g := \lambda s. \pi_0(\mathrm{unfold} s) : \mathrm{Str}^g A \to A $$

$$ \mathrm{tl}^g := \lambda s. \pi_1(\mathrm{unfold} s) : \mathrm{Str}^g A \to \mathrm{Str}^g A $$

$$ \mathrm{map}^g := \lambda f. \mathrm{fix}(g). \lambda s. \mathrm{Cons}^g (f(\mathrm{hd}^g s)) (g \circled{\scriptstyle (\mathrm{tl}^g s)}) : (B \to A) \to \mathrm{Str}^g B \to \mathrm{Str}^g A $$

<caption>**Fig. 1.** Constructor, Destructors and Map on Guarded Streams.</caption>

we prove liveness properties similar to (⋆) above. Our system also handles safety properties on breadth-first (infinite) tree traversals à la [35] and [10].

**Organization of the paper.** We give an overview of our approach in §2. Then §3 presents the syntax of the guarded λ-calculus. Our base temporal logic (without liveness) is introduced in §4, and is used to define our refinement type system in §5. Liveness properties are handled in §6. The semantics is given in §7, and §8 presents examples. Finally, we discuss related work in §9 and future work in §10. Table 4 (§8) gathers the main refinement types we can give to example functions, most of them defined in Table 3. Omitted material is available in [28].

## 2 Outline

**Overview of the Guarded λ-Calculus.** Guarded recursion enforces productivity of programs using a type system equipped with a type modality ▶, in order to indicate that one has access to a value not right now but only “later”. One can define guarded streams Strg A over a type A via the guarded recursive definition Strg A = A × ▶ Strg A. Streams that inhabit this type have their head available now, but their tail only one step in the future. The type modality ▶ is reflected in programs with the next operation. One also has a fixpoint constructor on terms fix(x).M for guarded recursive definitions. They are typed with

$$ \frac{\mathcal{E} \vdash M : A}{\mathcal{E} \vdash \mathrm{next}(M) : \mathrm{▶} A} $$

$$ \frac{\mathcal{E}, x : \mathrm{▶} A \vdash M : A}{\mathcal{E} \vdash \mathrm{fix}(x).M : A} $$

This allows for the constructor and basic destructors on guarded streams to be defined as in Fig. 1, where fold(-) and unfold(-) are explicit operations for folding and unfolding guarded recursive types. In the following, we use the infix notation a ::= s for Consg a s. Using the fact that the type modality ▶ is an applicative functor [49], we can distribute ▶ over the arrow type. This is represented in the programming language by the infix applicative operator ⊗. With it, one can define the usual map function on guarded streams as in Fig. 1.

**Compositional Safety Reasoning on Streams.** Given a property ϕ on a type A, we would like to consider a subtype of Strg A that selects those streams whose elements all satisfy ϕ. To do so, we use a temporal modal formula □[hd]ϕ,
<table><caption>**Table 1.** Syntactic Classes and Judgments.</caption><thead><tr><th>Typed Formulae</th><th>Provability</th><th>Refinement Types</th><th>Subtyping</th><th>Typing</th></tr></thead><tbody><tr><td>Σ ⊢ ϕ : A<br>(§4)</td><td>شد ϕ<br>(where ⊢ ϕ : A, §4)</td><td>{A | ϕ}<br>(where ⊢ ϕ : A, §5)</td><td>T ≤ U<br>(T, U refinement types, §5)</td><td>ε ⊢ M : T</td></tr></tbody></table>

and consider the *refinement type* {$\text{Str}^g A \mid \Box[\text{hd}]\varphi$}. Suppose for now that we can give the following refinement types to the basic stream operations:

$$
\begin{align*}
\text{hd}^g & : \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \rightarrow \{A \mid \varphi\} \\
\text{tl}^g & : \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \rightarrow \bullet \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \\
\text{Cons}^g & : \{A \mid \varphi\} \rightarrow \bullet \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \rightarrow \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\}
\end{align*}
$$

By using the standard typing rules for λ-abstraction and application, together with the rules to type fix($x$).M and ⊕, we can type the function map<sup>g</sup> as

$$
\text{map}^g : (\{B \mid \psi\} \rightarrow \{A \mid \varphi\}) \rightarrow \{\text{Str}^g B \mid \Box[\text{hd}]\psi\} \rightarrow \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\}
$$

**A Manysorted Temporal Logic.** Our logical language, taken with minor adaptations from [30], is *manysorted*: for each type *A* we have formulae of type *A* (notation ⊢ *ϕ* : *A*), where *ϕ* selects inhabitants of *A*.

We use atomic modalities ([π<sub>i</sub>], [fold], [next],...) in refinements to navigate between types (see Fig. 5, §4). For instance, a formula *ϕ* of type *A*<sub>0</sub>, specifying a property over the inhabitants of *A*<sub>0</sub>, can be lifted to the formula [π<sub>0</sub>]*ϕ* of type *A*<sub>0</sub> × *A*<sub>1</sub>, which intuitively describes those inhabitants of *A*<sub>0</sub> × *A*<sub>1</sub> whose first component satisfy *ϕ*. Given a formula *ϕ* of type *A*, one can define its “head lift” [hd]*ϕ* of type Str<sup>*g*</sup> *A*, that enforces *ϕ* to be satisfied on the head of the provided stream. Also, one can define a modality ○ such that given a formula ψ : Str<sup>*g*</sup> *A*, the formula ○ψ : Str<sup>*g*</sup> *A* enforces ψ to be satisfied on the tail of the provided stream. These modalities are obtained resp. as [hd]*ϕ* := [fold][π<sub>0</sub>]*ϕ* and ○*ϕ* := [fold][π<sub>1</sub>][next]*ϕ*. We similarly have atomic modalities [in<sub>0</sub>], [in<sub>1</sub>] on sum types. For instance, on the type of guarded colists defined as CoList<sup>*g*</sup> *A* := Fix(X). 1 + A × ▶X, we can express the fact that a colist is empty (resp. non-empty) with the formula [nil] := [fold][in<sub>0</sub>]<sub>⊤</sub> (resp. [¬nil] := [fold][in<sub>1</sub>]<sub>⊤</sub>).

We also provide a deduction system ⊢<sup>A</sup> *ϕ* on temporal modal formulae. This deduction system is used to define a subtyping relation T ≤ U between refinement types, with {A | *ϕ*} ≤ {A | ψ} when ⊢<sup>A</sup> *ϕ* ⇒ ψ. The subtyping relation thus incorporates logical reasoning in the type system.

In addition, we have greatest fixpoints formulae ναϕ (so that formulae can have free typed propositional variables), equipped with Kozen's reasoning principles [43]. In particular, we can form an *always* modality as □ϕ := να. ϕ ∧ ○α, with □ϕ : Str<sup>*g*</sup> A if ϕ : Str<sup>*g*</sup> A. The formula □ϕ holds on a stream s = (s<sub>i</sub> | i ≥ 0), iff ϕ holds on every substream (s<sub>i</sub> | i ≥ n) for n ≥ 0. If we rather start with ψ : A, one first need to lift it to [hd]ψ : Str<sup>*g*</sup> A. Then □[hd]ψ means that all the elements of the stream satisfies ψ, since all its suffixes satisfy [hd]ψ.

Table 1 summarizes the different judgments used in this paper.
<table><caption>**Table 1.** Syntactic Classes and Judgments.</caption><thead><tr><th>Typed Formulae</th><th>Provability</th><th>Refinement Types</th><th>Subtyping</th><th>Typing</th></tr></thead><tbody><tr><td>Σ ⊢ ϕ : A<br>(§4)</td><td>⊢<sup>A</sup> ϕ<br>(where ⊢ ϕ : A, §4)</td><td>{A | ϕ}<br>(where ⊢ ϕ : A, §5)</td><td>T ≤ U<br>(T, U refinement types, §5)</td><td>ε ⊢ M : T</td></tr></tbody></table>

and consider the *refinement type* $\{\text{Str}^g A \mid \Box[\text{hd}]\varphi\}$. Suppose for now that we can give the following refinement types to the basic stream operations:

$$ 
\begin{align*}
\text{hd}^g & : \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \rightarrow \{A \mid \varphi\} \\
\text{tl}^g & : \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \rightarrow \bullet \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \\
\text{Cons}^g & : \{A \mid \varphi\} \rightarrow \bullet \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} \rightarrow \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\}
\end{align*}
$$

By using the standard typing rules for λ-abstraction and application, together with the rules to type fix($x$).M and ⊕, we can type the function map<sup>g</sup> as

$$ \text{map}^g : (\{B \mid \psi\} \rightarrow \{A \mid \varphi\}) \rightarrow \{\text{Str}^g B \mid \Box[\text{hd}]\psi\} \rightarrow \{\text{Str}^g A \mid \Box[\text{hd}]\varphi\} $$

**A Manysorted Temporal Logic.** Our logical language, taken with minor adaptations from [30], is *manysorted*: for each type *A* we have formulae of type *A* (notation ⊢ *ϕ* : *A*), where *ϕ* selects inhabitants of *A*.

We use atomic modalities ([π<sub>i</sub>], [fold], [next],...) in refinements to navigate between types (see Fig. 5, §4). For instance, a formula *ϕ* of type *A*<sub>0</sub>, specifying a property over the inhabitants of *A*<sub>0</sub>, can be lifted to the formula [π<sub>0</sub>]*ϕ* of type *A*<sub>0</sub> × *A*<sub>1</sub>, which intuitively describes those inhabitants of *A*<sub>0</sub> × *A*<sub>1</sub> whose first component satisfy *ϕ*. Given a formula *ϕ* of type *A*, one can define its “head lift” [hd]*ϕ* of type Str<sup>*g*</sup> *A*, that enforces *ϕ* to be satisfied on the head of the provided stream. Also, one can define a modality ○ such that given a formula ψ : Str<sup>*g*</sup> *A*, the formula ○ψ : Str<sup>*g*</sup> *A* enforces ψ to be satisfied on the tail of the provided stream. These modalities are obtained resp. as [hd]*ϕ* := [fold][π<sub>0</sub>]*ϕ* and ○*ϕ* := [fold][π<sub>1</sub>][next]*ϕ*. We similarly have atomic modalities [in<sub>0</sub>], [in<sub>1</sub>] on sum types. For instance, on the type of guarded colists defined as CoList<sup>*g*</sup> *A* := Fix(X). 1 + A × ▶X, we can express the fact that a colist is empty (resp. non-empty) with the formula [nil] := [fold][in<sub>0</sub>]<sup>⊤</sup> (resp. [¬nil] := [fold][in<sub>1</sub>]<sup>⊤</sup>).

We also provide a deduction system ⊢<sup>A</sup> *ϕ* on temporal modal formulae. This deduction system is used to define a subtyping relation T ≤ U between refinement types, with {A | *ϕ*} ≤ {A | ψ} when ⊢<sup>A</sup> *ϕ* ⇒ ψ. The subtyping relation thus incorporates logical reasoning in the type system.

In addition, we have greatest fixpoints formulae ναϕ (so that formulae can have free typed propositional variables), equipped with Kozen's reasoning principles [43]. In particular, we can form an *always* modality as □ϕ := να. ϕ ∧ ○α, with □ϕ : Str<sup>*g*</sup> *A* if ϕ : Str<sup>*g*</sup> *A*. The formula □ϕ holds on a stream s = (s<sub>i</sub> | i ≥ 0), iff ϕ holds on every substream (s<sub>i</sub> | i ≥ n) for n ≥ 0. If we rather start with ψ : A, one first need to lift it to [hd]ψ : Str<sup>*g*</sup> A. Then □[hd]ψ means that all the elements of the stream satisfies ψ, since all its suffixes satisfy [hd]ψ.

Table 1 summarizes the different judgments used in this paper.
**Beyond Safety.** In order to handle liveness properties, we also need to have least fixpoints formulae $\mu\alpha\varphi$. For example, this would give the eventually modality $\diamond\varphi := \mu\alpha$. $\varphi \lor \Box\alpha$. With Kozen-style rules, one could then give the following two types to the guarded stream constructor:

$$ 
\begin{align*}
\text{Cons}^g & : \{A \mid \varphi\} \rightarrow \text{Str}^g A \rightarrow \{\text{Str}^g A \mid \diamond[\text{hd}]\varphi\} \\
\text{Cons}^g & : A \rightarrow \text{Str}^g A \mid \diamond[\text{hd}]\varphi \rightarrow \{\text{Str}^g A \mid \diamond[\text{hd}]\varphi\}
\end{align*}
$$

But consider a finite base type B with two distinguished elements a, b, and suppose that we have access to a modality [b] on B so that terms inhabiting {$B \mid [b]$} must be equal to b. Using the above types for Cons<sup>g</sup>, we could type the stream with constant value a, defined as fix(s).a ::= 
, with the type {$\text{Str}^g B \mid \diamond[\text{hd}]b$} that is supposed to enforce the existence of an occurrence of b in the stream. Similarly, on colists we would have fix(s).a ::= 
 of type {$\text{CoList}^g B \mid \diamond[\text{nil}]$}, while $\diamond[\text{nil}]$ expresses that a colist will eventually contain a nil, and is thus finite. Hence, liveness properties may interact quite badly with guarded recursion. Let us look at this in a semantic model of guarded recursion.

**Internal Semantics in the Topos of Trees.** The types of the guarded $\lambda$-calculus can be interpreted as sequences of sets $(X(n))_{n>0}$ where $X(n)$ represents the values available “at time $n$”. In order to interpret guarded recursion, one also needs to have access to functions $r_n^X : X(n+1) \to X(n)$, which tell how values “at $n+1$” can be restricted (actually most often truncated) to values “at $n$”. This means that the objects used to represent types are in fact presheaves over the poset $(\mathbb{N} \setminus \{0\}, \leq)$. The category $S$ of such presheaves is the topos of trees [13]. For instance, the type $\text{Str}^g B$ of guarded streams over a finite base type B is interpreted in $S$ as $(B^n)_{n>0}$, with restriction maps taking $(b_0, \dots, b_{n-1}, b_n)$ to $(b_0, \dots, b_{n-1})$. We write $[[A]]$ for the interpretation of a type A in $S$.

**The Necessity of an External Semantics.** The topos of trees cannot correctly handle liveness properties. For instance, the formula $\diamond[\text{hd}][b]$ cannot describe in $S$ the set of streams that contain at least one occurrence of b. Indeed, the interpretation of $\diamond[\text{hd}][b]$ in $S$ is a sequence $(C(n))_{n>0}$ with $C(n) \subseteq B^n$. But any element of $B^n$ can be extended to a stream which contains an occurrence of b. Hence $C(n)$ should be equal to $B^n$, and the interpretation of $\diamond[\text{hd}][b]$ is the whole $[[\text{Str}^g B]]$. More generally, guarded fixpoints have unique solutions in the topos of trees [13], and $\diamond\varphi = \mu\alpha$. $\varphi \lor \Box\varphi$ gets the same interpretation as $\nu\alpha$. $\varphi \lor \Box\alpha$.

We thus have a formal system with least and greatest fixpoints, that has a semantics inside the topos of trees, but which does not correctly handle least fixpoints. On the other hand, it was shown by [50] that the interpretation of guarded polynomial (i.e. first-order) recursive types in $S$ induces final coalgebras for the corresponding polynomial functors on the category Set of usual sets and functions. This applies e.g. to streams and colists. Hence, it makes sense to think of interpreting least fixpoint formulae over such types externally, in Set.
**Beyond Safety.** In order to handle liveness properties, we also need to have least fixpoints formulae $\mu\alpha\varphi$. For example, this would give the eventually modality $\diamond\varphi := \mu\alpha$. $\varphi \lor \Box\alpha$. With Kozen-style rules, one could then give the following two types to the guarded stream constructor:

$$ 
\begin{align*}
\mathit{Cons}^g & : \{A \mid \varphi\} \rightarrow \mathbf{Str}^g A \rightarrow \{\mathit{Str}^g A \mid \diamond[\mathit{hd}]\varphi\} \\
\mathit{Cons}^g & : A \rightarrow \mathbf{Str}^g A \mid \diamond[\mathit{hd}]\varphi \rightarrow \{\mathit{Str}^g A \mid \diamond[\mathit{hd}]\varphi\}
\end{align*}
$$

But consider a finite base type B with two distinguished elements a, b, and suppose that we have access to a modality [b] on B so that terms inhabiting {$B | [b]$} must be equal to b. Using the above types for $\mathit{Cons}^g$, we could type the stream with constant value a, defined as $\mathit{fix}(s).a ::^g s$, with the type {$\mathit{Str}^g B | \diamond[\mathit{hd}] [b]$} that is supposed to enforce the existence of an occurrence of b in the stream. Similarly, on colists we would have $\mathit{fix}(s).a ::=^g s$ of type {$\mathit{CoList}^g B | \diamond[\mathit{nil}]$}, while $\diamond[\mathit{nil}]$ expresses that a colist will eventually contain a nil, and is thus finite. Hence, liveness properties may interact quite badly with guarded recursion. Let us look at this in a semantic model of guarded recursion.

**Internal Semantics in the Topos of Trees.** The types of the guarded $\lambda$-calculus can be interpreted as sequences of sets $(X(n))_{n>0}$ where $X(n)$ represents the values available “at time $n$”. In order to interpret guarded recursion, one also needs to have access to functions $r_n^X : X(n+1) \to X(n)$, which tell how values “at $n+1$” can be restricted (actually most often truncated) to values “at $n$”. This means that the objects used to represent types are in fact presheaves over the poset $(\mathbb{N} \setminus \{0\}, \leq)$. The category $S$ of such presheaves is the topos of trees [13]. For instance, the type $\mathbf{Str}^g B$ of guarded streams over a finite base type B is interpreted in $S$ as $(B^n)_{n>0}$, with restriction maps taking $(b_0, \dots, b_{n-1}, b_n)$ to $(b_0, \dots, b_{n-1})$. We write $[[A]]$ for the interpretation of a type A in $S$.

**The Necessity of an External Semantics.** The topos of trees cannot correctly handle liveness properties. For instance, the formula $\diamond[\mathit{hd}][b]$ cannot describe in $S$ the set of streams that contain at least one occurrence of b. Indeed, the interpretation of $\diamond[\mathit{hd}][b]$ in $S$ is a sequence $(C(n))_{n>0}$ with $C(n) \subseteq B^n$. But any element of $B^n$ can be extended to a stream which contains an occurrence of b. Hence $C(n)$ should be equal to $B^n$, and the interpretation of $\diamond[\mathit{hd}][b]$ is the whole $[[\mathbf{Str}^g B]]$. More generally, guarded fixpoints have unique solutions in the topos of trees [13], and $\diamond\varphi = \mu\alpha$. $\varphi \lor \Box\varphi$ gets the same interpretation as $\nu\alpha$. $\varphi \lor \Box\alpha$.

We thus have a formal system with least and greatest fixpoints, that has a semantics inside the topos of trees, but which does not correctly handle least fixpoints. On the other hand, it was shown by [50] that the interpretation of guarded polynomial (i.e. first-order) recursive types in $S$ induces final coalgebras for the corresponding polynomial functors on the category Set of usual sets and functions. This applies e.g. to streams and colists. Hence, it makes sense to think of interpreting least fixpoint formulae over such types externally, in Set.
<figure><img src="image_3.png" /><figcaption>Fig. 2. Internal and External Semantics</figcaption></figure>

**The Constant Type Modality.** Figure 2 represents adjoint functors $\Gamma : S \to \text{Set}$ and $\Delta : \text{Set} \to S$. To correctly handle least fixpoints $\mu\alpha\varphi : A$, we would like to see them as subsets of $\Gamma[[A]]$ in $\text{Set}$ rather than subobjects of $[[A]]$ in $S$. On the other hand, the internal semantics in $S$ is still necessary to handle definitions by guarded recursion. We navigate between the internal semantics in $S$ and the external semantics in $\text{Set}$ via the adjunction $\Delta \dashv \Gamma$. This adjunction induces a comonad $\Delta\Gamma$ on $S$, which is represented in the guarded $\lambda$-calculus of [18] by the constant type modality $\blacksquare$. This gives coinductive versions of guarded recursive types, e.g. $\text{Str A} := \blacksquare \text{Str}^g A$ for streams and $\text{CoList A} := \blacksquare \text{CoList}^g A$ for colists, which allow for productive but not causal programs [18, Ex. 1.10.(3)].

Each formula gets two interpretations: $[[\varphi]]$ in $S$ and $\{|\varphi|\}$ in $\text{Set}$. The external semantics $\{|\varphi|\}$ handles least fixpoints in the standard set-theoretic way, thus the two interpretations differ in general. But we do have $\{|\varphi|\} = \Gamma[[\varphi]]$ when $\varphi$ is safe (Def. 6.5), that is, when $\varphi$ describes a safety property. We have a modality $[\text{box}]\varphi$ which lifts $\varphi : A$ to $\blacksquare A$. By defining $[[[\text{box}]\varphi]] := \Delta \{|\varphi|\}$, we correctly handle the least fixpoints which are guarded by a $[\text{box}]$ modality. When $\varphi$ is safe, we can navigate between $\{\blacksquare A \mid [\text{box}]\varphi\}$ and $\{\blacksquare A \mid \varphi\}$, thus making available the comonad structure of $\blacksquare$ on $[\text{box}]\varphi$. Note that $[\text{box}]$ is unrelated to $\blacksquare$.

**Approximating Least Fixpoints.** For proving liveness properties on functions defined by guarded recursion, one needs to navigate between e.g. $[\text{box}]\diamond\varphi$ and $\diamond\varphi$, while $\diamond\varphi$ is in general unsafe. The fixpoint $\diamond\varphi = \mu\alpha.\varphi \vee \Box\alpha$ is alternation-free (see e.g. [16, §4.1]). This implies that $\diamond\varphi$ can be seen as the supremum of the $\Box^m\varphi$ for $m \in \mathbb{N}$, where each $\Box^m\varphi$ is safe when $\varphi$ is safe. More generally, we can approximate alternation-free $\mu\alpha\varphi$ by their finite unfoldings $\varphi^m(\perp)$, à la Kleene. We extend the logic with finite iterations $\mu^k\alpha\varphi$, where $k$ is an *iteration variable*, and where $\mu^k\alpha\varphi$ is seen as $\varphi^k(\perp)$. Let $\diamond^k\varphi := \mu^k\alpha$. $\varphi \vee \Box\alpha$. If $\varphi$ is safe then so is $\diamond^k\varphi$. For safe $\varphi$, $\psi$, we have the following refinement typings for the guarded recursive $\text{map}^g$ and its coinductive lift $\text{map}$:

$$ \text{map}^g : (\{B \mid \psi\} \to \{A \mid \varphi\}) \to \{\text{Str}^g B \mid \diamond^k [\text{hd}]\psi\} \to \{\text{Str}^g A \mid \diamond^k [\text{hd}]\varphi\} $$

$$ \text{map} : (\{B \mid \psi\} \to \{A \mid \varphi\}) \to \{\text{Str B} \mid [\text{box}]\diamond[\text{hd}]\psi\} \to \{\text{Str A} \mid [\text{box}]\diamond[\text{hd}]\varphi\} $$

## 3 The Pure Calculus

Our system lies on top of the guarded $\lambda$-calculus of [18]. We briefly review it here. We consider values and terms from the grammar given in Fig. 3 (left). In
<figure><img src="image_3.png" /><figcaption>Fig. 2. Internal and External Semantics</figcaption></figure>

**The Constant Type Modality.** Figure 2 represents adjoint functors $\Gamma : S \to \text{Set}$ and $\Delta : \text{Set} \to S$. To correctly handle least fixpoints $\mu\alpha\varphi : A$, we would like to see them as subsets of $\Gamma[[A]]$ in $\text{Set}$ rather than subobjects of $[[A]]$ in $S$. On the other hand, the internal semantics in $S$ is still necessary to handle definitions by guarded recursion. We navigate between the internal semantics in $S$ and the external semantics in $\text{Set}$ via the adjunction $\Delta \dashv \Gamma$. This adjunction induces a comonad $\Delta\Gamma$ on $S$, which is represented in the guarded $\lambda$-calculus of [18] by the constant type modality $\blacksquare$. This gives coinductive versions of guarded recursive types, e.g. $\text{Str A} := \blacksquare \text{Str}^g A$ for streams and $\text{CoList A} := \blacksquare \text{CoList}^g A$ for colists, which allow for productive but not causal programs [18, Ex. 1.10.(3)].

Each formula gets two interpretations: $[[\varphi]]$ in $S$ and $\{|\varphi|\}$ in $\text{Set}$. The external semantics $\{|\varphi|\}$ handles least fixpoints in the standard set-theoretic way, thus the two interpretations differ in general. But we do have $\{|\varphi|\} = \Gamma[[\varphi]]$ when $\varphi$ is safe (Def. 6.5), that is, when $\varphi$ describes a safety property. We have a modality $[\text{box}]\varphi$ which lifts $\varphi : A$ to $\blacksquare A$. By defining $[[[\text{box}]\varphi]] := \Delta \{|\varphi|\}$, we correctly handle the least fixpoints which are guarded by a $[\text{box}]$ modality. When $\varphi$ is safe, we can navigate between $\{\blacksquare A \mid [\text{box}]\varphi\}$ and $\{\blacksquare A \mid \varphi\}$, thus making available the comonad structure of $\blacksquare$ on $[\text{box}]\varphi$. Note that $[\text{box}]$ is unrelated to $\blacksquare$.

**Approximating Least Fixpoints.** For proving liveness properties on functions defined by guarded recursion, one needs to navigate between e.g. $[\text{box}]\diamond\varphi$ and $\diamond\varphi$, while $\diamond\varphi$ is in general unsafe. The fixpoint $\diamond\varphi = \mu\alpha.\varphi \vee \Box\alpha$ is alternation-free (see e.g. [16, §4.1]). This implies that $\diamond\varphi$ can be seen as the supremum of the $\Box^m\varphi$ for $m \in \mathbb{N}$, where each $\Box^m\varphi$ is safe when $\varphi$ is safe. More generally, we can approximate alternation-free $\mu\alpha\varphi$ by their finite unfoldings $\varphi^m(\perp)$, à la Kleene. We extend the logic with finite iterations $\mu^k\alpha\varphi$, where $k$ is an *iteration variable*, and where $\mu^k\alpha\varphi$ is seen as $\varphi^k(\perp)$. Let $\diamond^k\varphi := \mu^k\alpha.\varphi \vee \Box\alpha$. If $\varphi$ is safe then so is $\diamond^k\varphi$. For safe $\varphi$, $\psi$, we have the following refinement typings for the guarded recursive $\text{map}^g$ and its coinductive lift $\text{map}$:

$$ \text{map}^g : (\{B \mid \psi\} \to \{A \mid \varphi\}) \to \{\text{Str}^g B \mid \diamond^k [\text{hd}]\psi\} \to \{\text{Str}^g A \mid \diamond^k [\text{hd}]\varphi\} $$

$$ \text{map} : (\{B \mid \psi\} \to \{A \mid \varphi\}) \to \{\text{Str B} \mid [\text{box}]\diamond[\text{hd}]\psi\} \to \{\text{Str A} \mid [\text{box}]\diamond[\text{hd}]\varphi\} $$

## 3 The Pure Calculus

Our system lies on top of the guarded $\lambda$-calculus of [18]. We briefly review it here. We consider values and terms from the grammar given in Fig. 3 (left). In
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** Syntax and Operational Semantics of the Pure Calculus.</figcaption></figure>

both $\mathbf{box}_\sigma(M)$ and $\mathbf{prev}_\sigma(M)$, $\sigma$ is a *delayed substitution* of the form $\sigma = [x_1 \mapsto M_1, \dots, x_k \mapsto M_k]$ and such that $\mathbf{box}_\sigma(M)$ and $\mathbf{prev}_\sigma(M)$ bind $x_1, \dots, x_k$ in $M$. We use the following conventions of [18]: $\mathbf{box}(M)$ and $\mathbf{prev}(M)$ (without indicated substitution) stand resp. for $\mathbf{box}_\llbracket M \rrbracket$ and $\mathbf{prev}_\llbracket M \rrbracket$ ($i.e.$ bind no variable of $M$). Moreover, $\mathbf{box}_\iota(M)$ stands for $\mathbf{box}_{[x_1 \mapsto x_1, \dots, x_k \mapsto x_k]}(M)$ where $x_1, \dots, x_k$ is a list of all free variables of $M$, and similarly for $\mathbf{prev}_\iota(M)$. We consider the weak call-by-name reduction of [18], recalled in Fig. 3 (right).

Pure types (notation $A, B$, etc.) are the closed types over the grammar

$$A ::= \mathbf{1} \mid A + A \mid A \times A \mid A \to A \mid \mathbf{▶} A \mid X \mid \mathbf{Fix}(X).A \mid \mathbf{■} A$$

where, (1) in the case $\mathbf{Fix}(X).A$, each occurrence of $X$ in $A$ must be guarded by a $\mathbf{▶}$, and (2) in the case of $\mathbf{■}A$, the type $A$ is closed (i.e. has no free type variable). Guarded recursive types are built with the fixpoint constructor $\mathbf{Fix}(X).A$, which allows for $X$ to appear in $A$ both at positive and negative positions, but only under a $\mathbf{▶}$. In this paper we shall only consider positive types.

**Example 3.1.** We can code a finite base type $\mathbf{B} = \{\mathbf{b}_1, \dots, \mathbf{b}_n\}$ as a sum of unit types $\sum_{i=1}^n \mathbf{1} = \mathbf{1} + (\cdots + \mathbf{1})$, where the $i$th component of the sum is intended to represent the element $\mathbf{b}_i$ of $\mathbf{B}$. At the term level, the elements of $\mathbf{B}$ are represented as compositions of injections $\mathbf{in}_{j_1}(\mathbf{in}_{j_2}(\dots \mathbf{in}_{j_i}(\langle\rangle)))$. For instance, Booleans are represented by $\mathbf{Bool} := \mathbf{1} + \mathbf{1}$, with $\mathbf{tt} := \mathbf{in}_0(\langle\rangle)$ and $\mathbf{ff} := \mathbf{in}_1(\langle\rangle)$.

**Example 3.2.** Besides streams ($\mathbf{Str}^g A$), colists ($\mathbf{CoList}^g A$), conatural numbers ($\mathbf{CoNat}^g$) and infinite binary trees ($\mathbf{Tree}^g A$), we consider a type $\mathbf{Res}^g A$ of re-sumptions (parametrized by $\mathbf{I}, \mathbf{O}$) adapted from [44], and a higher-order recursive type $\mathbf{Rou}^g A$, used in Martin Hofmann's breadth-first tree traversal (see e.g. [10]):

$$ \begin{aligned} \mathbf{Tree}^g A &:= \mathbf{Fix}(X). A \times (\mathbf{▶} X \times \mathbf{▶} X) & \mathbf{CoNat}^g &:= \mathbf{Fix}(X). \mathbf{1} + \mathbf{▶} X \\ \mathbf{Res}^g A &:= \mathbf{Fix}(X). A + (\mathbf{I} \to (\mathbf{O} \times \mathbf{▶} X)) & \mathbf{Rou}^g A &:= \mathbf{Fix}(X). \mathbf{1} + ((\mathbf{▶} X \to \mathbf{▶} A) \to A) \end{aligned} $$

Some typing rules of the pure calculus are given in Fig. 4, where a pure type $A$ is *constant* if each occurrence of $\mathbf{▶}$ in $A$ is guarded by a $\mathbf{■}$. The omitted rules are the standard ones for simple types with finite sums and products [28, §A].
<figure><img src="image_4.png" /><figcaption>**Fig. 3.** Syntax and Operational Semantics of the Pure Calculus.</figcaption></figure>

both $\mathbf{box}_{\sigma}(M)$ and $\mathbf{prev}_{\sigma}(M)$, $\sigma$ is a *delayed substitution* of the form $\sigma = [x_1 \mapsto M_1, \dots, x_k \mapsto M_k]$ and such that $\mathbf{box}_{\sigma}(M)$ and $\mathbf{prev}_{\sigma}(M)$ bind $x_1, \dots, x_k$ in $M$. We use the following conventions of [18]: $\mathbf{box}(M)$ and $\mathbf{prev}(M)$ (without indicated substitution) stand resp. for $\mathbf{box}_{\llbracket} (M)$ and $\mathbf{prev}_{\llbracket} (M)$ i.e. bind no variable of $M$. Moreover, $\mathbf{box}_{\iota}(M)$ stands for $\mathbf{box}_{[x_1 \mapsto x_1, \dots, x_k \mapsto x_k]}(M)$ where $x_1, \dots, x_k$ is a list of all free variables of $M$, and similarly for $\mathbf{prev}_{\iota}(M)$. We consider the weak call-by-name reduction of [18], recalled in Fig. 3 (right).

Pure types (notation $A, B$, etc.) are the closed types over the grammar

$$A ::= \mathbf{1} \mid A + A \mid A \times A \mid A \to A \mid \mathbf{▶} A \mid X \mid \mathrm{Fix}(X).A \mid \mathbf{■} A$$

where, (1) in the case $\mathrm{Fix}(X).A$, each occurrence of $X$ in $A$ must be guarded by a $\mathbf{▶}$, and (2) in the case of $\mathbf{■}A$, the type $A$ is closed (i.e. has no free type variable). Guarded recursive types are built with the fixpoint constructor $\mathrm{Fix}(X).A$, which allows for $X$ to appear in $A$ both at positive and negative positions, but only under a $\mathbf{▶}$. In this paper we shall only consider positive types.

**Example 3.1.** We can code a finite base type $\mathbf{B} = \{\mathbf{b}_1, \dots, \mathbf{b}_n\}$ as a sum of unit types $\sum_{i=1}^n \mathbf{1} = \mathbf{1} + (\cdots + \mathbf{1})$, where the $i$th component of the sum is intended to represent the element $\mathbf{b}_i$ of $\mathbf{B}$. At the term level, the elements of $\mathbf{B}$ are represented as compositions of injections $\mathrm{in}_{j_1}(\mathrm{in}_{j_2}(\dots \mathrm{in}_{j_i}(\langle\rangle)))$. For instance, Booleans are represented by $\mathbf{Bool} := \mathbf{1} + \mathbf{1}$, with $\mathrm{tt} := \mathrm{in}_0(\langle\rangle)$ and $\mathrm{ff} := \mathrm{in}_1(\langle\rangle)$.

**Example 3.2.** Besides streams ($\mathrm{Str}^g A$), colists ($\mathrm{CoList}^g A$), conatural numbers ($\mathrm{CoNat}^g$) and infinite binary trees ($\mathrm{Tree}^g A$), we consider a type $\mathrm{Res}^g A$ of re-sumptions (parametrized by $\mathbf{I}, \mathbf{O}$) adapted from [44], and a higher-order recursive type $\mathrm{Rou}^g A$, used in Martin Hofmann's breadth-first tree traversal (see e.g. [10]):

$$ \begin{aligned} \mathrm{Tree}^g A &:= \mathrm{Fix}(X).A \times (\mathbf{▶} X \times \mathbf{▶} X) & \mathrm{CoNat}^g &:= \mathrm{Fix}(X).1 + \mathbf{▶} X \\ \mathrm{Res}^g A &:= \mathrm{Fix}(X).A + (\mathbf{I} \to (\mathbf{O} \times \mathbf{▶} X)) & \mathrm{Rou}^g A &:= \mathrm{Fix}(X).1 + ((\mathbf{▶} X \to \mathbf{▶} A) \to A) \end{aligned} $$

Some typing rules of the pure calculus are given in Fig. 4, where a pure type $A$ is *constant* if each occurrence of $\mathbf{▶}$ in $A$ is guarded by a $\mathbf{■}$. The omitted rules are the standard ones for simple types with finite sums and products [28, §A].
$$ \frac{\mathcal{E} \vdash M : A[\text{Fix}(X).A/X]}{\mathcal{E} \vdash \text{fold}(M) : \text{Fix}(X).A} \qquad \frac{\mathcal{E} \vdash M : \text{Fix}(X).A}{\mathcal{E} \vdash \text{unfold}(M) : A[\text{Fix}(X).A/X]} \qquad \frac{\mathcal{E} \vdash M : \text{ fun} (B \to A)}{\mathcal{E} \vdash M \otimes N : \text{ fun } A} \qquad \mathcal{E} \vdash N : \text{ fun } B $$

$$ \frac{\mathcal{E} \vdash M : A}{\mathcal{E} \vdash \text{next}(M) : \text{ fun } A} \qquad \frac{x_1 : A_1, \dots, x_k : A_k \vdash M : \text{ fun } A}{\mathcal{E} \vdash \text{prev}_{[x_1 \to M_1, \dots, x_k \to M_k]}(M) : A} $$

$$ \frac{x_1 : A_1, \dots, x_k : A_k \vdash M : A}{\mathcal{E} \vdash \text{box}_{[x_1 \to M_1, \dots, x_k \to M_k]}(M) : \mathbf{A}} \qquad \frac{\mathcal{E} \vdash M : \mathbf{A}}{\mathcal{E} \vdash \text{unbox}(M) : A} $$

<caption>Fig. 4. Typing Rules of the Pure Calculus (excerpt).</caption>

*Example 3.3.* Figure 1 defines some operations on guarded streams. On other types of Ex. 3.2, we have e.g. the constructors of colists $Nil^g := \text{fold}(\text{in}_0(\langle\rangle)) : \text{CoList}^g A$ and $\text{Cons}^g := \lambda x. \lambda s. \text{fold}(\text{in}_1(x, xs)) : A \to \text{CoList}^g A \to \text{CoList}^g A$. Infinite binary trees $\text{Tree}^g A$ have operations $\text{son}_d^g : \text{Tree}^g A \to \text{Tree}^g A$ for $d \in \{\ell, r\}$, $\text{Node}^g : A \to \text{Tree}^g A \to \text{Tree}^g A \to \text{Tree}^g A$ and $\text{label}^g : \text{Tree}^g A \to A$.

*Example 3.4.* Coinductive types are guarded recursive types under a $\blacksquare$. For instance $\text{Str} A := \blacksquare \text{Str}^g A$, $\text{CoList} A := \blacksquare \text{CoList}^g A$, $\text{CoNat} := \blacksquare \text{CoNat}^g A$ and $\text{Res} A := \blacksquare \text{Res}^g A$, with A, I, 0 constant. Basic operations on guarded types lift to coinductive ones. For instance

$$ \text{Cons} := \lambda x. \lambda s. \text{box}_t (\text{Cons}^g x \text{ next}(\text{unbox } s)) : A \to \text{Str} A \to \text{Str} A $$

$$ \text{hd} := \lambda s. \text{hd}^g (\text{unbox } s) : \text{Str } A \to A $$

$$ \text{tl} := \lambda s. \text{box}_t (\text{prev}_t (\text{tl}^g (\text{unbox } s))) : \text{Str } A \to \text{Str} A $$

These definitions follow a general pattern to lift a function over a guarded recursive type into one over its coinductive version, by performing an $\eta$-expansion with some box and unbox inserted in the right places. For example, one can define the map function on coinductive streams as:

$$ \text{map} := \lambda f. \lambda s. \text{box}_t (\text{map}^g f (\text{unbox } s)) : (B \to A) \longrightarrow \text{Str} B \longrightarrow \text{Str} A $$

# 4 A Temporal Modal Logic

We present here a logic of (modal) temporal specifications. We focus on syntactic aspects. The semantics is discussed in §7. For the moment the logic has only one form of fixpoints $(\nu\alpha\varphi)$. It is extended with least fixpoints $(\mu\alpha\varphi)$ in §6.

**Manysorted Modal Temporal Formulae.** The main ingredient of this paper is the logical language we use to annotate pure types when forming refinement types. This language, that we took with minor adaptations from [30], is *manysorted*: for each pure type A we have formulae $\varphi$ of type A (notation $\vdash \varphi : A$). The formulation rules of formulae are given in Fig. 5.

*Example 4.1.* Given a finite base type $B = \{b_1, \dots, b_n\}$ as in Ex. 3.1, with element $b_i$ represented by $\text{in}_{j_1}(\text{in}_{j_2}(\dots \text{in}_{j_i}(\langle\rangle)))$, the formula $[\text{in}_{j_1}][\text{in}_{j_2}]\dots[\text{in}_{j_i}]\top$ represents the singleton subset $\{b_k\}$ of $B$. On $\text{Bool}$, we have the formulae $[\text{tt}] := [\text{in}_0]\top$ and $[\text{ff}] := [\text{in}_1]\top$ representing resp. tt and ff.
$$ \frac{\mathcal{E} \vdash M : A[\text{Fix}(X).A/X]}{\mathcal{E} \vdash \text{fold}(M) : \text{Fix}(X).A} \qquad \frac{\mathcal{E} \vdash M : \text{Fix}(X).A}{\mathcal{E} \vdash \text{unfold}(M) : A[\text{Fix}(X).A/X]} \qquad \frac{\mathcal{E} \vdash M : \text{ fun} (B \to A)}{\mathcal{E} \vdash M \otimes N : \text{ fun } A} \qquad \mathcal{E} \vdash N : \text{ fun } B $$

$$ \frac{\mathcal{E} \vdash M : A}{\mathcal{E} \vdash \text{next}(M) : \text{ fun } A} \qquad \frac{x_1 : A_1, \dots, x_k : A_k \vdash M : \text{ fun } A}{\mathcal{E} \vdash \text{prev}_{[x_1 \to M_1, \dots, x_k \to M_k]}(M) : A} $$

$$ \frac{x_1 : A_1, \dots, x_k : A_k \vdash M : A}{\mathcal{E} \vdash \text{box}_{[x_1 \to M_1, \dots, x_k \to M_k]}(M) : \mathbf{A}} \qquad \frac{\mathcal{E} \vdash M : \mathbf{A}}{\mathcal{E} \vdash \text{unbox}(M) : A} $$

<caption>Fig. 4. Typing Rules of the Pure Calculus (excerpt).</caption>

*Example 3.3.* Figure 1 defines some operations on guarded streams. On other types of Ex. 3.2, we have e.g. the constructors of colists $\text{Nil}^g := \text{fold}(\text{in}_0(\langle\rangle)) : \text{CoList}^g A$ and $\text{Cons}^g := \lambda x. \lambda s. \text{fold}(\text{in}_1(x, xs)) : A \to \text{CoList}^g A \to \text{CoList}^g A$. Infinite binary trees $\text{Tree}^g A$ have operations $\text{son}^g_d : \text{Tree}^g A \to \text{Tree}^g A$ for $d \in \{\ell, r\}$, $\text{Node}^g : A \to \text{Tree}^g A \to \text{Tree}^g A \to \text{Tree}^g A$ and $\text{label}^g : \text{Tree}^g A \to A$.

*Example 3.4.* Coinductive types are guarded recursive types under a $\blacksquare$. For instance $\text{Str} A := \blacksquare \text{Str}^g A$, $\text{CoList} A := \blacksquare \text{CoList}^g A$, $\text{CoNat} := \blacksquare \text{CoNat}^g A$ and $\text{Res} A := \blacksquare \text{Res}^g A$, with A, I, O constant. Basic operations on guarded types lift to coinductive ones. For instance

$$ \text{Cons} := \lambda x. \lambda s. \text{box}_t (\text{Cons}^g x \text{ next}(\text{unbox } s)) : A \to \text{Str} A \to \text{Str} A $$

$$ \text{hd} := \lambda s. \text{hd}^g (\text{unbox } s) : \text{Str } A \to A $$

$$ \text{tl} := \lambda s. \text{box}_t (\text{prev}_t (\text{tl}^g (\text{unbox } s))) : \text{Str } A \to \text{Str} A $$

These definitions follow a general pattern to lift a function over a guarded recursive type into one over its coinductive version, by performing an $\eta$-expansion with some box and unbox inserted in the right places. For example, one can define the map function on coinductive streams as:

$$ \text{map} := \lambda f. \lambda s. \text{box}_t (\text{map}^g f (\text{unbox } s)) : (B \to A) \longrightarrow \text{Str} B \longrightarrow \text{Str} A $$

# 4 A Temporal Modal Logic

We present here a logic of (modal) temporal specifications. We focus on syntactic aspects. The semantics is discussed in §7. For the moment the logic has only one form of fixpoints $(\nu\alpha\varphi)$. It is extended with least fixpoints $(\mu\alpha\varphi)$ in §6.

**Manysorted Modal Temporal Formulae.** The main ingredient of this paper is the logical language we use to annotate pure types when forming refinement types. This language, that we took with minor adaptations from [30], is *manysorted*: for each pure type A we have formulae $\varphi$ of type A (notation $\vdash \varphi : A$). The formulation rules of formulae are given in Fig. 5.

*Example 4.1.* Given a finite base type $\mathbf{B} = \{\mathbf{b}_1, \dots, \mathbf{b}_n\}$ as in Ex. 3.1, with element $\mathbf{b}_i$ represented by $\text{in}_{j_1}(\text{in}_{j_2}(\dots \text{in}_{j_i}(\langle\rangle)))$, the formula $[\text{in}_{j_1}][\text{in}_{j_2}]\dots[\text{in}_{j_i}]\top$ represents the singleton subset $\{\mathbf{b}_k\}$ of $\mathbf{B}$. On $\text{Bool}$, we have the formulae $[\text{tt}] := [\text{in}_0]\top$ and $[\text{ff}] := [\text{in}_1]\top$ representing resp. tt and ff.
<figure><img src="image_5.png" /><figcaption>Fig. 5. Formation Rules of Formulae (where A, B are pure types).</figcaption></figure>

*Example 4.2.* (a) The formula $[hd][a] \Rightarrow \mathcal{O}[hd][b]$ means that if the head of a stream is *a*, then its second element (the head of its tail) should be *b*.

(b) On colists, we let $[hd]\varphi := [fold][in_1][\pi_0]\varphi$ and $\mathcal{O}\psi := [fold][in_1][\pi_1][next]\psi$.

(c) On (guarded) infinite binary trees over A, we also have a modality $[lbl]\varphi := [fold][\pi_0]\varphi: \text{Tree}^g A$ (provided $\varphi: A$). Moreover, we have modalities $\mathcal{O}_\ell$ and $\mathcal{O}_r$ defined on formulae $\varphi: \text{Tree}^g A$ as $\mathcal{O}_\ell\varphi := [fold][\pi_1][\pi_0][next]\varphi$ and $\mathcal{O}_r\varphi := [fold][\pi_1][\pi_1][next]\varphi$. Intuitively, $[lbl]\varphi$ should hold on a tree $t$ over A iff the root label of $t$ satisfies $\varphi$, and $\mathcal{O}_\ell\varphi$ (resp. $\mathcal{O}_r\varphi$) should hold on $t$ iff $\varphi$ holds on the left (resp. right) immediate subtree of $t$.

Formulae have fixpoints $\nu\alpha\varphi$. The rules of Fig. 5 thus allow for the formation of formulae with free typed propositional variables (ranged over by $\alpha, \beta, \dots$), and involve contexts $\Sigma$ of the form $\alpha_1 : A_1, \dots, \alpha_n : A_n$. In the formation of a fixpoint, the side condition “$\alpha$ guarded in $\varphi$” asks that each occurrence of $\alpha$ is beneath a $[next]$ modality. Because we are ultimately interested in the *external* set-theoretic semantics of formulae, we assume a usual positivity condition of $\alpha$ in $\varphi$. It is defined with relations $\alpha \text{ Pos } \varphi$ and $\alpha \text{ Neg } \varphi$ (see [28, §B]). We just mention here that $[\text{ev}(-)](-)$ is contravariant in its first argument. Note that $[box]\varphi$ can only be formed for *closed* $\varphi$.

*Example 4.3.* (a) The modality $\square$ makes it possible to express a range of safety properties. For instance, assuming $\varphi, \psi : \text{Str}^g A$, the formula $\square(\psi \Rightarrow \mathcal{O}\varphi)$ is intended to hold on a stream $s = (s_i | i \ge 0)$ iff, for all $n \in \mathbb{N}$, if $(s_i | i \ge n)$ satisfies $\psi$, then $(s_i | i \ge n+1)$ satisfies $\varphi$.

(b) The modality $\square$ has its two CTL-like variants on $\text{Tree}^g A$, namely $\forall\square\varphi := \nu\alpha$. $\varphi \wedge (\mathcal{O}_\ell\alpha \wedge \mathcal{O}_r\alpha)$ and $\exists\square\varphi := \nu\alpha$. $\varphi \wedge (\mathcal{O}_\ell\alpha \vee \mathcal{O}_r\alpha)$. Assuming $\psi: A$, $\forall\square[lbl]\psi$ is intended to hold on a tree $t: \text{Tree}^g A$ iff all node-labels of $t$ satisfy $\psi$, while $\exists\square[lbl]\psi$ holds on $t$ iff $\psi$ holds on all nodes of some infinite path from the root of $t$.
<figure><img src="image_5.png" /><figcaption>**Fig. 5.** Formation Rules of Formulae (where A, B are pure types).</figcaption></figure>

*Example 4.2.* (a) The formula $[hd][a] \Rightarrow \mathcal{O}[hd][b]$ means that if the head of a stream is *a*, then its second element (the head of its tail) should be *b*.

(b) On colists, we let $[hd]\varphi := [fold][in_1][\pi_0]\varphi$ and $\mathcal{O}\psi := [fold][in_1][\pi_1][next]\psi$.

(c) On (guarded) infinite binary trees over A, we also have a modality $[lbl]\varphi := [fold][\pi_0]\varphi : \text{Tree}^g A$ (provided $\varphi : A$). Moreover, we have modalities $\mathcal{O}_\ell$ and $\mathcal{O}_r$ defined on formulae $\varphi : \text{Tree}^g A$ as $\mathcal{O}_\ell\varphi := [fold][\pi_1][\pi_0][next]\varphi$ and $\mathcal{O}_r\varphi := [fold][\pi_1][\pi_1][next]\varphi$. Intuitively, $[lbl]\varphi$ should hold on a tree $t$ over A iff the root label of $t$ satisfies $\varphi$, and $\mathcal{O}_\ell\varphi$ (resp. $\mathcal{O}_r\varphi$) should hold on $t$ iff $\varphi$ holds on the left (resp. right) immediate subtree of $t$.

Formulae have fixpoints $\nu\alpha\varphi$. The rules of Fig. 5 thus allow for the formation of formulae with free typed propositional variables (ranged over by $\alpha, \beta, \dots$), and involve contexts $\Sigma$ of the form $\alpha_1 : A_1, \dots, \alpha_n : A_n$. In the formation of a fixpoint, the side condition “$\alpha$ guarded in $\varphi$” asks that each occurrence of $\alpha$ is beneath a $[next]$ modality. Because we are ultimately interested in the *external* set-theoretic semantics of formulae, we assume a usual positivity condition of $\alpha$ in $\varphi$. It is defined with relations $\alpha$ Pos $\varphi$ and $\alpha$ Neg $\varphi$ (see [28, §B]). We just mention here that $[ev(-)](-)$ is contravariant in its first argument. Note that $[box]\varphi$ can only be formed for *closed* $\varphi$.

*Example 4.3.* (a) The modality $\Box$ makes it possible to express a range of safety properties. For instance, assuming $\varphi, \psi : \text{Str}^g A$, the formula $\Box(\psi \Rightarrow \mathcal{O}\varphi)$ is intended to hold on a stream $s = (s_i | i \ge 0)$ iff, for all $n \in \mathbb{N}$, if $(s_i | i \ge n)$ satisfies $\psi$, then $(s_i | i \ge n+1)$ satisfies $\varphi$.

(b) The modality $\Box$ has its two CTL-like variants on $\text{Tree}^g A$, namely $\forall\Box\varphi := \nu\alpha$. $\varphi \wedge (\mathcal{O}_\ell\alpha \wedge \mathcal{O}_r\alpha)$ and $\exists\Box\varphi := \nu\alpha$. $\varphi \wedge (\mathcal{O}_\ell\alpha \vee \mathcal{O}_r\alpha)$. Assuming $\psi : A$, $\forall\Box[lbl]\psi$ is intended to hold on a tree $t : \text{Tree}^g A$ iff all node-labels of $t$ satisfy $\psi$, while $\exists\Box[lbl]\psi$ holds on $t$ iff $\psi$ holds on all nodes of some infinite path from the root of $t$.
<table><caption>**Table 2.** Modal Axioms and Rules. Types are omitted in $\vdash$ and (C) marks axioms assumed for $\vdash_c$ but not for $\vdash$. Properties of the non-atomic [hd] and $\bigcirc$ are derived.</caption><thead><tr><th>Name Formulation</th><th>[π<sub>i</sub>]</th><th>[fold]</th><th>[next]</th><th>[in<sub>i</sub>]</th><th>[ev(ψ)]</th><th>[box]</th><th>[hd]</th><th>○</th></tr></thead><tbody><tr><td>(RM) <span style="text-decoration: overline;">[ψ] ⇒ ϕ</span> / <span style="text-decoration: overline;">[Δ]ψ ⇒ [Δ]ϕ</span></td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(C) [Δ]ϕ ∧ [Δ]ψ ⇒ [Δ](ϕ ∧ ψ)</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(N) [Δ]<sup>T</sup></td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(P) [Δ]<sup>⊥</sup> ⇒ ⊥</td><td>✓</td><td>✓</td><td>(C)</td><td>✓</td><td></td><td>✓</td><td>✓</td><td>(C)</td></tr><tr><td>(C<sub>V</sub>) [Δ](ϕ ∨ ψ) ⇒ [Δ]ϕ ∨ [Δ]ψ</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(C<sub>⇒</sub>) ([Δ]ψ ⇒ [Δ]ϕ) ⇒ [Δ](ψ ⇒ ϕ)</td><td>✓</td><td>✓</td><td>(C)</td><td></td><td></td><td>✓</td><td>✓</td><td>(C)</td></tr></tbody></table>

**Modal Theories.** Formulae are equipped with a modal deduction system which enters the type system via a subtyping relation (§5). For each pure type A, we have an intuitionistic theory $\vdash^A$ (the general case) and a classical theory $\vdash_c^A$ (which is only assumed under ■/[box]), summarized in Fig. 6 and Table 2 (where we also give properties of the derived modalities [hd], $\bigcirc$). In any case, $\vdash_c^A$ $\varphi$ is only defined when $\vdash \varphi : A$ (and so when $\varphi$ has no free propositional variable).

Fixpoints $\nu\alpha\varphi$ are equipped with their usual Kozen axioms [43]. The atomic modalities $[\pi_i]$, $[fold]$, $[next]$, $[in_i]$ and $[box]$ have deterministic branching (see Fig. 12, §7). We can get the axioms of the intuitionistic (normal) modal logic IK [56] (see also e.g. [60,48]) for $[\pi_i]$, $[fold]$ and $[box]$ but not for $[in_i]$ nor for the intuitionistic $[next]$. For $[next]$, in the intuitionistic case this is due to semantic issues with step indexing (discussed in §7) which are absent from the classical case. As for $[in_i]$, we have a logical theory allowing for a coding of finite base types as finite sum types, which allows to derive, for a finite base type B:

$$ \vdash^B \bigvee_{a \in B} ([a] \wedge \bigwedge_{b \in B, b \neq a} \neg [b]) $$

**Definition 4.4 (Modal Theories).** For each pure type A, the intuitionistic and classical modal theories $\vdash^A \varphi$ and $\vdash_c^A \varphi$ (where $\vdash \varphi : A$) are defined by mutual induction:

- The theory $\vdash^A$ is deduction for intuitionistic propositional logic augmented with the check-marked (✓) axioms and rules of Table 2 and the axioms and rules of Fig. 6 (for $\vdash^A$).

- The theory $\vdash_c^A$ is $\vdash^A$ augmented with the axioms (P) and (C$\Rightarrow$) for $[next]$ and with the axiom (CL) (Fig. 6).

For example, we have $\vdash^{\text{Strg A}} \square\psi \Rightarrow (\psi \wedge \bigcirc \square\psi)$ and $\vdash^{\text{Strg A}} (\psi \wedge \bigcirc \square\psi) \Rightarrow \square\psi$.
<table><caption>**Table 2.** Modal Axioms and Rules. Types are omitted in $\vdash$ and (C) marks axioms assumed for $\vdash_c$ but not for $\vdash$. Properties of the non-atomic [hd] and ○ are derived.</caption><thead><tr><th>Name Formulation</th><th>[π<sub>i</sub>]</th><th>[fold]</th><th>[next]</th><th>[in<sub>i</sub>]</th><th>[ev(ψ)]</th><th>[box]</th><th>[hd]</th><th>○</th></tr></thead><tbody><tr><td>(RM) <span style="text-decoration: overline;">[</span>ψ ⇒ φ<br>☐<span style="text-decoration: overline;">[</span>ψ ⇒ [Δ]φ<br>☐</span></td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(C) [Δ]φ ∧ [Δ]ψ ⇒ [Δ](φ ∧ ψ)</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(N) [Δ]<sup>T</sup></td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(P) [Δ]⊥ ⇒ ⊥</td><td>✓</td><td>✓</td><td>(C)</td><td>✓</td><td></td><td>✓</td><td>✓</td><td>(C)</td></tr><tr><td>(C<sub>v</sub>) [Δ](φ ∨ ψ) ⇒ [Δ]φ ∨ [Δ]ψ</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td></td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>(C<sub>⇒</sub>) ([Δ]ψ ⇒ [Δ]φ) ⇒ [Δ](ψ ⇒ φ)</td><td>✓</td><td>✓</td><td>(C)</td><td></td><td></td><td>✓</td><td>✓</td><td>(C)</td></tr></tbody></table>

**Modal Theories.** Formulae are equipped with a modal deduction system which enters the type system via a subtyping relation (§5). For each pure type A, we have an intuitionistic theory $\vdash^A$ (the general case) and a classical theory $\vdash_c^A$ (which is only assumed under ■/[box]), summarized in Fig. 6 and Table 2 (where we also give properties of the derived modalities [hd], ○). In any case, $\vdash_c^A$ $\varphi$ is only defined when $\vdash \varphi : A$ (and so when $\varphi$ has no free propositional variable).

Fixpoints $\nu\alpha\varphi$ are equipped with their usual Kozen axioms [43]. The atomic modalities $[\pi_i]$, $[fold]$, $[next]$, $[in_i]$ and $[box]$ have deterministic branching (see Fig. 12, §7). We can get the axioms of the intuitionistic (normal) modal logic IK [56] (see also e.g. [60,48]) for $[\pi_i]$, $[fold]$ and $[box]$ but not for $[in_i]$ nor for the intuitionistic $[next]$. For $[next]$, in the intuitionistic case this is due to semantic issues with step indexing (discussed in §7) which are absent from the classical case. As for $[in_i]$, we have a logical theory allowing for a coding of finite base types as finite sum types, which allows to derive, for a finite base type B:

$$ \vdash^B \bigvee_{a \in B} ([a] \wedge \bigwedge_{b \in B, b \neq a} \neg [b]) $$

**Definition 4.4 (Modal Theories).** For each pure type A, the intuitionistic and classical modal theories $\vdash^A \varphi$ and $\vdash_c^A \varphi$ (where $\vdash \varphi : A$) are defined by mutual induction:

- The theory $\vdash^A$ is deduction for intuitionistic propositional logic augmented with the check-marked (✓) axioms and rules of Table 2 and the axioms and rules of Fig. 6 (for $\vdash^A$).

- The theory $\vdash_c^A$ is $\vdash^A$ augmented with the axioms (P) and (C$\Rightarrow$) for $[next]$ and with the axiom (CL) (Fig. 6).

For example, we have $\vdash^{\text{Strg A}} \Box \psi \Rightarrow (\psi \wedge \Box \psi)$ and $\vdash^{\text{Strg A}} (\psi \wedge \Box \psi) \Rightarrow \Box \psi$.
<figure><img src="image_6.png" /><figcaption>Fig. 6. Modal Axioms and Rules.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 7. Subtyping Rules (excerpt).</figcaption></figure>

## 5 A Temporally Refined Type System

Temporal refinement types (or types), notation $T, U, V$, etc., are defined by:

$$T, U ::= A \mid \{A \mid \varphi\} \mid T + T \mid T \times T \mid T \to T \mid \textcolor{red}{\bullet}T \mid \textcolor{blue}{\bullet}T$$

where $\vdash \varphi : A$ and, in the case of $\blacksquare T$, the type $T$ has no free type variable. So types are built from (closed) pure types $A$ and temporal refinements $\{A \mid \varphi\}$. They allow for all the type constructors of pure types.

As a refinement type $\{A \mid \varphi\}$ intuitively represents a subset of the inhabitants of $A$, it is natural to equip our system with a notion of *subtyping*. In addition to the usual rules for product, arrow and sum types, our subtyping relation is made of two more ingredients. The first follows the principle that our refinement type system is meant to prove properties of programs, and not to type more programs, so that (say) a type of the form $\{A \mid \varphi\} \to \{B \mid \psi\}$ is a subtype of $A \to B$. We formalize this with the notion of *underlying pure type* $|T|$ of a type $T$. The second ingredient is the modal theory $\vdash^A \varphi$ of §4. The subtyping rules concerning refinements are given in Fig. 7, where $T \equiv U$ enforces both $T \le U$ and $U \le T$. The full set of rules is given in [28, §C]. Notice that subtyping does not incorporate (un)folding of guarded recursive types.

Typing for refinement types is given by the rules of Fig. 8, together with the rules of §3 *extended to refinement types*, where $T$ is *constant* if $|T|$ is constant. Modalities $[\pi_i]$, $[\text{in}_i]$, $[\text{fold}]$ and $[\text{ev}(-)]$ (but not $[\text{next}]$) have introduction rules extending those of the corresponding term formers.
<figure><img src="image_6.png" /><figcaption>Fig. 6. Modal Axioms and Rules.</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 7. Subtyping Rules (excerpt).</figcaption></figure>

## 5 A Temporally Refined Type System

Temporal refinement types (or *types*), notation *T*, *U*, *V*, etc., are defined by:

$$T, U ::= A \mid \{A \mid \varphi\} \mid T + T \mid T \times T \mid T \to T \mid \textcolor{red}{\bullet}T \mid \textcolor{blue}{\blacksquare}T$$

where $\vdash \varphi : A$ and, in the case of $\blacksquare T$, the type *T* has no free type variable. So types are built from (closed) pure types *A* and temporal refinements $\{A \mid \varphi\}$. They allow for all the type constructors of pure types.

As a refinement type $\{A \mid \varphi\}$ intuitively represents a subset of the inhabitants of *A*, it is natural to equip our system with a notion of *subtyping*. In addition to the usual rules for product, arrow and sum types, our subtyping relation is made of two more ingredients. The first follows the principle that our refinement type system is meant to prove properties of programs, and not to type more programs, so that (say) a type of the form $\{A \mid \varphi\} \to \{B \mid \psi\}$ is a subtype of $A \to B$. We formalize this with the notion of *underlying pure type* $|T|$ of a type *T*. The second ingredient is the modal theory $\vdash^A \varphi$ of §4. The subtyping rules concerning refinements are given in Fig. 7, where $T \equiv U$ enforces both $T \le U$ and $U \le T$. The full set of rules is given in [28, §C]. Notice that subtyping does not incorporate (un)folding of guarded recursive types.

Typing for refinement types is given by the rules of Fig. 8, together with the rules of §3 extended to refinement types, where *T* is constant if $|T|$ is constant. Modalities $[\pi_i]$, $[\text{in}_i]$, $[\text{fold}]$ and $[\text{ev}(-)]$ (but not $[\text{next}]$) have introduction rules extending those of the corresponding term formers.
<figure><img src="image_8.png" /><figcaption>Fig. 8. Typing Rules for Refined Modal Types.</figcaption></figure>

**Example 5.1.** Since $\varphi \Rightarrow \psi \Rightarrow (\varphi \wedge \psi)$ and using two times the rule (MP), we get the first derived rule below, from which we can deduce the second one:

$$ \frac{\mathcal{E} \vdash M : \{A \mid \varphi\} \quad \mathcal{E} \vdash M : \{A \mid \psi\} \qquad \mathcal{E} \vdash M : \{A \mid \varphi\} \quad \mathcal{E} \vdash N : \{B \mid \psi\}}{\mathcal{E} \vdash M : \{A \mid \varphi \wedge \psi\}} \qquad \mathcal{E} \vdash \langle M, N \rangle : \{A \times B \mid [\pi_0]\varphi \wedge [\pi_1]\psi\} $$

**Example 5.2.** We have the following derived rules:

$$ \frac{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \Box \varphi\}}{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \varphi \wedge \Box \varphi\}} \quad \text{and} \quad \frac{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \varphi \wedge \Box \varphi\}}{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \Box \varphi\}} $$

**Example 5.3.** We have $\text{Cons}^g : A \to \bullet \{\text{Str}^g A \mid \varphi\} \to \{\text{Str}^g A \mid \Box \varphi\}$ as well as $\text{tl}^g : \{\text{Str}^g A \mid \Box \varphi\} \to \bullet \{\text{Str}^g A \mid \varphi\}$.

**Example 5.4 ("Always" (□) on Guarded Streams).** The refined types of $\text{Cons}^g$, $\text{hd}^g$, $\text{tl}^g$ and $\text{map}^g$ mentioned in §2 are easy to derive. We also have the type

$$ \{\text{Str}^g A \mid \Box[\text{hd}]\varphi_0\} \to \{\text{Str}^g A \mid \Box[\text{hd}]\varphi_1\} \to \{\text{Str}^g A \mid \Box([\text{hd}]\varphi_0 \vee [\text{hd}]\varphi_1)\} $$

for the merge$^g$ function which takes two guarded streams and interleaves them:

$$ \begin{array}{l} \text{merge}^g : \text{Str}^g A \to \text{Str}^g A \to \text{Str}^g A \\ \qquad := \text{fix}(g) \cdot \lambda s_0 \cdot \lambda s_1. (\text{hd}^g s_0) ::^g \text{ next}((\text{hd}^g s_1) ::^g (g \circledast (\text{tl}^g s_0) \circledast (\text{tl}^g s_1))) \end{array} $$

# 6 The Full System

The system presented so far has only one form of fixpoints in formulae ($\nu\alpha\varphi$). We now present our full system, which also handles least fixpoints ($\mu\alpha\varphi$) and thus liveness properties. A key role is played by *polynomial* guarded recursive types, that we discuss first.
<figure><img src="image_8.png" /><figcaption>Fig. 8. Typing Rules for Refined Modal Types.</figcaption></figure>

*Example 5.1.* Since $\varphi \Rightarrow \psi \Rightarrow (\varphi \wedge \psi)$ and using two times the rule (MP), we get the first derived rule below, from which we can deduce the second one:

$$ \frac{\mathcal{E} \vdash M : \{A \mid \varphi\} \quad \mathcal{E} \vdash M : \{A \mid \psi\} \qquad \mathcal{E} \vdash M : \{A \mid \varphi\} \quad \mathcal{E} \vdash N : \{B \mid \psi\}}{\mathcal{E} \vdash M : \{A \mid \varphi \wedge \psi\}} \qquad (\text{InN}_i\text{-I}) \quad \mathcal{E} \vdash \langle M, N \rangle : \{A \times B \mid [\pi_0]\varphi \wedge [\pi_1]\psi\} $$

*Example 5.2.* We have the following derived rules:

$$ \frac{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \Box \varphi\}}{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \varphi \wedge \Box \varphi\}} \quad \text{and} \quad \frac{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \varphi \wedge \Box \varphi\}}{\mathcal{E} \vdash M : \{\text{Str}^g A \mid \Box \varphi\}} $$

*Example 5.3.* We have $\text{Cons}^g : A \to \bullet \{\text{Str}^g A \mid \varphi\} \to \{\text{Str}^g A \mid \Box \varphi\}$ as well as $\text{tl}^g : \{\text{Str}^g A \mid \Box \varphi\} \to \bullet \{\text{Str}^g A \mid \varphi\}$.

*Example 5.4* (“Always” (□) on Guarded Streams). The refined types of $\text{Cons}^g$, $\text{hd}^g$, $\text{tl}^g$ and $\text{map}^g$ mentioned in §2 are easy to derive. We also have the type

$$ \{\text{Str}^g A \mid \Box[\text{hd}]\varphi_0\} \to \{\text{Str}^g A \mid \Box[\text{hd}]\varphi_1\} \to \{\text{Str}^g A \mid \Box([\text{hd}]\varphi_0 \vee [\text{hd}]\varphi_1)\} $$

for the merge$^g$ function which takes two guarded streams and interleaves them:

$$ \begin{array}{rcl} \text{merge}^g : & \text{Str}^g A \to \text{Str}^g A & \to \text{Str}^g A \\ & := \text{fix}(g) \cdot \lambda s_0 \cdot \lambda s_1. & (\text{hd}^g s_0) ::^g \text{ next}((\text{hd}^g s_1) ::^g (g \circledast (\text{tl}^g s_0) \circledast (\text{tl}^g s_1))) \end{array} $$

# 6 The Full System

The system presented so far has only one form of fixpoints in formulae ($\nu\alpha\varphi$). We now present our full system, which also handles least fixpoints ($\mu\alpha\varphi$) and thus liveness properties. A key role is played by *polynomial* guarded recursive types, that we discuss first.
$$ (\mu\text{-F}) \frac{\Sigma, \alpha : A \vdash \varphi : A}{\Sigma \vdash \mu\alpha\varphi : A} \qquad \frac{\Sigma, \alpha : A \vdash \varphi : A}{\Sigma \vdash \mu^t \alpha\varphi : A} \qquad \frac{\Sigma, \alpha : A \vdash \varphi : A}{\Sigma \vdash \nu^t \alpha\varphi : A} $$

**Fig. 9.** Extended Formation Rules of Formulae (with $\alpha$ Pos $\varphi$ and $\alpha$ guarded in $\varphi$).

$$ \begin{array}{ccc} \vdash^A \varphi[\mu\alpha\varphi/\alpha] \Rightarrow \mu\alpha\varphi & \vdash^A \varphi[\psi/\alpha] \Rightarrow \psi \\ \vdash^A \theta^{t+1}\alpha\varphi \Leftrightarrow \varphi[\theta^t\alpha\varphi/\alpha] & \vdash^A \mu^0\alpha\varphi \Leftrightarrow \perp & \vdash^A \nu^0\alpha\varphi \Leftrightarrow \top \\ \llbracket \mathbf{t} \rrbracket \le \llbracket \mathbf{u} \rrbracket & \vdash^A \mu^t\alpha\varphi \Rightarrow \mu^u\alpha\varphi & \vdash^A \nu^t\alpha\varphi \Rightarrow \nu^u\alpha\varphi \\ \vdash^A \mu^t\alpha\varphi \Rightarrow \mu^u\alpha\varphi & \vdash^A \mu^t\alpha\varphi \Rightarrow \mu\alpha\varphi & \vdash^A \nu^t\alpha\varphi \Rightarrow \nu^u\alpha\varphi \\ \end{array} $$

**Fig. 10.** Extended Modal Axioms and Rules (with $A$ a pure type and $\theta$ either $\mu$ or $\nu$).

**Strictly Positive and Polynomial Types.** *Strictly positive types* (notation $P^+, Q^+, \text{etc.}$) are given by

$$ P^+ ::= A \mid X \mid \mathbf{▶} P^+ \mid P^+ + P^+ \mid P^+ \times P^+ \mid \mathrm{Fix}(X).P^+ \mid B \to P^+ $$

where $A, B$ are (closed) *constant* pure types. Strictly positive types are a convenient generalization of polynomial types. A guarded recursive type $\mathrm{Fix}(X).P(X)$ is *polynomial* if $P(X)$ is induced by

$$ P(X) ::= A \mid \mathbf{▶} X \mid P(X) + P(X) \mid P(X) \times P(X) \mid B \to P(X) $$

where $A, B$ are (closed) *constant* pure types. Note that if $\mathrm{Fix}(X).P(X)$ is polynomial, $X$ cannot occur on the left of an arrow ($\to$) in $P(X)$. We say that $\mathrm{Fix}(X).P(X)$ (resp. $P^+$) is *finitary* polynomial (resp. *finitary* strictly positive) if $B$ is a finite base type (see Ex. 3.1) in the above grammars. The set-theoretic counterpart of our polynomial recursive types are the *exponent* polynomial functions of [31], which all have final **Set-coalgebras** (see e.g. [31, Cor. 4.6.3]).

**Example 6.1.** For $A$ a constant pure type, e.g. $\mathrm{Strg}^g A$, $\mathrm{CoList}^g A$ and $\mathrm{Tree}^g A$ as well as $\mathrm{Strg}^g(\mathrm{Str} A)$, $\mathrm{CoList}^g(\mathrm{Str} A)$ and $\mathrm{Res}^g A$ (with I, O constant) are polynomial. More generally, polynomial types include all recursive types $\mathrm{Fix}(X).P(X)$ where $P(X)$ is of the form $\sum_{i=0}^n A_i \times (\mathbf{▶}X)^{B_i}$ with $A_i, B_i$ constant. The non-strictly positive recursive type $\mathrm{Rou}^g A$ of Ex. 3.2, used in Hofmann's breadth-first traversal (see e.g. [10]), is not polynomial.

**The Full Temporal Modal Logic.** We assume given a first-order signature of *iteration terms* (notation $t, u, \text{etc.}$), with *iteration variables* $k, \ell, \text{etc.}$, and for each iteration term $t(k_1, \dots, k_m)$ with variables as shown, a given primitive recursive function $\llbracket t \rrbracket : \mathbb{N}^m \to \mathbb{N}$. We assume a term 0 for $0 \in \mathbb{N}$ and a term $k+1$ for the successor function $n \in \mathbb{N} \mapsto n+1 \in \mathbb{N}$.
$$ (\mu\text{-F}) \frac{\Sigma, \alpha : A \vdash \varphi : A}{\Sigma \vdash \mu\alpha\varphi : A} \quad \frac{\Sigma, \alpha : A \vdash \varphi : A}{\Sigma \vdash \mu^t \alpha\varphi : A} \quad \frac{\Sigma, \alpha : A \vdash \varphi : A}{\Sigma \vdash \nu^t \alpha\varphi : A} $$

**Fig. 9.** Extended Formation Rules of Formulae (with $\alpha$ Pos $\varphi$ and $\alpha$ guarded in $\varphi$).

$$ \begin{array}{ccc} \vdash^A \varphi[\mu\alpha\varphi/\alpha] \Rightarrow \mu\alpha\varphi & \vdash^A \varphi[\psi/\alpha] \Rightarrow \psi \\ \vdash^A \theta^{t+1}\alpha\varphi \Leftrightarrow \varphi[\theta^t\alpha\varphi/\alpha] & \vdash^A \mu^0\alpha\varphi \Leftrightarrow \perp & \vdash^A \nu^0\alpha\varphi \Leftrightarrow \top \\ \llbracket \mathbf{t} \rrbracket \le \llbracket \mathbf{u} \rrbracket & \vdash^A \mu^t\alpha\varphi \Rightarrow \mu^u\alpha\varphi & \vdash^A \nu^t\alpha\varphi \Rightarrow \nu^u\alpha\varphi \\ \vdash^A \mu^t\alpha\varphi \Rightarrow \mu^u\alpha\varphi & \vdash^A \mu^t\alpha\varphi \Rightarrow \mu\alpha\varphi & \vdash^A \nu^t\alpha\varphi \Rightarrow \nu^u\alpha\varphi \\ \end{array} $$

**Fig. 10.** Extended Modal Axioms and Rules (with $A$ a pure type and $\theta$ either $\mu$ or $\nu$).

**Strictly Positive and Polynomial Types.** *Strictly positive types* (notation $P^+, Q^+, \text{etc.}$) are given by

$$ P^+ ::= A \mid X \mid \mathbf{▶} P^+ \mid P^+ + P^+ \mid P^+ \times P^+ \mid \mathrm{Fix}(X).P^+ \mid B \to P^+ $$

where $A, B$ are (closed) *constant* pure types. Strictly positive types are a convenient generalization of polynomial types. A guarded recursive type $\mathrm{Fix}(X).P(X)$ is *polynomial* if $P(X)$ is induced by

$$ P(X) ::= A \mid \mathbf{▶} X \mid P(X) + P(X) \mid P(X) \times P(X) \mid B \to P(X) $$

where $A, B$ are (closed) *constant* pure types. Note that if $\mathrm{Fix}(X).P(X)$ is polynomial, $X$ cannot occur on the left of an arrow ($\to$) in $P(X)$. We say that $\mathrm{Fix}(X).P(X)$ (resp. $P^+$) is *finitary* polynomial (resp. *finitary* strictly positive) if $B$ is a finite base type (see Ex. 3.1) in the above grammars. The set-theoretic counterpart of our polynomial recursive types are the *exponent* polynomial functions of [31], which all have final **Set-coalgebras** (see e.g. [31, Cor. 4.6.3]).

**Example 6.1.** For $A$ a constant pure type, e.g. $\mathrm{Strg}^g A$, $\mathrm{CoList}^g A$ and $\mathrm{Tree}^g A$ as well as $\mathrm{Strg}^g(\mathrm{Str} A)$, $\mathrm{CoList}^g(\mathrm{Str} A)$ and $\mathrm{Res}^g A$ (with I, O constant) are polynomial. More generally, polynomial types include all recursive types $\mathrm{Fix}(X).P(X)$ where $P(X)$ is of the form $\sum_{i=0}^n A_i \times (\mathbf{▶}X)^{B_i}$ with $A_i, B_i$ constant. The non-strictly positive recursive type $\mathrm{Rou}^g A$ of Ex. 3.2, used in Hofmann's breadth-first traversal (see e.g. [10]), is not polynomial.

**The Full Temporal Modal Logic.** We assume given a first-order signature of *iteration terms* (notation $t, u, \text{etc.}$), with *iteration variables* $k, \ell, \text{etc.}$, and for each iteration term $t(k_1, \dots, k_m)$ with variables as shown, a given primitive recursive function $\llbracket t \rrbracket : \mathbb{N}^m \to \mathbb{N}$. We assume a term $\mathbf{0}$ for $\mathbf{0} \in \mathbb{N}$ and a term $k+1$ for the successor function $n \in \mathbb{N} \mapsto n+1 \in \mathbb{N}$.
The formulae of the full temporal modal logic extend those of Fig. 5 with least fixpoints $\mu\alpha\varphi$ and with approximated fixpoints $\mu^t\alpha\varphi$ and $\nu^t\alpha\varphi$ where $t$ is an iteration term. The additional formation rule for formulae are given in Fig. 9. We use $\theta$ as a generic notation for $\mu$ and $\nu$. Least fixpoints $\mu\alpha\varphi$ are equipped with their usual Kozen axioms. In addition, iteration formulae $\nu^t\alpha\varphi(\alpha)$ and $\mu^t\alpha\varphi(\alpha)$ have axioms expressing that they are indeed iterations of $\varphi(\alpha)$ from resp. $\top$ and $\bot$. A fixpoint logic with iteration variables was already considered in [63].

**Definition 6.2 (Full Modal Theories).** The full intuitionistic and classical modal theories (still denoted $\vdash^A$ and $\vdash_c^A$) are defined by extending Def. 4.4 with the axioms and rules of Fig. 10.

*Example 6.3.* Least fixpoints allow us to define liveness properties. On streams and colists, we have $\diamond\varphi := \mu\alpha$. $\varphi \vee \Box\alpha$ and $\varphi \cup \psi := \mu\alpha$. $\psi \vee (\varphi \wedge \Box\alpha)$. On trees, we have the CTL-like $\exists\diamond\varphi := \mu\alpha$. $\varphi \vee (\Box\ell\alpha \vee \Box r\alpha)$ and $\forall\diamond\varphi := \mu\alpha$. $\varphi \vee (\Box\ell\alpha \wedge \Box r\alpha)$. The formula $\exists\diamond\varphi$ is intended to hold on a tree if there is a finite path which leads to a subtree satisfying $\varphi$, while $\forall\diamond\varphi$ is intended to hold if every infinite path crosses a subtree satisfying $\varphi$.

*Remark 6.4.* On finitary trees (as in Ex. 6.1 but with $A_i, B_i$ finite base types), we have all formulae of the modal $\mu$-calculus. For this fragment, satisfiability is decidable (see e.g. [16]), as well as the classical theory $\vdash_c$ by completeness of Kozen's axiomatization [68] (see [58] for completeness results on fragments of the $\mu$-calculus).

**The Safe and Smooth Fragments.** We now discuss two related but distinct fragments of the temporal modal logic. Both fragments directly impact the refinement type system by allowing for more typing rules.

The safe fragment plays a crucial role, because it reconciles the internal and external semantics of our system (see §7). It gives subtyping rules for ■ (Fig. 11), which makes available the comonad structure of ■ on $[\boxtimes]\varphi$ when $\varphi$ is safe.

**Definition 6.5 (Safe Formula).** Say $\alpha_1 : A_1, \dots, \alpha_n : A_n \vdash \varphi : A$ is safe if

(i) the types $A_1, \dots, A_n$, $A$ are strictly positive, and

(ii) for each occurrence in $\varphi$ of a modality $[ev(\psi)]$, the formula $\psi$ is closed, and

(iii) each occurrence in $\varphi$ of a least fixpoint ($\mu\alpha(-)$) and of an implication ($\Rightarrow$) is guarded by a $[box]$.

Note that the safe restriction imposes no condition on approximated fixpoints $\theta^t\alpha$. Recalling that the theory under a $[box]$ is $\vdash_c^A$, the only propositional connectives accessible to $\vdash^A$ in safe formulae are those on which $\vdash^A$ and $\vdash_c^A$ coincide. The formula $[\neg nil] = [fold][in_1]\top$ is safe. Moreover:

*Example 6.6.* Any formula without fixpoint nor $[ev(-)]$ is equivalent in $\vdash_c$ to a safe one. It $\varphi$ is safe, then so are $[hd]\varphi$, $[lbl]\varphi$, as well as $\Delta\varphi$ (for $\Delta \in \{\Box, \forall\Box, \exists\Box\}$) and $[box]\Delta\varphi$ (for $\Delta \in \{\diamond, \exists\diamond, \forall\diamond\}$).
The formulae of the full temporal modal logic extend those of Fig. 5 with least fixpoints $\mu\alpha\varphi$ and with approximated fixpoints $\mu^t\alpha\varphi$ and $\nu^t\alpha\varphi$ where $t$ is an iteration term. The additional formation rule for formulae are given in Fig. 9. We use $\theta$ as a generic notation for $\mu$ and $\nu$. Least fixpoints $\mu\alpha\varphi$ are equipped with their usual Kozen axioms. In addition, iteration formulae $\nu^t\alpha\varphi(\alpha)$ and $\mu^t\alpha\varphi(\alpha)$ have axioms expressing that they are indeed iterations of $\varphi(\alpha)$ from resp. $\vdash$ and $\perp$. A fixpoint logic with iteration variables was already considered in [63].

**Definition 6.2 (Full Modal Theories).** The full intuitionistic and classical modal theories (still denoted $\vdash^A$ and $\vdash_c^A$) are defined by extending Def. 4.4 with the axioms and rules of Fig. 10.

*Example 6.3.* Least fixpoints allow us to define liveness properties. On streams and colists, we have $\diamond\varphi := \mu\alpha$. $\varphi \vee \Box\alpha$ and $\varphi \cup \psi := \mu\alpha$. $\psi \vee (\varphi \wedge \Box\alpha)$. On trees, we have the CTL-like $\exists\diamond\varphi := \mu\alpha$. $\varphi \vee (\Box\ell\alpha \vee \Box r\alpha)$ and $\forall\diamond\varphi := \mu\alpha$. $\varphi \vee (\Box\ell\alpha \wedge \Box r\alpha)$. The formula $\exists\diamond\varphi$ is intended to hold on a tree if there is a finite path which leads to a subtree satisfying $\varphi$, while $\forall\diamond\varphi$ is intended to hold if every infinite path crosses a subtree satisfying $\varphi$.

*Remark 6.4.* On finitary trees (as in Ex. 6.1 but with $A_i$, $B_i$ finite base types), we have all formulae of the modal $\mu$-calculus. For this fragment, satisfiability is decidable (see e.g. [16]), as well as the classical theory $\vdash_c$ by completeness of Kozen's axiomatization [68] (see [58] for completeness results on fragments of the $\mu$-calculus).

**The Safe and Smooth Fragments.** We now discuss two related but distinct fragments of the temporal modal logic. Both fragments directly impact the refinement type system by allowing for more typing rules.

The safe fragment plays a crucial role, because it reconciles the internal and external semantics of our system (see §7). It gives subtyping rules for ■ (Fig. 11), which makes available the comonad structure of ■ on $[\boxtimes]\varphi$ when $\varphi$ is safe.

**Definition 6.5 (Safe Formula).** Say $\alpha_1 : A_1, \dots, A_n : A_n \vdash \varphi : A$ is safe if

(i) the types $A_1, \dots, A_n$, $A$ are strictly positive, and

(ii) for each occurrence in $\varphi$ of a modality $[ev(\psi)]$, the formula $\psi$ is closed, and

(iii) each occurrence in $\varphi$ of a least fixpoint ($\mu\alpha(-)$) and of an implication ($\Rightarrow$) is guarded by a $[box]$.

Note that the safe restriction imposes no condition on approximated fixpoints $\theta^t\alpha$. Recalling that the theory under a $[box]$ is $\vdash_c^A$, the only propositional connectives accessible to $\vdash^A$ in safe formulae are those on which $\vdash^A$ and $\vdash_c^A$ coincide. The formula $[\neg nil] = [fold][in_1]\vdash$ is safe. Moreover:

*Example 6.6.* Any formula without fixpoint nor $[ev(-)]$ is equivalent in $\vdash_c$ to a safe one. It $\varphi$ is safe, then so are $[hd]\varphi$, $[lbl]\varphi$, as well as $\Delta\varphi$ (for $\Delta \in \{\Box, \forall\Box, \exists\Box\}$) and $[box]\Delta\varphi$ (for $\Delta \in \{\diamond, \exists\diamond, \forall\diamond\}$).
**Definition 6.7 (Smooth Formula).** A formula $\alpha_1 : A_1, \dots, \alpha_n : A_n \vdash \varphi : A$ is smooth if

(i) the types $A_1, \dots, A_n, A$ are finitary strictly positive, and

(ii) for each occurrence in $\varphi$ of a modality $[ev(\psi)]$, the formula $\psi$ is closed, and

(iii) $\varphi$ is alternation-free: for $\theta, \theta' \in \{\mu, \nu\}$, (1) if $\theta\beta_0\psi_0$ is a subformula of $\varphi$, and $\theta'\beta_1\psi_1$ is a subformula of $\psi_0$ s.t. $\beta_0$ occurs free in $\psi_1$, then $\theta = \theta'$, (2) if some $\alpha_i$ occurs in two subformulae $\theta\beta_0\psi_0$ and $\theta'\beta_1\psi_1$ of $\varphi$, then $\theta = \theta'$, and (3) if some $\alpha_i$ occurs in a subformula $\theta'\beta\psi$ of $\varphi$, then $\alpha_i$ Pos $\psi$.

Our notion of alternation freedom is adapted from [16], in which propositional (fixpoint) variables are always positive. Note that the smooth restriction imposes no further conditions on approximated fixpoints $\theta^t\alpha$. In the smooth fragment, greatest and least fixpoints can be thought about resp. as

$$ \bigwedge_{m \in \mathbb{N}} \varphi^m(\top) \quad \text{and} \quad \bigvee_{m \in \mathbb{N}} \varphi^m(\bot) $$

Iteration terms allow for formal reasoning about such unfoldings. Assuming $[[\top]] = m \in \mathbb{N}$, the formula $\nu^t\alpha\varphi(\alpha)$ (resp. $\mu^t\alpha\varphi(\alpha)$) can be read as $\varphi^m(\top)$ (resp. $\varphi^m(\bot)$). This gives the rules $(\nu-I)$ and $(\mu-E)$ (Fig. 11), which allow for reductions to the safe case (see examples in §8).

**Remark 6.8.** It is well-known (see e.g. [16, §4.1]) that on finitary trees (see Rem. 6.4) the alternation-free fragment is equivalent to Weak MSO (MSO with second-order variables restricted to finite sets). In the case of streams Str B (for a finite base type B), Weak MSO is in turn equivalent to the full modal $\mu$-calculus. In particular, the alternation-free fragment contains all the flat fixpoints of [58] and thus LTL on Str B and CTL on Tree B and on Res B with I, O, B finite base types. A typical property on Tree B which cannot be expressed with alternation-free formulae is “there is an infinite path with infinitely many occurrences of b” for a fixed b : B (see e.g. [16, §2.2]).

**Example 6.9.** Any formula without fixpoint nor $[ev(-)]$ is smooth. It $\varphi$ is smooth, then so are $[hd]\varphi$, $[lbl]\varphi$ and $\Delta\varphi$ for $\Delta \in \{\Box, \forall\Box, \exists\Box, \Diamond, \exists\Diamond, \forall\Diamond\}$.

**The Full System.** We extend the types of §5 with universal quantification over iteration variables $(\forall k \cdot T)$. The type system of §5 is extended with the rules of Fig. 11.

**Example 6.10.** The logical rules of Fig. 10 give the following derived typing rules (where $\beta$ Pos $\gamma$):

$$ (\mu\text{-}I) \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\mu^t\alpha\varphi/\beta]\}}{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\mu\alpha\varphi/\beta]\}} \quad (\nu\text{-}E) \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu\alpha\varphi/\beta]\}}{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu^t\alpha\varphi/\beta]\}} $$
**Definition 6.7 (Smooth Formula).** A formula $\alpha_1 : A_1, \dots, \alpha_n : A_n \vdash \varphi : A$ is smooth if

(i) the types $A_1, \dots, A_n, A$ are finitary strictly positive, and

(ii) for each occurrence in $\varphi$ of a modality $[ev(\psi)]$, the formula $\psi$ is closed, and

(iii) $\varphi$ is alternation-free: for $\theta, \theta' \in \{\mu, \nu\}$, (1) if $\theta\beta_0\psi_0$ is a subformula of $\varphi$, and $\theta'\beta_1\psi_1$ is a subformula of $\psi_0$ s.t. $\beta_0$ occurs free in $\psi_1$, then $\theta = \theta'$, (2) if some $\alpha_i$ occurs in two subformulae $\theta\beta_0\psi_0$ and $\theta'\beta_1\psi_1$ of $\varphi$, then $\theta = \theta'$, and (3) if some $\alpha_i$ occurs in a subformula $\theta'\beta\psi$ of $\varphi$, then $\alpha_i$ Pos $\psi$.

Our notion of alternation freedom is adapted from [16], in which propositional (fixpoint) variables are always positive. Note that the smooth restriction imposes no further conditions on approximated fixpoints $\theta^t\alpha$. In the smooth fragment, greatest and least fixpoints can be thought about resp. as

$$ \bigwedge_{m \in \mathbb{N}} \varphi^m(\top) \quad \text{and} \quad \bigvee_{m \in \mathbb{N}} \varphi^m(\bot) $$

Iteration terms allow for formal reasoning about such unfoldings. Assuming $[[\top]] = m \in \mathbb{N}$, the formula $\nu^t\alpha\varphi(\alpha)$ (resp. $\mu^t\alpha\varphi(\alpha)$) can be read as $\varphi^m(\top)$ (resp. $\varphi^m(\bot)$). This gives the rules $(\nu-I)$ and $(\mu-E)$ (Fig. 11), which allow for reductions to the safe case (see examples in §8).

**Remark 6.8.** It is well-known (see e.g. [16, §4.1]) that on finitary trees (see Rem. 6.4) the alternation-free fragment is equivalent to Weak MSO (MSO with second-order variables restricted to finite sets). In the case of streams Str B (for a finite base type B), Weak MSO is in turn equivalent to the full modal $\mu$-calculus. In particular, the alternation-free fragment contains all the flat fixpoints of [58] and thus LTL on Str B and CTL on Tree B and on Res B with I, O, B finite base types. A typical property on Tree B which cannot be expressed with alternation-free formulae is “there is an infinite path with infinitely many occurrences of b” for a fixed b : B (see e.g. [16, §2.2]).

**Example 6.9.** Any formula without fixpoint nor $[ev(-)]$ is smooth. It $\varphi$ is smooth, then so are $[hd]\varphi$, $[lbl]\varphi$ and $\Delta\varphi$ for $\Delta \in \{\Box, \forall\Box, \exists\Box, \Diamond, \exists\Diamond, \forall\Diamond\}$.

**The Full System.** We extend the types of §5 with universal quantification over iteration variables $(\forall k \cdot T)$. The type system of §5 is extended with the rules of Fig. 11.

**Example 6.10.** The logical rules of Fig. 10 give the following derived typing rules (where $\beta$ Pos $\gamma$):

$$ (\mu-I) \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\mu^t \alpha \varphi / \beta]\}}{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\mu \alpha \varphi / \beta]\}} \quad (\nu-E) \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu \alpha \varphi / \beta]\}}{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu^t \alpha \varphi / \beta]\}} $$
$$
\begin{array}{ccc}
\frac{}{\{\Box A \mid [\text{box}]\varphi\} \equiv \{\Box A \mid \varphi\}} & \frac{}{\forall k \cdot \text{▶} T \equiv \text{▶} \forall k \cdot T} & \\
(\forall\text{-I}) \quad \frac{\mathcal{E} \vdash M : T}{\mathcal{E} \vdash M : \forall k \cdot T} & (\forall\text{-CI}) \quad \frac{\mathcal{E} \vdash M : T[0/k]}{\mathcal{E} \vdash M : \forall k \cdot T} & \\
(\nu\text{-I}) \quad \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu^\ell \alpha\psi/\beta]\}}{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu\alpha\psi/\beta]\}} & (\forall\text{-E}) \quad \frac{\mathcal{E} \vdash M : \forall k \cdot T}{\mathcal{E} \vdash M : T[t/k]} & \\
(\mu\text{-E}) \quad \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\mu\alpha\psi/\beta]\}}{\mathcal{E} \vdash N[M/x] : U} & \mathcal{E}, x : \{\Box A \mid [\text{box}]\gamma[\mu^\ell \alpha\psi/\beta]\} \vdash N : U &
\end{array}
$$

<caption>**Fig. 11.** Extended (Sub)Typing Rules for Refinement Types (where $k$ is not free in $\mathcal{E}$ in $(\forall\text{-I})$ & $(\forall\text{-CI})$, $\ell$ is fresh in $(\nu\text{-I})$ & $(\mu\text{-E})$, $\theta\alpha\psi$ and $\gamma$ are smooth, and $\beta$ Pos $\gamma$).</caption>

# 7 Semantics

We present the main ingredients of the semantics of our type system. We take as base the denotational semantics of guarded recursion in the topos of trees.

**Denotational Semantics in the Topos of Trees.** The topos of trees $\mathcal{S}$ provides a natural model of guarded recursion [13]. Formally, $\mathcal{S}$ is the category of presheaves over $(\mathbb{N} \setminus \{0\}, \leq)$. In words, the objects of $\mathcal{S}$ are indexed sets $X = (X(n))_{n>0}$ equipped with restriction maps $r_n^X : X(n+1) \to X(n)$. Excluding $0$ from the indexes is a customary notational convenience ([13]). The morphisms from $X$ to $Y$ are families of functions $f = (f_n : X(n) \to Y(n))_{n>0}$ which commute with restriction, that is $f_n \circ r_n^X = r_n^Y \circ f_{n+1}$. As any presheaf category, $\mathcal{S}$ has (pointwise) limits and colimits, and is Cartesian closed (see e.g. [47, §I.6]). We write $\Gamma : \mathcal{S} \to \text{Set}$ for the global section functor, which takes $X$ to $\mathcal{S}[1, X]$, the set of morphisms $1 \to X$ in $\mathcal{S}$, where $1 = (\{\bullet\})_{n>0}$ is terminal in $\mathcal{S}$. A typed term $\mathcal{E} \vdash M : T$ is to be interpreted in $\mathcal{S}$ as a morphism

$$ [[M]] : [[|\mathcal{E}|]] \to [[|T|]] $$

where $[[|\mathcal{E}|]] = [[|T_1|]] \times \dots \times [[|T_n|]]$ for $\mathcal{E} = x_1 : T_1, \dots, x_n : T_n$. In particular, a closed term $M : T$ is to be interpreted as a global section $[[M]] \in \Gamma([T])$. The $\times/+/\to$ fragment of the calculus is interpreted by the corresponding structure in $\mathcal{S}$. The $\text{▶}$ modality is interpreted by the functor $\text{▶} : \mathcal{S} \to \mathcal{S}$ of [13]. This functor shifts indexes by 1 and inserts a singleton set **1** at index 1. The term constructor next is interpreted by the natural map with component $\text{next}^X : X \to \text{▶}X$ as in

<figure><img src="image_9.png" /></figure>
$$
\begin{array}{ccc}
& \varphi \text{ safe} & \\
\{\Box A \mid [\text{box}]\varphi\} \equiv \{\Box \{A \mid \varphi\}\} & \overline{\forall k \cdot \text{▶} T \equiv \text{▶} \forall k \cdot T} & \\
(\forall\text{-I}) \quad \frac{\mathcal{E} \vdash M : T}{\mathcal{E} \vdash M : \forall k \cdot T} & (\forall\text{-CI}) \quad \frac{\mathcal{E} \vdash M : T[0/k]}{\mathcal{E} \vdash M : \forall k \cdot T} & \\
(\nu\text{-I}) \quad \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu^\ell \alpha \psi / \beta]\}}{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\nu \alpha \psi / \beta]\}} & (\forall\text{-E}) \quad \frac{\mathcal{E} \vdash M : \forall k \cdot T}{\mathcal{E} \vdash M : T[t/k]} & \\
(\mu\text{-E}) \quad \frac{\mathcal{E} \vdash M : \{\Box A \mid [\text{box}]\gamma[\mu \alpha \psi / \beta]\}}{\mathcal{E} \vdash N[M/x] : U} & \mathcal{x} : \{\Box A \mid [\text{box}]\gamma[\mu^\ell \alpha \psi / \beta]\} \vdash N : U &
\end{array}
$$

**Fig. 11.** Extended (Sub)Typing Rules for Refinement Types (where $k$ is not free in $\mathcal{E}$ in $(\forall\text{-I})$ & $(\forall\text{-CI})$, $\ell$ is fresh in $(\nu\text{-I})$ & $(\mu\text{-E})$, $\theta\alpha\psi$ and $\gamma$ are smooth, and $\beta$ Pos $\gamma$).

# 7 Semantics

We present the main ingredients of the semantics of our type system. We take as base the denotational semantics of guarded recursion in the topos of trees.

**Denotational Semantics in the Topos of Trees.** The topos of trees $S$ provides a natural model of guarded recursion [13]. Formally, $S$ is the category of presheaves over $(\mathbb{N} \setminus \{0\}, \leq)$. In words, the objects of $S$ are indexed sets $X = (X(n))_{n>0}$ equipped with restriction maps $r_n^X : X(n+1) \to X(n)$. Excluding $0$ from the indexes is a customary notational convenience ([13]). The morphisms from $X$ to $Y$ are families of functions $f = (f_n : X(n) \to Y(n))_{n>0}$ which commute with restriction, that is $f_n \circ r_n^X = r_n^Y \circ f_{n+1}$. As any presheaf category, $S$ has (pointwise) limits and colimits, and is Cartesian closed (see e.g. [47, §I.6]). We write $\Gamma : S \to \text{Set}$ for the global section functor, which takes $X$ to $S[1, X]$, the set of morphisms $1 \to X$ in $S$, where $1 = (\{\bullet\})_{n>0}$ is terminal in $S$. A typed term $\mathcal{E} \vdash M : T$ is to be interpreted in $S$ as a morphism

$$ [[M]] : [[|\mathcal{E}|]] \to [[|T|]] $$

where $[[|\mathcal{E}|]] = [[|T_1|]] \times \dots \times [[|T_n|]]$ for $\mathcal{E} = x_1 : T_1, \dots, x_n : T_n$. In particular, a closed term $M : T$ is to be interpreted as a global section $[[M]] \in \Gamma([T])$. The $\times/+/\to$ fragment of the calculus is interpreted by the corresponding structure in $S$. The $\text{▶}$ modality is interpreted by the functor $\text{▶} : S \to S$ of [13]. This functor shifts indexes by 1 and inserts a singleton set **1** at index 1. The term constructor next is interpreted by the natural map with component $\text{next}^X : X \to \text{▶}X$ as in

<figure><img src="image_9.png" /></figure>
$$
\begin{align*}
\{[\pi_i]\varphi\} &:= \{x \in \Gamma[[A_0 \times A_1]] \mid \pi_i \circ x \in \{\varphi\}\} & \{[\text{next}]\varphi\} &:= \{\text{next} \circ x \in \Gamma^{\text{tr}}[\text{A}] \mid x \in \{\varphi\}\} \\
\{[\text{fold}]\varphi\} &:= \{x \in \Gamma[[\text{Fix}(X).A]] \mid \text{unfold} \circ x \in \{\varphi\}\} & \{[\text{box}]\varphi\} &:= \{x \in \Gamma[[\Box A]] \mid x_1(\bullet) \in \{\varphi\}\} \\
\{[\text{in}_i]\varphi\} &:= \{x \in \Gamma[[A_0 + A_i]] \mid \exists y \in \Gamma[[A_i]](x = \text{in}_i \circ y \text{ and } y \in \{\varphi\})\} \\
\{[\text{ev}(\psi)]\varphi\} &:= \{x \in \Gamma[[B \to A]] \mid \forall y \in \Gamma[[B]](y \in \{\psi\} \implies \text{ev} \circ (x, y) \in \{\varphi\})\}
\end{align*}
$$

<caption>**Fig. 12.** External Semantics (for closed formulae).</caption>

The guarded fixpoint combinator fix is interpreted by the morphism fix<sup>X</sup> : X<sup>▶</sup><sup>X</sup> → X of [13, Thm. 2.4].

The constant type modality ■ is interpreted as the comonad **ΔΓ**: S → S,
where the left adjoint **Δ**: Set → S is the constant object functor, which takes a
set S to the constant family (S)_{n>0}. In words, all components ■[A](n) are equal
to Γ[A], and the restriction maps of ■[A] are identities. In particular, a global
section x ∈ Γ[■A] is a constant family (x_n)_n describing a unique global section
x_{n+1}(•) = x_n(•) ∈ Γ[A]. We refer to [18] and [28, §D] for the interpretation of
prev, box and unbox. Just note that the unit η : Id<sub>Set</sub> → ΓΔ is an iso.

Together with an interpretation of guarded recursive types, this gives a deno-
tational semantics of the pure calculus of §3. See [13,18] for details. We write fold :
[A[Fix(X).A/X]] → [Fix(X).A] and unfold : [Fix(X).A] → [A[Fix(X).A/X]] for
the two components of the iso [Fix(X).A] ≃ [A[Fix(X).A/X]].

**External Semantics.** Møgelberg [50] has shown that for polynomial types such as $\text{Str}^g B$ with $B$ a constant type, the set of global sections $\Gamma[[\text{Str}^g B]]$ is equipped with the usual final coalgebra structure of streams over $B$ in Set. To each polynomial recursive type $\text{Fix}(X).P(X)$, we associate a polynomial functor $P_{\text{Set}}: \text{Set} \to \text{Set}$ in the obvious way.

**Theorem 7.1 ([50] (see also [18]))**. If $\text{Fix}(X).P(X)$ is polynomial, then the set $\Gamma[[\text{Fix}(X).P(X)]]$ carries a final Set-coalgebra structure for $P_{\text{Set}}$.

We devise a **Set** interpretation {$|\varphi| \in \mathcal{P}(\Gamma[[A]])$} of formulae $\varphi : A$. We rely on the (complete) Boolean algebra structure of powersets for propositional connectives and on Knaster-Tarski Fixpoint Theorem for fixpoints $\mu$ and $\nu$. The interpretations of $\nu^t \alpha \varphi(\alpha)$ and $\mu^t \alpha \varphi(\alpha)$ (for t closed) are defined to be the interpretations resp. of $\varphi^{[t]}(\top)$ and $\varphi^{[t]}(\bot)$, where e.g. $\varphi^0(\top) := \top$ and $\varphi^{n+1}(\top) := \varphi(\varphi^n(\top))$. We give the cases of the atomic modalities in Fig. 12 (where for simplicity we assume formulae to be closed). It can be checked that, when restricting to polynomial types, one gets the coalgebraic semantics of [30] (with sums as in [31]) extended to fixpoints.

**Internal Semantics of Formulae.** We would like to have adequacy w.r.t. the external semantics of formulae, namely that given $M: \{A | \varphi\}$, the global section $[[M]] \in \Gamma[[A]]$ satisfies $\{|\varphi|\} \in \mathcal{P}(\Gamma[[A]])$ in the sense that $[[M]] \in \{|\varphi|\}$. But in general we can only have adequacy w.r.t. an internal semantics $[[\varphi]] \in \text{Sub}([A])$
$$
\begin{align*}
\{\llbracket \pi_i \rbracket \varphi \} &:= \{x \in \Gamma \llbracket A_0 \times A_1 \rrbracket \mid \pi_i \circ x \in \{\varphi\} \} &
\{\llbracket \text{next} \rbracket \varphi \} &:= \{\text{next} \circ x \in \Gamma \llbracket \text{\texttt{\textbf{\textit{A}}}} \rrbracket \mid x \in \{\varphi\} \} \\
\{\llbracket \text{fold} \rbracket \varphi \} &:= \{x \in \Gamma \llbracket \text{Fix}(X).A \rrbracket \mid \text{unfold} \circ x \in \{\varphi\} \} &
\{\llbracket \text{box} \rbracket \varphi \} &:= \{x \in \Gamma \llbracket \text{\texttt{\textbf{\textit{A}}}} \rrbracket \mid x_1(\bullet) \in \{\varphi\} \} \\
\{\llbracket \text{in}_i \rbracket \varphi \} &:= \{x \in \Gamma \llbracket A_0 + A_1 \rrbracket \mid \exists y \in \Gamma \llbracket A_i \rrbracket (x = \text{in}_i \circ y \text{ and } y \in \{\varphi\}) \} \\
\{\llbracket \text{ev}(\psi) \rbracket \varphi \} &:= \{x \in \Gamma \llbracket B \to A \rrbracket \mid \forall y \in \Gamma \llbracket B \rrbracket (y \in \{\psi\} \implies \text{ev} \circ (x, y) \in \{\varphi\}) \}
\end{align*}
$$

<caption>**Fig. 12.** External Semantics (for closed formulae).</caption>

The guarded fixpoint combinator fix is interpreted by the morphism fix<sup>X</sup> : X<sup>▶</sup><sup>X</sup> → X of [13, Thm. 2.4].

The constant type modality ■ is interpreted as the comonad **ΔΓ**: S → S, where the left adjoint **Δ**: Set → S is the constant object functor, which takes a set S to the constant family (S)<sub>n>0</sub>. In words, all components ■[■A](n) are equal to Γ[■A], and the restriction maps of ■[■A] are identities. In particular, a global section x ∈ Γ[■A] is a constant family (x<sub>n</sub>)<sub>n</sub> describing a unique global section x<sub>n+1</sub>(•) = x<sub>n</sub>(•) ∈ Γ[■A]. We refer to [18] and [28, §D] for the interpretation of prev, box and unbox. Just note that the unit η : Id<sub>Set</sub> → Γ**Δ** is an iso.

Together with an interpretation of guarded recursive types, this gives a denotational semantics of the pure calculus of §3. See [13,18] for details. We write fold : ■[A[Fix(X).A/X]] → ■[Fix(X).A] and unfold : ■[Fix(X).A] → ■[A[Fix(X).A/X]] for the two components of the iso ■[Fix(X).A] ≃ ■[A[Fix(X).A/X]].

**External Semantics.** Møgelberg [50] has shown that for polynomial types such as Str<sup>g</sup> B with B a constant type, the set of global sections Γ[Str<sup>g</sup> B] is equipped with the usual final coalgebra structure of streams over B in Set. To each polynomial recursive type Fix(X).P(X), we associate a polynomial functor P<sub>Set</sub>: Set → Set in the obvious way.

**Theorem 7.1 ([50] (see also [18]))**. If Fix(X).P(X) is polynomial, then the set Γ[Fix(X).P(X)] carries a final Set-coalgebra structure for P<sub>Set</sub>.

We devise a **Set** interpretation {|ϕ} ∈ P(Γ[■A]) of formulae ϕ : A. We rely on the (complete) Boolean algebra structure of powersets for propositional connectives and on Knaster-Tarski Fixpoint Theorem for fixpoints μ and ν. The interpretations of ν<sup>t</sup>αϕ(α) and μ<sup>t</sup>αϕ(α) (for t closed) are defined to be the interpretations resp. of ϕ<sup>[t]</sup>(⊤) and ϕ<sup>[t]</sup>(⊥), where e.g. ϕ<sup>0</sup>(⊤) := ⊤ and ϕ<sup>n+1</sup>(⊤) := ϕ(ϕ<sup>n</sup>(⊤)). We give the cases of the atomic modalities in Fig. 12 (where for simplicity we assume formulae to be closed). It can be checked that, when restricting to polynomial types, one gets the coalgebraic semantics of [30] (with sums as in [31]) extended to fixpoints.

**Internal Semantics of Formulae.** We would like to have adequacy w.r.t. the external semantics of formulae, namely that given M : {A | ϕ}, the global section [[M]] ∈ Γ[■A] satisfies {|ϕ} ∈ P(Γ[■A]) in the sense that [[M]] ∈ {|ϕ}. But in general we can only have adequacy w.r.t. an internal semantics [[ϕ]] ∈ Sub([■A])
of formulae $\varphi : A$. We sketch it here. First, Sub($X$) is the (complete) Heyting algebra of subobjects of an object $X$ of $\mathcal{S}$. Explicitly, we have $S = (S(n))_n \in \text{Sub}(X)$ iff for all $n > 0$, $S(n) \subseteq X(n)$ and $r_n^X(t) \in S(n)$ whenever $t \in S(n+1)$. For propositional connectives and fixpoints, the internal $\llbracket - \rrbracket$ is defined similarly as the external $\{|-|\}$, but using (complete) Heyting algebras of subobjects rather than (complete) Boolean algebras of subsets.

As for modalities, let $[\triangle]$ be of the form $[\pi_i]$, $[in_i]$, $[next]$ or $[fold]$, and assume $[\triangle]\varphi : B$ whenever $\varphi : A$. Standard topos theoretic constructions give posets morphisms $\llbracket[\triangle]\rrbracket : \text{Sub}(\llbracket A \rrbracket) \to \text{Sub}(\llbracket B \rrbracket)$ such that $\llbracket\pi_i\rrbracket$, $\llbracket[fold]\rrbracket$ are maps of Heyting algebras, $\llbracket in_i \rrbracket$ preserves $\lor, \bot$ and $\wedge$, while $\llbracket next \rrbracket$ preserves $\wedge, \top$ and $\lor$. With $\llbracket[\triangle]\varphi\rrbracket := \llbracket[\triangle]\rrbracket(\llbracket\varphi\rrbracket)$, all the axioms and rules of Table 2 are validated for these modalities. To handle guarded recursion, it is crucial to have $\llbracket[\text{next}]\varphi\rrbracket := \text{▶}(\llbracket\varphi\rrbracket)$, with $\llbracket[\text{next}]\varphi\rrbracket$ true at time 1, independently from $\varphi$. As a consequence, $[\text{next}]$ and $\bigcirc$ do not validate axiom (P) (Table 2), and $\diamond[\text{hd}]\varphi$ can "lie" about the next time step. We let $\llbracket[\text{box}]\varphi\rrbracket := \Delta(\{|\varphi|\})$.

The modality $[\text{ev}(\psi)]$ is a bit more complex. For $\psi : B$ and $\varphi : A$, the formula $[\text{ev}(\psi)]\varphi$ is interpreted as a *logical predicate* in the sense of [29, §9.2 & Prop. 9.2.4]. The idea is that for a term $M : \{B \to A \mid [\text{ev}(\psi)]\varphi\}$, the global section $\text{ev} \circ \langle\llbracket M \rrbracket, x\rangle \in \Gamma\llbracket A \rrbracket$ should satisfy $\varphi$ whenever $x \in \Gamma\llbracket B \rrbracket$ satisfies $\psi$. We refer to [28, §D] for details.

Our semantics are both correct w.r.t. the full modal theories of Def. 6.2.

**Lemma 7.2.** If $\vdash_C^A \varphi$ then $\{|\varphi|\} = \{|\top|\}$. If $\vdash^A \varphi$ then $\llbracket\varphi\rrbracket = \llbracket\top\rrbracket$.

**The Safe Fragment.** For $\alpha$ (positive and) guarded in $\varphi$, the internal semantics of $\theta\alpha\varphi$ is somewhat meaningless because $\mathcal{S}$ has unique guarded fixpoints [13, §2.5]. In particular, the typing fix($s$).Cons$^g a s : \{\text{Str}^g A \mid \diamond[\varphi]\}$ for arbitrary $a : A$ and $\varphi : \text{Str}^g A$ (extending §2) is indeed verified by the $\mathcal{S}$ semantics $\llbracket-\rrbracket$. This prevents us from adequacy w.r.t. the external semantics in general. But this is possible for *safe* formulae since in this case we have:

**Proposition 7.3.** If $\varphi : A$ is safe then $\{|\varphi|\} = \Gamma\llbracket\varphi\rrbracket$.

Proposition 7.3 gives the subtyping rule $\{\blacksquare A \mid [\text{box}]\varphi\} \equiv \blacksquare \{A \mid \varphi\}$ (Fig. 11), which makes available the comonad structure of $\blacksquare$ on $[\text{box}]\varphi$ when $\varphi$ is safe. Recall that in safe formulae, implications can only occur under a $[\text{box}]$ modality and thus in *closed* subformulae. It is crucial for Prop. 7.3 that infs and sups are pointwise in the subobject lattices of $\mathcal{S}$, so that conjunctions and disjunctions are interpreted as with the usual classical Kripke semantics (see e.g. [47, §VI.7]). This does not hold for implications!

The second key to Prop. 7.3 is the following. For $L$ a complete lattice, a Scott cocontinuous function $L \to L$ is a Scott continuous function $L^{\text{op}} \to L^{\text{op}}$, i.e. which preserves codirected infs. For a safe $\alpha : A \vdash \varphi : A$, the poset maps $\llbracket\varphi\rrbracket : \text{Sub}(\llbracket A \rrbracket) \to \text{Sub}(\llbracket A \rrbracket)$ and $\{|\varphi|\} : \mathcal{P}(\Gamma\llbracket A \rrbracket) \to \mathcal{P}(\Gamma\llbracket A \rrbracket)$ are Scott cocontinuous. The greatest fixpoint $\nu\alpha\varphi(\alpha)$ can thus be interpreted, both in *Set* and $\mathcal{S}$, using Kleene's Fixpoint Theorem, as the infs of the interpretations of $\varphi^m(\top)$ for $m \in \mathbb{N}$. This leads to the expected coincidence of the two semantics for safe formulae.
of formulae $\varphi : A$. We sketch it here. First, Sub($X$) is the (complete) Heyting algebra of subobjects of an object $X$ of $\mathcal{S}$. Explicitly, we have $S = (S(n))_n \in \text{Sub}(X)$ iff for all $n > 0$, $S(n) \subseteq X(n)$ and $r_n^X(t) \in S(n)$ whenever $t \in S(n+1)$. For propositional connectives and fixpoints, the internal $\llbracket - \rrbracket$ is defined similarly as the external $\{|-|\}$, but using (complete) Heyting algebras of subobjects rather than (complete) Boolean algebras of subsets.

As for modalities, let $[\triangle]$ be of the form $[\pi_i]$, $[\text{in}_i]$, $[\text{next}]$ or $[\text{fold}]$, and assume $[\triangle]\varphi : B$ whenever $\varphi : A$. Standard topos theoretic constructions give posets morphisms $\llbracket[\triangle]\rrbracket : \text{Sub}(\llbracket A \rrbracket) \to \text{Sub}(\llbracket B \rrbracket)$ such that $\llbracket \pi_i \rrbracket$, $\llbracket \text{fold} \rrbracket$ are maps of Heyting algebras, $\llbracket \text{in}_i \rrbracket$ preserves $\lor, \bot$ and $\wedge$, while $\llbracket \text{next} \rrbracket$ preserves $\wedge, \top$ and $\lor$. With $\llbracket [\triangle]\varphi \rrbracket := \llbracket [\triangle] \rrbracket(\llbracket \varphi \rrbracket)$, all the axioms and rules of Table 2 are validated for these modalities. To handle guarded recursion, it is crucial to have $\llbracket \text{next} \varphi \rrbracket := \text{▶}(\llbracket \varphi \rrbracket)$, with $\llbracket \text{next} \varphi \rrbracket$ true at time 1, independently from $\varphi$. As a consequence, $[\text{next}]$ and $\bigcirc$ do not validate axiom (P) (Table 2), and $\diamond[\text{hd}]\varphi$ can "lie" about the next time step. We let $\llbracket [\text{box}]\varphi \rrbracket := \Delta(\{|\varphi|\})$.

The modality $[\text{ev}(\psi)]$ is a bit more complex. For $\psi : B$ and $\varphi : A$, the formula $[\text{ev}(\psi)]\varphi$ is interpreted as a *logical predicate* in the sense of [29, §9.2 & Prop. 9.2.4]. The idea is that for a term $M : \{B \to A \mid [\text{ev}(\psi)]\varphi\}$, the global section $\text{ev} \circ \langle\llbracket M \rrbracket, x\rangle \in \Gamma\llbracket A \rrbracket$ should satisfy $\varphi$ whenever $x \in \Gamma\llbracket B \rrbracket$ satisfies $\psi$. We refer to [28, §D] for details.

Our semantics are both correct w.r.t. the full modal theories of Def. 6.2.

**Lemma 7.2.** If $\vdash_C^A \varphi$ then $\{|\varphi|\} = \{|\top|\}$. If $\vdash^A \varphi$ then $\llbracket \varphi \rrbracket = \llbracket \top \rrbracket$.

**The Safe Fragment.** For $\alpha$ (positive and) guarded in $\varphi$, the internal semantics of $\theta\alpha\varphi$ is somewhat meaningless because $\mathcal{S}$ has unique guarded fixpoints [13, §2.5]. In particular, the typing fix($s$).Cons$^g a s : \{\text{Str}^g A \mid \diamond[\varphi]\}$ for arbitrary $a : A$ and $\varphi : \text{Str}^g A$ (extending §2) is indeed verified by the $\mathcal{S}$ semantics $\llbracket - \rrbracket$. This prevents us from adequacy w.r.t. the external semantics in general. But this is possible for *safe* formulae since in this case we have:

**Proposition 7.3.** If $\varphi : A$ is safe then $\{|\varphi|\} = \Gamma\llbracket \varphi \rrbracket$.

Proposition 7.3 gives the subtyping rule $\{\blacksquare A \mid [\text{box}]\varphi\} \equiv \{\blacksquare A \mid \varphi\}$ (Fig. 11), which makes available the comonad structure of $\blacksquare$ on $[\text{box}]\varphi$ when $\varphi$ is safe. Recall that in safe formulae, implications can only occur under a $[\text{box}]$ modality and thus in *closed* subformulae. It is crucial for Prop. 7.3 that infs and sups are pointwise in the subobject lattices of $\mathcal{S}$, so that conjunctions and disjunctions are interpreted as with the usual classical Kripke semantics (see e.g. [47, §VI.7]). This does not hold for implications!

The second key to Prop. 7.3 is the following. For $L$ a complete lattice, a Scott cocontinuous function $L \to L$ is a Scott continuous function $L^{\text{op}} \to L^{\text{op}}$, i.e. which preserves codirected infs. For a safe $\alpha : A \vdash \varphi : A$, the poset maps $\llbracket \varphi \rrbracket : \text{Sub}(\llbracket A \rrbracket) \to \text{Sub}(\llbracket A \rrbracket)$ and $\{|\varphi|\} : \mathcal{P}(\Gamma\llbracket A \rrbracket) \to \mathcal{P}(\Gamma\llbracket A \rrbracket)$ are Scott cocontinuous. The greatest fixpoint $\nu\alpha\varphi(\alpha)$ can thus be interpreted, both in *Set* and $\mathcal{S}$, using Kleene's Fixpoint Theorem, as the infs of the interpretations of $\varphi^m(\top)$ for $m \in \mathbb{N}$. This leads to the expected coincidence of the two semantics for safe formulae.
<figure><img src="image_10.png" /><figcaption>Fig. 13. The Realizability Semantics.</figcaption></figure>

**The Smooth Fragment.** The smooth restriction allows for continuity properties needed to compute fixpoints iteratively, following Kleene's Fixpoint Theorem. This implies the correctness of the typing rules ($\nu$-I) and ($\mu$-E) of Fig. 11.

**Lemma 7.4.** Given a closed smooth $\nu\alpha\varphi(\alpha) : A$ (resp. $\mu\alpha\varphi(\alpha) : A$), the function $\{|\varphi|\} : \mathcal{P}(\Gamma[\!\!\Gamma[A]]) \to \mathcal{P}(\Gamma[\!\!\Gamma[A]])$ is Scott-cocontinuous (resp. Scott-continuous). We have $\{|\nu\alpha\varphi(\alpha)|\} = \bigcap_{m \in \mathbb{N}} \{|\varphi^m(\top)|\}$ (resp. $\{|\mu\alpha\varphi(\alpha)|\} = \bigcup_{m \in \mathbb{N}} \{|\varphi^m(\bot)|\}$).

**The Realizability Semantics.** The correctness of the type system w.r.t. its semantics in $S$ is proved with a realizability relation.

**Definition 7.5 (Realizability).** Given a type $T$ without free iteration variable, a global section $x \in \Gamma[\!\!\Gamma[T]]$ and $n > 0$, we define the realizability relation $x \Vdash_n T$ by induction on lexicographicaly ordered pairs $(n, T)$ in Fig. 13.

**Lemma 7.6.** Given types $T, U$ without free iteration variable, if $x \Vdash_n U$ and $U \le T$ then $x \Vdash_n T$.

**Theorem 7.7 (Adequacy).** If $\vdash M : T$, where $T$ has no free iteration variable, then $[M] \Vdash_n T$ for all $n > 0$.

By Thm. 7.7, a program $M : B \to A$ induces a set-theoretic function $\Gamma[\!\!\Gamma[M]] : \Gamma[\!\!\Gamma[B]] \to \Gamma[\!\!\Gamma[A]]$, $x \mapsto [M] \circ x$. When $B$ and $A$ are polynomial (e.g. streams $\text{Str}^g B$, $\text{Str}^g A$ with $B, A$ constant), Møgelberg's Thm. 7.1 says that $\Gamma[\!\!\Gamma[M]]$ is a function on the usual final coalgebra for $B$, $A$ in **Set** (e.g. the set of usual streams over $B$ and $A$). Moreover, if e.g. $M : \{\text{Str } B \mid [\text{box}]\psi\} \to \{\text{Str } A \mid [\text{box}]\varphi\}$, then (modulo $\Gamma\Delta \simeq \text{Id}_\text{Set}$) given a stream $x$ that satisfies $\psi$ (i.e. $x \in \{|\psi|\}$) the stream $\Gamma[\!\!\Gamma[M]](x)$ satisfies $\varphi$ (i.e. $\Gamma[\!\!\Gamma[M]](x) \in \{|\varphi|\}$). See §8 for examples.

# 8 Examples

We exemplified basic manipulations of our system over §3-6. We give further examples here. The functions used in our main examples are gathered in Table 3, with the following conventions. We use the infix notation $a ::^g s$ for $\text{Cons}^g a$ and $s$ and write $[]^g$ for the empty colist $\text{Nil}^g$. Moreover, we use some syntactic sugar for pattern matching, e.g. assuming $s : \text{CoList}^g A$ we write case $s$ of ($[]^g \mapsto N|x ::^g xs \mapsto M$) for case(unfold $s$) of ($y.N[\langle\rangle/y]|y.M[\pi_0(y)/x, \pi_1(y)/xs]$). Most of the
<figure><img src="image_10.png" /><figcaption>Fig. 13. The Realizability Semantics.</figcaption></figure>

**The Smooth Fragment.** The smooth restriction allows for continuity properties needed to compute fixpoints iteratively, following Kleene's Fixpoint Theorem. This implies the correctness of the typing rules ($\nu$-I) and ($\mu$-E) of Fig. 11.

**Lemma 7.4.** Given a closed smooth $\nu\alpha\varphi(\alpha) : A$ (resp. $\mu\alpha\varphi(\alpha) : A$), the function $\{|\varphi|\} : \mathcal{P}(\Gamma[\!\!\Gamma[A]]) \to \mathcal{P}(\Gamma[\!\!\Gamma[A]])$ is Scott-cocontinuous (resp. Scott-continuous). We have $\{|\nu\alpha\varphi(\alpha)|\} = \bigcap_{m \in \mathbb{N}} \{|\varphi^m(\top)|\}$ (resp. $\{|\mu\alpha\varphi(\alpha)|\} = \bigcup_{m \in \mathbb{N}} \{|\varphi^m(\bot)|\}$).

**The Realizability Semantics.** The correctness of the type system w.r.t. its semantics in $S$ is proved with a realizability relation.

**Definition 7.5 (Realizability).** Given a type $T$ without free iteration variable, a global section $x \in \Gamma[\!\!\Gamma[T]]$ and $n > 0$, we define the realizability relation $x \Vdash_n T$ by induction on lexicographicaly ordered pairs $(n, T)$ in Fig. 13.

**Lemma 7.6.** Given types $T, U$ without free iteration variable, if $x \Vdash_n U$ and $U \le T$ then $x \Vdash_n T$.

**Theorem 7.7 (Adequacy).** If $\Gamma \vdash M : T$, where $T$ has no free iteration variable, then $\Gamma[\!\!\Gamma[M]] \Vdash_n T$ for all $n > 0$.

By Thm. 7.7, a program $M : B \to A$ induces a set-theoretic function $\Gamma[\!\!\Gamma[M]] : \Gamma[\!\!\Gamma[B]] \to \Gamma[\!\!\Gamma[A]]$, $x \mapsto [M] \circ x$. When $B$ and $A$ are polynomial (e.g. streams $\text{Str}^g B$, $\text{Str}^g A$ with $B, A$ constant), Møgelberg's Thm. 7.1 says that $\Gamma[\!\!\Gamma[M]]$ is a function on the usual final coalgebra for $B$, $A$ in **Set** (e.g. the set of usual streams over $B$ and $A$). Moreover, if e.g. $M : \{\text{Str } B \mid [\text{box}]\psi\} \to \{\text{Str } A \mid [\text{box}]\varphi\}$, then (modulo $\Gamma\Delta \simeq \text{Id}_\text{Set}$) given a stream $x$ that satisfies $\psi$ (i.e. $x \in \{|\psi|\}$) the stream $\Gamma[\!\!\Gamma[M]](x)$ satisfies $\varphi$ (i.e. $\Gamma[\!\!\Gamma[M]](x) \in \{|\varphi|\}$). See §8 for examples.

## 8 Examples

We exemplified basic manipulations of our system over §3-6. We give further examples here. The functions used in our main examples are gathered in Table 3, with the following conventions. We use the infix notation $a ::^g s$ for $\text{Cons}^g a$ and $s$ and write $\llbracket g \rrbracket$ for the empty colist $\text{Nil}^g$. Moreover, we use some syntactic sugar for pattern matching, e.g. assuming $s : \text{CoList}^g A$ we write case $s$ of ($\llbracket g \rrbracket \mapsto N|x ::^g xs \mapsto M$) for case(unfold $s$) of $(y.N[\langle\rangle/y] | y.M[\pi_0(y)/x, \pi_1(y)/xs])$. Most of the
<table><caption>**Table 3.** Code of the Examples.</caption>
  <tbody>
    <tr>
      <td>
        <b>append</b> : CoList<sup>g</sup> A → CoList<sup>g</sup> A → CoList<sup>g</sup> A<br>
        &nbsp;&nbsp;:= λs.λt.<br>
        &nbsp;&nbsp;&nbsp;&nbsp;box<sub>l</sub>(append<sup>g</sup> (unbox s) (unbox t))
      </td>
      <td>
        <b>sched</b> : Res<sup>g</sup> A → Res<sup>g</sup> A → Res<sup>g</sup> A<br>
        &nbsp;&nbsp;:= λp.λq.<br>
        &nbsp;&nbsp;&nbsp;&nbsp;box<sub>l</sub>(sched<sup>g</sup> (unbox p) (unbox q))
      </td>
    </tr>
    <tr>
      <td>
        <b>append<sup>g</sup></b> : CoList<sup>g</sup> A → CoList<sup>g</sup> A → CoList<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λs.λt. case s of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;[]<sup>g</sup> ↦→ t<br>
        &nbsp;&nbsp;&nbsp;&nbsp;x ::= g xs ↦→ x ::= g (g ⊗ xs ⊗ (next t))
      </td>
      <td>
        <b>sched<sup>g</sup></b> : Res<sup>g</sup> A → Res<sup>g</sup> A → Res<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λp.λq. case p of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;Ret<sup>g</sup> a ↦→ Ret<sup>g</sup> a<br>
        &nbsp;&nbsp;&nbsp;&nbsp;Cont<sup>g</sup> k ↦→<br>
        &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;let h = λi. let ⟨o, t⟩ = ki<br>
        &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in ⟨o, g ⊗ (next q) ⊗ t⟩<br>
        &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in Cont<sup>g</sup> h
      </td>
    </tr>
    <tr>
      <td>
        <b>diag</b> := λs.box<sub>l</sub>(diag<sup>g</sup> (unbox s)) : Str(Str A) → Str A<br>
        <b>diag<sup>g</sup></b> := diagaux<sup>g</sup> (λx.x) : Str<sup>g</sup>(Str A) → Str<sup>g</sup> A<br>
        <b>diagaux<sup>g</sup></b> : (Str A → Str A) → Str<sup>g</sup>(Str A) → Str<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λt.λs. Cons<sup>g</sup> ((hd ◦ t)(hd<sup>g</sup> s)) (g ⊗ next(t ◦ tl) ⊗ (tl<sup>g</sup> s))
      </td>
      <td></td>
    </tr>
    <tr>
      <td>
        <b>fb</b> : CoNat → CoNat → Str Bool<br>
        &nbsp;&nbsp;:= λc.λm. box<sub>l</sub>(fb<sup>g</sup> (unbox c) (unbox m))
      </td>
      <td>
        <b>fb<sup>g</sup></b> : CoNat<sup>g</sup> → CoNat<sup>g</sup> → Str<sup>g</sup> Bool<br>
        &nbsp;&nbsp;:= fix(g).λc.λm. case c of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Z<sup>g</sup> ↦→ ff ::= g ⊗ (next m) ⊗ next(S<sup>g</sup> (next m))<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| S<sup>g</sup>n ↦→ tt ::= g ⊗ n ⊗ (next m)
      </td>
    </tr>
    <tr>
      <td>
        <b>extract</b> : Rou<sup>g</sup>(CoList<sup>g</sup> A) → CoList<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λc. case c of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Over<sup>g</sup> ↦→ Nil<sup>g</sup><br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Cont<sup>g</sup> f ↦→ fg<sup>⊗</sup>
      </td>
      <td>
        <b>unfold</b> : Rou<sup>g</sup> A → (▶ Rou<sup>g</sup> A → ▶A) → ▶A<br>
        &nbsp;&nbsp;:= λc. case c of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Over<sup>g</sup> ↦→ λk. k (next Over<sup>g</sup>)<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Cont<sup>g</sup> f ↦→ λk. next(fk)
      </td>
    </tr>
    <tr>
      <td>
        <b>bft<sup>g</sup></b> := λt. extract (bftaux t Over<sup>g</sup>) : Tree<sup>g</sup> A → CoList<sup>g</sup> A<br>
        <b>bftaux</b> : Tree<sup>g</sup> A → Rou<sup>g</sup>(CoList<sup>g</sup> A) → Rou<sup>g</sup>(CoList<sup>g</sup> A)<br>
        &nbsp;&nbsp;:= fix(g).λt.λc. Cont (λk. (label<sup>g</sup> t) ::= g) unfold c (k ◦ (g ⊗ (son<sup>g</sup><sub>l</sub>t))) ◦ (g ⊗ (son<sup>g</sup><sub>r</sub>t)))
      </td>
      <td></td>
    </tr>
  </tbody>
</table>

functions of Table 3 are obtained from usual recursive definitions by inserting ⊗ and next at the right places. We often write $\psi \| \to \varphi$ for $[\mathrm{ev}(\psi)]\varphi$. Table 4 recaps our main examples of refinement typings, all of which (for A, B, 0, I constant, I finite and $\varphi$, $\psi$ safe and smooth) can be derived syntactically for the functions of Table 3. We use intermediate typings requiring iteration terms whenever a ◇ is involved. Below, "$\Gamma[[M]]$ satisfies $\varphi$" means $\Gamma[[M]] \in \{\lvert\varphi\rvert\}$ (modulo $\Gamma\Delta \simeq \mathrm{Id}_{\mathrm{Set}}$, see §7). We refer to [28, §E] for details.

**Example 8.1 (The Append Function on CoLists).** Our system can derive that $\Gamma[[append]]$ returns a non-empty colist if one of its argument is non-empty. Using $\diamondnil$ (which says that a colist is finite), we can derive that $\Gamma[[append]]$ returns a finite colist if its arguments are both finite. This involves the intermediate typing

$$ \forall k. \forall \ell. (\{\text{CoList}^g A \mid \diamond^k \text{[nil]}\} \to \{\text{CoList}^g A \mid \diamond^\ell \text{[nil]}\} \to \{\text{CoList}^g A \mid \diamond^{k+\ell} \text{[nil]}\}) $$

In addition, if the first argument of $\Gamma[[append]]$ has an element which satisfies $\varphi$, then the result has an element which satisfies $\varphi$. The same holds if the first argument is finite while the second one has an element which satisfies $\varphi$ [28, §E.6]. □
<table><caption>**Table 3.** Code of the Examples.</caption>
  <tbody>
    <tr>
      <td>
        <b>append</b> : CoList<sup>g</sup> A → CoList<sup>g</sup> A → CoList<sup>g</sup> A<br>
        &nbsp;&nbsp;:= λs.λt.<br>
        &nbsp;&nbsp;&nbsp;&nbsp;box<sub>l</sub>(append<sup>g</sup> (unbox s) (unbox t))
      </td>
      <td>
        <b>sched</b> : Res<sup>g</sup> A → Res<sup>g</sup> A → Res<sup>g</sup> A<br>
        &nbsp;&nbsp;:= λp.λq.<br>
        &nbsp;&nbsp;&nbsp;&nbsp;box<sub>l</sub>(sched<sup>g</sup> (unbox p) (unbox q))
      </td>
    </tr>
    <tr>
      <td>
        <b>append<sup>g</sup></b> : CoList<sup>g</sup> A → CoList<sup>g</sup> A → CoList<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λs.λt. case s of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;[]<sup>g</sup> ↦→ t<br>
        &nbsp;&nbsp;&nbsp;&nbsp;x ::= xs ↦→ x ::= g (g ⊗ xs ⊗ (next t))
      </td>
      <td>
        <b>sched<sup>g</sup></b> : Res<sup>g</sup> A → Res<sup>g</sup> A → Res<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λp.λq. case p of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;Ret<sup>g</sup> a ↦→ Ret<sup>g</sup> a<br>
        &nbsp;&nbsp;&nbsp;&nbsp;Cont<sup>g</sup> k ↦→<br>
        &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;let h = λi. let ⟨o, t⟩ = ki<br>
        &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in ⟨o, g ⊗ (next q) ⊗ t⟩<br>
        &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;in Cont<sup>g</sup> h
      </td>
    </tr>
    <tr>
      <td>
        <b>diag</b> := λs.box<sub>l</sub>(diag<sup>g</sup> (unbox s)) : Str(Str A) → Str A<br>
        <b>diag<sup>g</sup></b> := diagaux<sup>g</sup> (λx.x) : Str<sup>g</sup>(Str A) → Str<sup>g</sup> A<br>
        <b>diagaux<sup>g</sup></b> : (Str A → Str A) → Str<sup>g</sup>(Str A) → Str<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λt.λs. Cons<sup>g</sup> ((hd ◦ t)(hd<sup>g</sup> s)) (g ⊗ next(t ◦ tl) ⊗ (tl<sup>g</sup> s))
      </td>
      <td></td>
    </tr>
    <tr>
      <td>
        <b>fb</b> : CoNat → CoNat → Str Bool<br>
        &nbsp;&nbsp;:= λc.λm. box<sub>l</sub>(fb<sup>g</sup> (unbox c) (unbox m))
      </td>
      <td>
        <b>fb<sup>g</sup></b> : CoNat<sup>g</sup> → CoNat<sup>g</sup> → Str<sup>g</sup> Bool<br>
        &nbsp;&nbsp;:= fix(g).λc.λm. case c of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Z<sup>g</sup> ↦→ ff ::= g ⊗ (next m) ⊗ next(S<sup>g</sup> (next m))<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| S<sup>g</sup>n ↦→ tt ::= g ⊗ n ⊗ (next m)
      </td>
    </tr>
    <tr>
      <td>
        <b>extract</b> : Rou<sup>g</sup>(CoList<sup>g</sup> A) → CoList<sup>g</sup> A<br>
        &nbsp;&nbsp;:= fix(g).λc. case c of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Over<sup>g</sup> ↦→ Nil<sup>g</sup><br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Cont<sup>g</sup> f ↦→ fg<sup>⊗</sup>
      </td>
      <td>
        <b>unfold</b> : Rou<sup>g</sup> A → (▶ Rou<sup>g</sup> A → ▶A) → ▶A<br>
        &nbsp;&nbsp;:= λc. case c of<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Over<sup>g</sup> ↦→ λk. k (next Over<sup>g</sup>)<br>
        &nbsp;&nbsp;&nbsp;&nbsp;| Cont<sup>g</sup> f ↦→ λk. next(fk)
      </td>
    </tr>
    <tr>
      <td>
        <b>bft<sup>g</sup></b> := λt. extract (bftaux t Over<sup>g</sup>) : Tree<sup>g</sup> A → CoList<sup>g</sup> A<br>
        <b>bftaux</b> : Tree<sup>g</sup> A → Rou<sup>g</sup>(CoList<sup>g</sup> A) → Rou<sup>g</sup>(CoList<sup>g</sup> A)<br>
        &nbsp;&nbsp;:= fix(g).λt.λc. Cont (λk. (label<sup>g</sup> t) ::= g<sup>g</sup> unfold c (k ◦ (g ⊗ (son<sup>g</sup><sub>l</sub>t)))<sup>⊗</sup> ◦ (g ⊗ (son<sup>g</sup><sub>r</sub>t)))<sup>⊗</sup>)
      </td>
      <td></td>
    </tr>
  </tbody>
</table>

functions of Table 3 are obtained from usual recursive definitions by inserting ⊗ and next at the right places. We often write $\psi \| \to \varphi$ for $[\text{ev}(\psi)]\varphi$. Table 4 recaps our main examples of refinement typings, all of which (for A, B, 0, I constant, I finite and $\varphi$, $\psi$ safe and smooth) can be derived syntactically for the functions of Table 3. We use intermediate typings requiring iteration terms whenever a ◇ is involved. Below, "$\Gamma[[M]]$ satisfies $\varphi$" means $\Gamma[[M]] \in \{\vert\varphi\vert\}$ (modulo $\Gamma\Delta \simeq \text{Id}_{\text{Set}}$, see §7). We refer to [28, §E] for details.

**Example 8.1 (The Append Function on CoLists).** Our system can derive that $\Gamma[[append]]$ returns a non-empty colist if one of its argument is non-empty. Using $\diamondnil$ (which says that a colist is finite), we can derive that $\Gamma[[append]]$ returns a finite colist if its arguments are both finite. This involves the intermediate typing

$$ \forall k. \forall \ell. (\{\text{CoList}^g A \mid \diamond^k \text{[nil]}\} \to \{\text{CoList}^g A \mid \diamond^\ell \text{[nil]}\} \to \{\text{CoList}^g A \mid \diamond^{k+\ell} \text{[nil]}\}) $$

In addition, if the first argument of $\Gamma[[append]]$ has an element which satisfies $\varphi$, then the result has an element which satisfies $\varphi$. The same holds if the first argument is finite while the second one has an element which satisfies $\varphi$ [28, §E.6]. □
**Map over coinductive streams** (with △ either □, ◇, ◇□ or □◇)

map : ({B | ψ} → {A | ϕ}) → {Str B | [box]△[hd]ψ} → {Str A | [box]△[hd]ϕ}

**Diagonal of coinductive streams of streams** (with △ either □ or ◇□)

diag : {Str(Str A) | [box]△[hd][box]□[hd]ϕ} → {Str A | [box]△[hd]ϕ}

**A fair stream of Booleans** (adapted from [17,8])

fb : CoNat → CoNat → Str Bool

fb 0 1 : {Str Bool | [box]◇□[hd][tt] ∧ [box]◇□[hd][ff]}

**Append on guarded recursive colists**

append<sup>g</sup> : {CoList<sup>g</sup> A | [¬nil]} → CoList<sup>g</sup> A → {CoList<sup>g</sup> A | [¬nil]}

append<sup>g</sup> : CoList<sup>g</sup> A → {CoList<sup>g</sup> A | [¬nil]} → {CoList<sup>g</sup> A | [¬nil]}

**Append on coinductive colists**

append : {CoList A | [box]◇[hd]ϕ} → CoList A → {CoList A | [box]◇[hd]ϕ}

append : {CoList A | [box]◇[nil]} → {CoList A | [box]◇[hd]ϕ} → {CoList A | [box]◇[hd]ϕ}

append : {CoList A | [box]◇[nil]} → {CoList A | [box]◇[nil]} → {CoList A | [box]◇[nil]}

**Breadth-first tree traversal**

bft<sup>g</sup> : {Tree<sup>g</sup> C | ∀□[lbl]ϑ} → {CoList<sup>g</sup> C | □[hd]ϑ}

(à la [35] or with Hofmann's algorithm (see e.g. [10]))

**A scheduler of resumptions** (adapted from [44])

sched : {Res A | [box]◇[Ret]} → {Res A | [box]◇[Ret]} → {Res A | [box]◇[Ret]}

sched : {Res A | [box]◇[now]ψ} → {Res A | [box]◇[now]ψ} → {Res A | [box]◇[now]ψ}

sched : {Res A | [box]□◇[Ret]} → {Res A | [box]□◇[Ret]} → {Res A | [box]□◇[Ret]}

sched : {Res A | [box]□◇[out]ϑ} → {Res A | [box]□◇[out]ϑ} → {Res A | [box]□◇[out]ϑ}

(where ◇ is either ∀◇ or ∃◇, □ is either ∀□ or ∃□, and [out] is either [∧out] or [√out])

<caption>**Table 4.** Some Refinement Typings (functions defined in Table 3).</caption>

**Example 8.2 (The Map Function on Streams).** The composite modalities □◇ and ◇□ over streams are read resp. as “infinitely often” and “eventually always”. Provided with a function $f : \mathcal{I}[B] \to \mathcal{I}[A]$ taking $b \in \mathcal{I}[B]$ satisfying $\psi$ to $f(b) \in \mathcal{I}[B]$ satisfying $\varphi$, the function $\mathcal{I}[\text{map}]$ on set-theoretic streams returns a stream which infinitely often (resp. eventually always) satisfies $\varphi$ if its stream argument infinitely often (resp. eventually always) satisfies $\psi$ [28, §E.3]. □

**Example 8.3 (The Diagonal Function).** Consider a stream of streams $s$. We have $s = (s_i | i \ge 0)$ where each $s_i$ is itself a stream $s_i = (s_{i,j} | j \ge 0)$. The diagonal of $s$ is then the stream $(s_{i,i} | i \ge 0)$. Note that $s_{i,i} = \text{hd}(\text{tl}^i(\text{hd}(\text{tl}^i(s))))$. Indeed, $\text{tl}^i(s)$ is the stream of streams $(s_k | k \ge i)$, so that $\text{hd}(\text{tl}^i(s))$ is the stream $s_i$ and $\text{tl}^i(\text{hd}(\text{tl}^i(s)))$ is the stream $(s_{i,k} | k \ge i)$. Taking its head thus gives $s_{i,i}$. In the diag function of Table 3, the auxiliary higher-order function diagaux<sup>g</sup> iterates the coinductive tl over the head of the stream of streams $s$. We write ◦ for function composition, so that assuming $s : \text{Str}^g(\text{Str A})$ and $t : \text{Str A} \to \text{Str A}$, we have (on the coinductive type Str A), $(\text{hd}^g s) : \text{Str A}$ and

$(\text{hd} \circ t) : \text{Str A} \to A \quad (\text{hd} \circ t)(\text{hd}^g s) : A \quad (t \circ \text{tl}) : \text{Str A} \to \text{Str A}$

The expected refinement types for diag (Table 4) say that if its argument is a stream whose component streams all satisfy □ϕ, then $\mathcal{I}[\text{diag}]$ returns a stream
**Map over coinductive streams** (with △ either □, ◇, ◇◇ or ◇◇)

map : ({B | ψ} → {A | ϕ}) → {Str B | [box]△[hd]ψ} → {Str A | [box]△[hd]ϕ}

**Diagonal of coinductive streams of streams** (with △ either □ or ◇◇)

diag : {Str(Str A) | [box]△[hd][box]□[hd]ϕ} → {Str A | [box]△[hd]ϕ}

**A fair stream of Booleans** (adapted from [17,8])

fb : CoNat → CoNat → Str Bool

fb 0 1 : {Str Bool | [box]◇◇[hd][tt] ∧ [box]◇◇[hd][ff]}

**Append on guarded recursive colists**

append<sup>g</sup> : {CoList<sup>g</sup> A | [¬nil]} → CoList<sup>g</sup> A → {CoList<sup>g</sup> A | [¬nil]}

append<sup>g</sup> : CoList<sup>g</sup> A → {CoList<sup>g</sup> A | [¬nil]} → {CoList<sup>g</sup> A | [¬nil]}

**Append on coinductive colists**

append : {CoList A | [box]◇[hd]ϕ} → CoList A → {CoList A | [box]◇[hd]ϕ}

append : {CoList A | [box]◇[nil]} → {CoList A | [box]◇[hd]ϕ} → {CoList A | [box]◇[hd]ϕ}

append : {CoList A | [box]◇[nil]} → {CoList A | [box]◇[nil]} → {CoList A | [box]◇[nil]}

**Breadth-first tree traversal**

bft<sup>g</sup> : {Tree<sup>g</sup> C | ∀□[lbl]ϑ} → {CoList<sup>g</sup> C | □[hd]ϑ}

(à la [35] or with Hofmann's algorithm (see e.g. [10]))

**A scheduler of resumptions** (adapted from [44])

sched : {Res A | [box]◇[Ret]} → {Res A | [box]◇[Ret]} → {Res A | [box]◇[Ret]}

sched : {Res A | [box]◇[now]ψ} → {Res A | [box]◇[now]ψ} → {Res A | [box]◇[now]ψ}

sched : {Res A | [box]◇◇[Ret]} → {Res A | [box]◇◇[Ret]} → {Res A | [box]◇◇[Ret]}

sched : {Res A | [box]◇◇[out]ϑ} → {Res A | [box]◇◇[out]ϑ} → {Res A | [box]◇◇[out]ϑ}

(where ◇ is either ∀◇ or ∃◇, □ is either ∀□ or ∃□, and [out] is either [∧out] or [√out])

<caption>**Table 4.** Some Refinement Typings (functions defined in Table 3).</caption>

**Example 8.2 (The Map Function on Streams).** The composite modalities □◇ and ◇◇ over streams are read resp. as “infinitely often” and “eventually always”. Provided with a function $f : \mathcal{I}[B] \to \mathcal{I}[A]$ taking $b \in \mathcal{I}[B]$ satisfying $\psi$ to $f(b) \in \mathcal{I}[B]$ satisfying $\varphi$, the function $\mathcal{I}[\text{map}]$ on set-theoretic streams returns a stream which infinitely often (resp. eventually always) satisfies $\varphi$ if its stream argument infinitely often (resp. eventually always) satisfies $\psi$ [28, §E.3]. □

**Example 8.3 (The Diagonal Function).** Consider a stream of streams $s$. We have $s = (s_i | i \ge 0)$ where each $s_i$ is itself a stream $s_i = (s_{i,j} | j \ge 0)$. The diagonal of $s$ is then the stream $(s_{i,i} | i \ge 0)$. Note that $s_{i,i} = \text{hd}(\text{tl}^i(\text{hd}(\text{tl}^i(s))))$. Indeed, $\text{tl}^i(s)$ is the stream of streams $(s_k | k \ge i)$, so that $\text{hd}(\text{tl}^i(s))$ is the stream $s_i$ and $\text{tl}^i(\text{hd}(\text{tl}^i(s)))$ is the stream $(s_{i,k} | k \ge i)$. Taking its head thus gives $s_{i,i}$. In the diag function of Table 3, the auxiliary higher-order function diagaux<sup>g</sup> iterates the coinductive tl over the head of the stream of streams $s$. We write ◦ for function composition, so that assuming $s : \text{Str}^g(\text{Str A})$ and $t : \text{Str A} \to \text{Str A}$, we have (on the coinductive type Str A), $(\text{hd}^g s) : \text{Str A}$ and

$(\text{hd} \circ t) : \text{Str A} \to A \quad (\text{hd} \circ t)(\text{hd}^g s) : A \quad (t \circ \text{tl}) : \text{Str A} \to \text{Str A}$

The expected refinement types for diag (Table 4) say that if its argument is a stream whose component streams all satisfy □ϕ, then $\mathcal{I}[\text{diag}]$ returns a stream
whose elements all satisfy $\varphi$. Also, if the argument of $\mathbf{I}[\mathrm{diag}]$ is a stream such that eventually all its component streams satisfy $\Box\varphi$, then it returns a stream which eventually always satisfies $\varphi$. See [28, §E.4] for details. $\Box$

**Example 8.4 (A Fair Stream of Booleans).** The non-regular stream (fb 0 1), adapted from [17,8], is of the form $\mathit{ff} \cdot \mathit{tt} \cdot \mathit{ff} \cdot \mathit{tt}^2 \cdot \mathit{ff} \dots \mathit{ff} \cdot \mathit{tt}^m \cdot \mathit{ff} \dots$. It thus contains infinitely many $\mathit{tt}$'s and infinitely many $\mathit{ff}$'s. We indeed have (see [28, §E.5] for details) (fb 0 1) : {Str Bool | [box] $\Box\diamond$ [hd][tt] $\wedge$ [box] $\Box\diamond$ [hd][ff]}.

**Example 8.5 (Resumptions).** The type of resumptions $\mathbf{Res}^g A$ (see Ex. 3.2) is adapted from [44]. Its guarded constructors are

$$ \mathrm{Ret}^g := \lambda a. \, \mathrm{fold}(\mathrm{in}_0 a) : A \longrightarrow \mathrm{Res}^g A $$

$$ \mathrm{Cont}^g := \lambda k. \, \mathrm{fold}(\mathrm{in}_1 k) : (I \to (0 \times \mathbf{Res}^g A)) \longrightarrow \mathrm{Res}^g A $$

$\mathrm{Ret}^g(a)$ represents a computation which returns the value $a : A$, while $\mathrm{Cont}^g \langle f, k \rangle$ (with $\langle f, k \rangle : I \to (0 \times \mathbf{Res}^g A)$) represents a computation which on input $i : I$ outputs $fi : 0$ and continues with $ki : \mathbf{Res}^g A$. Given $p, q : \mathbf{Res}^g A$, the scheduler $(\mathbf{sched}^g p q)$, adapted from [44], first evaluates $p$. If $p$ returns, then the whole computation returns, with the same value. Otherwise, $p$ evaluates to say $\mathrm{Cont}^g \langle f, k \rangle$. Then $(\mathbf{sched}^g p q)$ produces a computation which on input $i : I$ outputs $fi$ and continues with $(\mathbf{sched}^g q (ki))$, thus switching arguments.

Let $I$ be a finite base type (so that $\mathbf{Res}^g A$ is finitary polynomial). Let $\psi : A$, $\vartheta : 0$ and $\varphi : \mathbf{Res}^g A$. We have the following formulae (where $i : I$):

$$ \begin{aligned} [\mathrm{Ret}] &:= [\mathrm{fold}][\mathrm{in}_0]^{\top} \\ [\mathrm{now}]\psi &:= [\mathrm{fold}][\mathrm{in}_0]\psi \end{aligned} $$

$$ \begin{aligned} [\mathrm{out}_i]\vartheta &:= [\mathrm{fold}][\mathrm{in}_1] ([i] \dashv\dashv [\pi_0]\vartheta) \\ \bigcirc_i\varphi &:= [\mathrm{fold}][\mathrm{in}_1] ([i] \dashv\dashv [\pi_1][\mathrm{next}]\varphi) \end{aligned} $$

The formula $[\mathrm{Ret}]$ (resp. $[\mathrm{now}]\psi$) holds on a resumption which immediately returns (resp. with a value satisfying $\psi$) and we have $\mathrm{Ret}^g : A \to \{\mathbf{Res}^g A \mid [\mathrm{Ret}]\}$, $\mathrm{Ret}^g : \{A \mid \psi\} \to \{\mathbf{Res}^g A \mid [\mathrm{now}]\psi\}$. Moreover, the typings

$$ \mathrm{Cont}^g : \{I \to (0 \times \mathbf{Res}^g A) \mid [i] \dashv\dashv [\pi_0]\vartheta\} \longrightarrow \{\mathbf{Res}^g A \mid [\mathrm{out}_i]\vartheta\} $$

$$ \mathrm{Cont}^g : \{I \to (0 \times \mathbf{Res}^g A) \mid [i] \dashv\dashv [\pi_1][\mathrm{next}]\varphi\} \longrightarrow \{\mathbf{Res}^g A \mid \bigcirc_i\varphi\} $$

express that $[\mathrm{out}_i]\vartheta : \mathbf{Res}^g A$ is satisfied by $\mathrm{Cont}^g \langle f, k \rangle$ if $fi$ satisfies $\vartheta$, and that $\bigcirc_i\varphi : \mathbf{Res}^g A$ is satisfied by $\mathrm{Cont}^g \langle f, k \rangle$ if $ki$ satisfies $[\mathrm{next}]\varphi$. Since $I$ is a finite base type, it is possible to quantify over its inhabitants. We thus obtain CTL-like variants of $\Box$ and $\diamond$ (Ex. 4.3.(b) and Ex. 6.3). Namely:

$$ [\wedge\mathrm{out}]\vartheta := \wedge_{i \in I}[\mathrm{out}_i]\vartheta : \mathbf{Res}^g A $$

$$ [\vee\mathrm{out}]\vartheta := \vee_{i \in I}[\mathrm{out}_i]\vartheta : \mathbf{Res}^g A $$

$$ \forall \Box\varphi := \nu\alpha. \varphi \wedge \Box\alpha : \mathbf{Res}^g A $$

$$ \exists\Box\varphi := \nu\alpha. \varphi \wedge \Box\alpha : \mathbf{Res}^g A $$

$$ \Box\varphi := \wedge_{i \in I} \bigcirc_i\varphi : \mathbf{Res}^g A $$

$$ \Box\varphi := \vee_{i \in I} \bigcirc_i\varphi : \mathbf{Res}^g \varphi $$

$$ \forall\diamond\varphi := \mu\alpha. \varphi \vee \Box\alpha : \mathbf{Res}^g A $$

$$ \exists\diamond\varphi := \mu\alpha. \varphi \vee \Box\alpha : \mathbf{Res}^g A $$

Our system can prove that $\mathbf{I}[\mathrm{sched}]$ returns in finite time when so do its arguments, either along *some* or along *any* sequence of inputs. We moreover have expected $\Box\diamond$ properties for all possible (consistent) combinations of $\exists/\forall$ and $[\mathrm{Ret}]/[\vee\mathrm{out}]/[\wedge\mathrm{out}]$ (Table 4, with $\psi : A$, $\vartheta : 0$ safe and smooth) [28, §E.7]. $\Box$
whose elements all satisfy $\varphi$. Also, if the argument of $\mathbf{I}[\mathrm{diag}]$ is a stream such that eventually all its component streams satisfy $\Box\varphi$, then it returns a stream which eventually always satisfies $\varphi$. See [28, §E.4] for details. $\Box$

**Example 8.4 (A Fair Stream of Booleans).** The non-regular stream (fb 0 1), adapted from [17,8], is of the form $\mathit{ff} \cdot \mathit{tt} \cdot \mathit{ff} \cdot \mathit{tt}^2 \cdot \mathit{ff} \dots \mathit{ff} \cdot \mathit{tt}^m \cdot \mathit{ff} \dots$. It thus contains infinitely many $\mathit{tt}$'s and infinitely many $\mathit{ff}$'s. We indeed have (see [28, §E.5] for details) (fb 0 1) : {Str Bool | [box] $\Box\diamond$ [hd][tt] $\wedge$ [box] $\Box\diamond$ [hd][ff]}.

**Example 8.5 (Resumptions).** The type of resumptions $\mathbf{Res}^g A$ (see Ex. 3.2) is adapted from [44]. Its guarded constructors are

$$ \mathrm{Ret}^g := \lambda a. \, \mathrm{fold}(\mathrm{in}_0 a) : A \longrightarrow \mathrm{Res}^g A $$

$$ \mathrm{Cont}^g := \lambda k. \, \mathrm{fold}(\mathrm{in}_1 k) : (I \to (0 \times \mathbf{Res}^g A)) \longrightarrow \mathrm{Res}^g A $$

$\mathrm{Ret}^g(a)$ represents a computation which returns the value $a : A$, while $\mathrm{Cont}^g \langle f, k \rangle$ (with $\langle f, k \rangle : I \to (0 \times \mathbf{Res}^g A)$) represents a computation which on input $i : I$ outputs $fi : 0$ and continues with $ki : \mathbf{Res}^g A$. Given $p, q : \mathbf{Res}^g A$, the scheduler $(\mathbf{sched}^g p q)$, adapted from [44], first evaluates $p$. If $p$ returns, then the whole computation returns, with the same value. Otherwise, $p$ evaluates to say $\mathrm{Cont}^g \langle f, k \rangle$. Then $(\mathbf{sched}^g p q)$ produces a computation which on input $i : I$ outputs $fi$ and continues with $(\mathbf{sched}^g q (ki))$, thus switching arguments.

Let $I$ be a finite base type (so that $\mathbf{Res}^g A$ is finitary polynomial). Let $\psi : A$, $\vartheta : 0$ and $\varphi : \mathbf{Res}^g A$. We have the following formulae (where $i : I$):

$$ \begin{align*} [\mathrm{Ret}] &:= [\mathrm{fold}][\mathrm{in}_0]^{\top} \\ [\mathrm{now}]\psi &:= [\mathrm{fold}][\mathrm{in}_0]\psi \end{align*} $$

$$ \begin{align*} [\mathrm{out}_i]\vartheta &:= [\mathrm{fold}][\mathrm{in}_1] ([i] \dashv\dashv [\pi_0]\vartheta) \\ \bigcirc_i \varphi &:= [\mathrm{fold}][\mathrm{in}_1] ([i] \dashv\dashv [\pi_1][\mathrm{next}]\varphi) \end{align*} $$

The formula $[\mathrm{Ret}]$ (resp. $[\mathrm{now}]\psi$) holds on a resumption which immediately returns (resp. with a value satisfying $\psi$) and we have $\mathrm{Ret}^g : A \to \{\mathbf{Res}^g A \mid [\mathrm{Ret}]\}$, $\mathrm{Ret}^g : \{A \mid \psi\} \to \{\mathbf{Res}^g A \mid [\mathrm{now}]\psi\}$. Moreover, the typings

$$ \mathrm{Cont}^g : \{I \to (0 \times \mathbf{Res}^g A) \mid [i] \dashv\dashv [\pi_0]\vartheta\} \longrightarrow \{\mathbf{Res}^g A \mid [\mathrm{out}_i]\vartheta\} $$

$$ \mathrm{Cont}^g : \{I \to (0 \times \mathbf{Res}^g A) \mid [i] \dashv\dashv [\pi_1][\mathrm{next}]\varphi\} \longrightarrow \{\mathbf{Res}^g A \mid \bigcirc_i \varphi\} $$

express that $[\mathrm{out}_i]\vartheta : \mathbf{Res}^g A$ is satisfied by $\mathrm{Cont}^g \langle f, k \rangle$ if $fi$ satisfies $\vartheta$, and that $\bigcirc_i \varphi : \mathbf{Res}^g A$ is satisfied by $\mathrm{Cont}^g \langle f, k \rangle$ if $ki$ satisfies $[\mathrm{next}]\varphi$. Since $I$ is a finite base type, it is possible to quantify over its inhabitants. We thus obtain CTL-like variants of $\Box$ and $\diamond$ (Ex. 4.3.(b) and Ex. 6.3). Namely:

$$ [\wedge\mathrm{out}]\vartheta := \wedge_{i \in I}[\mathrm{out}_i]\vartheta : \mathbf{Res}^g A $$

$$ [\vee\mathrm{out}]\vartheta := \vee_{i \in I}[\mathrm{out}_i]\vartheta : \mathbf{Res}^g A $$

$$ \forall \Box \varphi := \nu \alpha. \, \varphi \wedge \Box \alpha : \mathbf{Res}^g A $$

$$ \exists \Box \varphi := \nu \alpha. \, \varphi \wedge \Box \alpha : \mathbf{Res}^g A $$

$$ \Box \varphi := \wedge_{i \in I} \bigcirc_i \varphi : \mathbf{Res}^g A $$

$$ \Box \varphi := \vee_{i \in I} \bigcirc_i \varphi : \mathbf{Res}^g \varphi $$

$$ \forall \diamond \varphi := \mu \alpha. \, \varphi \vee \Box \alpha : \mathbf{Res}^g A $$

$$ \exists \diamond \varphi := \mu \alpha. \, \varphi \vee \Box \alpha : \mathbf{Res}^g A $$

Our system can prove that $\mathbf{I}[\mathrm{sched}]$ returns in finite time when so do its arguments, either along *some* or along *any* sequence of inputs. We moreover have expected $\Box\diamond$ properties for all possible (consistent) combinations of $\exists/\forall$ and $[\mathrm{Ret}]/[\vee\mathrm{out}]/[\wedge\mathrm{out}]$ (Table 4, with $\psi : A$, $\vartheta : 0$ safe and smooth) [28, §E.7]. $\Box$
*Example 8.6 (Breadth-First Traversal).* The function `bftg` of Table 3 (where $g^\circ$ stands for $\lambda x.g \circledast x$) implements Martin Hofmann's algorithm for breadth-first tree traversal. This algorithm involves the higher-order type `RougA` (see Ex. 3.2) with constructors `Overg := fold(in₀(\cdot))`: `RougA` and

$$Contg := \lambda f. fold(in₁f) : ((\blacktriangleright \text{RougA} \to \blacktriangleright A) \to A) \to \text{RougA}$$

We refer to [10] for explanations. Consider a formula $\varphi: A$. We can lift $\varphi$ to

$$[\text{Rou}]\varphi := \nu\alpha. [\text{fold}][in₁]((\text{[next]}\alpha \rightharpoonup \text{[next]}\varphi) \rightharpoonup \varphi) : \text{RougA}$$

We then easily derive the expected refinement type of `bftg` (Table 4, where $\vartheta: C$). Assume that $\vartheta$ is safe. On the one hand it is not clear what the meaning of $[\text{Rou}]\vartheta$ is, because it is an unsafe formula over a non-polynomial type. On the other hand, the type of `bftg` in Tab. 4 has its standard expected meaning (namely: if all nodes of a tree satisfy $\vartheta$ then so do all elements of its traversal) because the types `TreegC`, `CoListgC` are polynomial and the formulae $\forall \Box[\text{lbl}]\vartheta$, $\Box[\text{hd}]\vartheta$ are safe. Hence, our system can prove standard statements via detours through non-standard ones, which illustrates its compositionality. We have the same typing for a usual breadth-first tree traversal with forests (à la [35]). See [28, §E.8]. □

# 9 Related Work

Type systems based on guarded recursion have been designed to enforce properties of programs handling coinductive types, like causality [45], productivity [5,50,18,6,25,24], or termination [62]. These properties are captured by the type systems, meaning that all well-typed programs satisfy these properties.

In an initially different line of work, temporal logics have been used as type systems for functional reactive programming (FRP), starting from LTL [32,33] to the intuitionistic modal $\mu$-calculus [17]. These works follow the Curry-Howard "proof-as-programs" paradigm, and reflect in the programming languages the constructions of the temporal logic.

The FRP approach has been adapted to guarded recursion, e.g. for the absence of space leaks [44], or the absence of time leaks, with the Fitch-style system of [7]. This more recently led [8] to consider liveness properties with an FRP approach based on guarded recursion. In this system, the guarded $\lambda$-calculus (presented in a Fitch-style type system) is extended with a delay modality (written $\O$) together with a "until type" A Until B. Following the Curry-Howard correspondence, A Until B is eliminated with a specific recursor, based on the usual unfolding of Until in LTL, and distinct from the guarded fixpoint operator.

In these Curry-Howard approaches, temporal operators are wired into the structure of types. This means that there is no separation between the program and the proof that it satisfies a given temporal property. Different type formers having different program constructs, different temporal specifications for the same program may lead to different actual code.

We have chosen a different approach, based on refinement types, with which the structure of formulae is not reflected in the structure of types. This allows
*Example 8.6 (Breadth-First Traversal).* The function `bftg` of Table 3 (where $g^\circ$ stands for $\lambda x.g \circledast x$) implements Martin Hofmann's algorithm for breadth-first tree traversal. This algorithm involves the higher-order type `RougA` (see Ex. 3.2) with constructors `Overg := fold(in₀(\cdot)) : RougA` and

$$Contg := \lambda f. fold(in₁f) : ((\blacktriangleright RougA \to \blacktriangleright A) \to A) \to RougA$$

We refer to [10] for explanations. Consider a formula $\varphi : A$. We can lift $\varphi$ to

$$[Rou]\varphi := \nu\alpha. [fold][in₁]((\lbrack next \rbrack\alpha \rightharpoonup \lbrack next \rbrack\varphi) \rightharpoonup \varphi) : RougA$$

We then easily derive the expected refinement type of `bftg` (Table 4, where $\vartheta : C$). Assume that $\vartheta$ is safe. On the one hand it is not clear what the meaning of $[Rou]\vartheta$ is, because it is an unsafe formula over a non-polynomial type. On the other hand, the type of `bftg` in Tab. 4 has its standard expected meaning (namely: if all nodes of a tree satisfy $\vartheta$ then so do all elements of its traversal) because the types `TreegC`, `CoListgC` are polynomial and the formulae $\forall \Box[\mathit{lbl}]\vartheta$, $\Box[\mathit{hd}]\vartheta$ are safe. Hence, our system can prove standard statements via detours through non-standard ones, which illustrates its compositionality. We have the same typing for a usual breadth-first tree traversal with forests ($\mathit{à la}$ [35]). See [28, §E.8]. $\square$

## 9 Related Work

Type systems based on guarded recursion have been designed to enforce properties of programs handling coinductive types, like causality [45], productivity [5,50,18,6,25,24], or termination [62]. These properties are captured by the type systems, meaning that all well-typed programs satisfy these properties.

In an initially different line of work, temporal logics have been used as type systems for functional reactive programming (FRP), starting from LTL [32,33] to the intuitionistic modal $\mu$-calculus [17]. These works follow the Curry-Howard "proof-as-programs" paradigm, and reflect in the programming languages the constructions of the temporal logic.

The FRP approach has been adapted to guarded recursion, e.g. for the absence of space leaks [44], or the absence of time leaks, with the Fitch-style system of [7]. This more recently lead [8] to consider liveness properties with an FRP approach based on guarded recursion. In this system, the guarded $\lambda$-calculus (presented in a Fitch-style type system) is extended with a delay modality (written $\circ$) together with a "until type" A Until B. Following the Curry-Howard correspondence, A Until B is eliminated with a specific recursor, based on the usual unfolding of Until in LTL, and distinct from the guarded fixpoint operator.

In these Curry-Howard approaches, temporal operators are wired into the structure of types. This means that there is no separation between the program and the proof that it satisfies a given temporal property. Different type formers having different program constructs, different temporal specifications for the same program may lead to different actual code.

We have chosen a different approach, based on refinement types, with which the structure of formulae is not reflected in the structure of types. This allows
for our examples to be mostly written in a usual guarded recursive fashion (see Table 3). Of course, we indeed use the modality `■` at the type level as a separation between safety and liveness properties. But different liveness properties (e.g. `◇`, `◇□`, `□◇`) are uniformly handled with the same `■`-type, which is moreover the expected one in the guarded $\lambda$-calculus [18].

Higher-order model checking (HOMC) [54,39] has been introduced to check automatically that higher-order recursion schemes, a simple form of higher-order programs with *finite* data-types, satisfy a $\mu$-calculus formula. Automatic verification of higher-order programs with infinite data-types (integers) has been explored for safety [40], termination [46], and more generally $\omega$-regular [51] properties. In presence of infinite datatypes, semi-automatic extensions of HOMC have recently been proposed [69]. In contrast with this paper, most HOMC approaches do not consider input-output behaviors on coalgebraic data. A notable exception is [41,23], but it does not handle higher-order functions (such as `map`), nor polynomial types such as `Str(Str A)` (Ex. 8.3) or non-positive types such as `Rou A` (Ex. 8.6) and imposes a strong linearity constraint on pattern matching.

Event-driven approaches consider effects generating streams of events [61], which can be checked for temporal properties with algorithms based on (HO)MC [26,27], or, in presence of infinite datatypes, with refinement type systems [42,53]. Our iteration terms can be seen as oracles, as required by [42] to handle liveness properties, but we do not know if they allow for the non-regular specifications of [53]. While such approaches can handle infinite data types with good levels of automation, they do not have coinductive types nor branching time properties, such as the temporal specification of `sched` on resumptions (Ex. 8.5).

Along similar lines, branching was approached via non-determinism in [64], which also handles universal and existential properties on traces. This framework can handle CTL-like properties of the form $∃/∀□/◇$ (with our notation of Ex. 8.5), but not nested combinations of these (as e.g. $∃□∀◇$ for `sched` in Ex. 8.5). It moreover does not handle coinductive types.

# 10 Conclusion and Future Work

We have presented a refinement type system for the guarded $\lambda$-calculus, with refinements expressing temporal properties stated as (alternation-free) $\mu$-calculus formulae. As we have seen, the system is general enough to prove precise behavioral input/output properties of coinductively-typed programs. Our main contribution is to handle liveness properties in presence of guarded recursive types. As seen in §2, this comes with inherent difficulties. In general, once guarded recursive functions are packed into coinductive ones using `■`, the logical reasoning is made in our system directly on top of programs, following their shape, but requiring no further modification. We thus believe to have achieved some separation between programs and proofs.

We provided several examples. While they demonstrate the flexibility of our system, they also show that more abstraction would be welcomed when proving
for our examples to be mostly written in a usual guarded recursive fashion (see Table 3). Of course, we indeed use the modality `■` at the type level as a separation between safety and liveness properties. But different liveness properties (e.g. `◇`, `◇□`, `□◇`) are uniformly handled with the same `■`-type, which is moreover the expected one in the guarded $\lambda$-calculus [18].

Higher-order model checking (HOMC) [54,39] has been introduced to check automatically that higher-order recursion schemes, a simple form of higher-order programs with *finite* data-types, satisfy a $\mu$-calculus formula. Automatic verification of higher-order programs with infinite data-types (integers) has been explored for safety [40], termination [46], and more generally $\omega$-regular [51] properties. In presence of infinite datatypes, semi-automatic extensions of HOMC have recently been proposed [69]. In contrast with this paper, most HOMC approaches do not consider input-output behaviors on coalgebraic data. A notable exception is [41,23], but it does not handle higher-order functions (such as `map`), nor polynomial types such as `Str(Str A)` (Ex. 8.3) or non-positive types such as `Rou A` (Ex. 8.6) and imposes a strong linearity constraint on pattern matching.

Event-driven approaches consider effects generating streams of events [61], which can be checked for temporal properties with algorithms based on (HO)MC [26,27], or, in presence of infinite datatypes, with refinement type systems [42,53]. Our iteration terms can be seen as oracles, as required by [42] to handle liveness properties, but we do not know if they allow for the non-regular specifications of [53]. While such approaches can handle infinite data types with good levels of automation, they do not have coinductive types nor branching time properties, such as the temporal specification of `sched` on resumptions (Ex. 8.5).

Along similar lines, branching was approached via non-determinism in [64], which also handles universal and existential properties on traces. This framework can handle CTL-like properties of the form $∃/∀□/◇$ (with our notation of Ex. 8.5), but not nested combinations of these (as e.g. $∃□∀◇$ for `sched` in Ex. 8.5). It moreover does not handle coinductive types.

# 10 Conclusion and Future Work

We have presented a refinement type system for the guarded $\lambda$-calculus, with refinements expressing temporal properties stated as (alternation-free) $\mu$-calculus formulae. As we have seen, the system is general enough to prove precise behavioral input/output properties of coinductively-typed programs. Our main contribution is to handle liveness properties in presence of guarded recursive types. As seen in §2, this comes with inherent difficulties. In general, once guarded recursive functions are packed into coinductive ones using `■`, the logical reasoning is made in our system directly on top of programs, following their shape, but requiring no further modification. We thus believe to have achieved some separation between programs and proofs.

We provided several examples. While they demonstrate the flexibility of our system, they also show that more abstraction would be welcomed when proving
liveness properties. In addition, our system lacks expressiveness to prove e.g. liveness properties on breadth-first tree traversals.

We believe that our approach could be generalized to other programming languages with inductive or coinductive types. The key requirement are: (1) modalities in the temporal logic to navigate through the types of the languages, (2) a semantics to indicate when a program satisfies a formula of the temporal logic, which is sufficiently closed to the set-theoretic one for liveness properties to get their expected meaning, and (3) inference rules to reason over this realizability semantics.

Extensions of the guarded λ-calculus with dependent types have been explored [14,11,6,24]. It may be possible to extend our work to these systems. This would require to work in a Fitch-style presentation of the ■ modality, as in [7,12], since it is not known how to extend delayed substitutions to dependent types while retaining decidability of type-checking [15]. Also, it is appealing to investigate the generalization of our approach to sized types [1], in which guarded recursive types are representable [67].

We plan to investigate type checking. For instance, in a decidable fragment like the μ-calculus on streams, one can check that a function of type {Strg C | ◇□[hd]ψ} → {Strg B | ◇□[hd]ψ} can be postcomposed with one of type {Strg B | □◇[hd]ψ} → {Strg A | □◇[hd]φ} (since ◇□[hd]ψ ⇒ □◇[hd]ψ). Hence, we expect that some automation is possible for fragments of our logic. In presence of iteration terms, arithmetic extensions of the μ-calculus [37,38] may provide interesting backends. An other direction is the interaction with HOMC. If (say) a stream over A is representable in a suitable format, one may use HOMC to check whether it can be argument of a function expecting e.g. a stream of type {Strg A | □◇[hd]φ}. This might provide automation for fragments of the guarded λ-calculus. Besides, the combination of refinement types with automatic techniques like predicate abstraction [57], abstract interpretation [34], or SMT solvers [66,65] has been particularly successful. More recently, the combination of refinement types inference with HOMC has been investigated [59].

We would like to explore temporal specification of general, effectful programs. To do so, we wish to develop the treatment of the coinductive resumptions monad [55], that provides a general framework to reason on effectful computations, as shown by interaction trees [70]. It would be interesting to study temporal specifications we could give to effectful programs encoded in this setting. To formalize reasoning on such examples, we would like to design an embedding of our system in a proof assistant like COQ.

Following [3], guarded recursion has been used to abstract the reasoning on step-indexing [4] that has been used to design Kripke Logical Relations [2] for typed higher-order effectful programming languages. Program logics for reasoning on such logical relations [19,20] uses this representation of step-indexing via guarded recursion. It is also found in Iris [36], a framework for higher-order concurrent separation logic. It would be interesting to explore the incorporation of temporal reasoning, especially liveness properties, in such logics.
liveness properties. In addition, our system lacks expressiveness to prove e.g. liveness properties on breadth-first tree traversals.

We believe that our approach could be generalized to other programming languages with inductive or coinductive types. The key requirement are: (1) modalities in the temporal logic to navigate through the types of the languages, (2) a semantics to indicate when a program satisfies a formula of the temporal logic, which is sufficiently closed to the set-theoretic one for liveness properties to get their expected meaning, and (3) inference rules to reason over this realizability semantics.

Extensions of the guarded λ-calculus with dependent types have been explored [14,11,6,24]. It may be possible to extend our work to these systems. This would require to work in a Fitch-style presentation of the ■ modality, as in [7,12], since it is not known how to extend delayed substitutions to dependent types while retaining decidability of type-checking [15]. Also, it is appealing to investigate the generalization of our approach to sized types [1], in which guarded recursive types are representable [67].

We plan to investigate type checking. For instance, in a decidable fragment like the μ-calculus on streams, one can check that a function of type {Strg C | ◇□[hd]ψ} → {Strg B | ◇□[hd]ψ} can be postcomposed with one of type {Strg B | □◇[hd]ψ} → {Strg A | □◇[hd]φ} (since ◇□[hd]ψ ⇒ □◇[hd]ψ). Hence, we expect that some automation is possible for fragments of our logic. In presence of iteration terms, arithmetic extensions of the μ-calculus [37,38] may provide interesting backends. An other direction is the interaction with HOMC. If (say) a stream over A is representable in a suitable format, one may use HOMC to check whether it can be argument of a function expecting e.g. a stream of type {Strg A | □◇[hd]φ}. This might provide automation for fragments of the guarded λ-calculus. Besides, the combination of refinement types with automatic techniques like predicate abstraction [57], abstract interpretation [34], or SMT solvers [66,65] has been particularly successful. More recently, the combination of refinement types inference with HOMC has been investigated [59].

We would like to explore temporal specification of general, effectful programs. To do so, we wish to develop the treatment of the coinductive resumptions monad [55], that provides a general framework to reason on effectful computations, as shown by interaction trees [70]. It would be interesting to study temporal specifications we could give to effectful programs encoded in this setting. To formalize reasoning on such examples, we would like to design an embedding of our system in a proof assistant like COQ.

Following [3], guarded recursion has been used to abstract the reasoning on step-indexing [4] that has been used to design Kripke Logical Relations [2] for typed higher-order effectful programming languages. Program logics for reasoning on such logical relations [19,20] uses this representation of step-indexing via guarded recursion. It is also found in Iris [36], a framework for higher-order concurrent separation logic. It would be interesting to explore the incorporation of temporal reasoning, especially liveness properties, in such logics.
References

1. Abel, A., Pientka, B.: Well-founded recursion with copatterns and sized types. J. Funct. Program. 26, e2 (2016). https://doi.org/10.1017/S0956796816000022, https://doi.org/10.1017/S0956796816000022

2. Ahmed, A.: Step-Indexed Syntactic Logical Relations for Recursive and Quanti-fied Types. In: Proceedings of the 15th European Conference on Programming Languages and Systems. pp. 69–83. ESOP’06, Springer-Verlag, Berlin, Heidelberg (2006). https://doi.org/10.1007/11693024.6, https://doi.org/10.1007/11693024.6

3. Appel, A., Melliès, P.A., Richards, C., Vouillon, J.: A Very Modal Model of a Modern, Major, General Type System. SIGPLAN Not. 42(1), 109–122 (2007). https://doi.org/10.1145/1190215.1190235, https://doi.org/10.1145/1190215.1190235

4. Appel, A.W., McAllester, D.: An Indexed Model of Recursive Types for Founda-tional Proof-Carrying Code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (2001). https://doi.org/10.1145/504709.504712, https://doi.org/10.1145/504709.504712

5. Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: Proceedings of the 18th ACM SIGPLAN International Conference on Func-tional Programming. pp. 197–208. ICFP ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2500365.2500597

6. Bahr, P., Grathwohl, H.B., Møgelberg, R.E.: The Clocks Are Ticking: No More De-lays! In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–12 (2017). https://doi.org/10.1109/LICS.2017.8005097

7. Bahr, P., Graulund, C., Møgelberg, R.: Simply RaTT: A Fitch-Style Modal Calcu-lus for Reactive Programming without Space Leaks. Proc. ACM Program. Lang. 3(ICFP), 109:1–109:27 (2019). https://doi.org/10.1145/3341713

8. Bahr, P., Graulund, C., Møgelberg, R.: Diamonds are not Forever: Liveness in Re-active Programming with Guarded Recursion (2020), https://arxiv.org/abs/2003.03170, To Appear in POPL’21

9. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)

10. Berger, U., Matthes, R., Setzer, A.: Martin Hofmann’s Case for Non-Strictly Positive Data Types. In: Dybjer, P., Espírito Santo, J., Pinto, L. (eds.) 24th International Conference on Types for Proofs and Programs (TYPES 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol. 130, pp. 1:1–1:22. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2019). https://doi.org/10.4230/LIPIcs.TYPES.2018.1, https://hal.archives-ouvertes.fr/hal-02365814

11. Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H.B., Spitters, B., Vezzosi, A.: Guarded cubical type theory. Journal of Automated Reasoning 63(2), 211–253 (2019). https://doi.org/10.1007/s10817-018-9471-7

12. Birkedal, L., Clouston, R., Mannaa, B., Møgelberg, R., Pitts, A.M., Spitters, B.: Modal dependent type theory and dependent right ad-joints. Mathematical Structures in Computer Science 30(2), 118–138 (2020). https://doi.org/10.1017/S0960129519000197

13. Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in syn-thetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8(4) (2012)

14. Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded Dependent Type Theory with Coinductive Types. In: Jacobs, B., Löding, C. (eds.)
References

1. Abel, A., Pientka, B.: Well-founded recursion with copatterns and sized types. J. Funct. Program. 26, e2 (2016). https://doi.org/10.1017/S0956796816000022, https://doi.org/10.1017/S0956796816000022

2. Ahmed, A.: Step-Indexed Syntactic Logical Relations for Recursive and Quanti-fied Types. In: Proceedings of the 15th European Conference on Programming Languages and Systems. pp. 69–83. ESOP’06, Springer-Verlag, Berlin, Heidelberg (2006). https://doi.org/10.1007/11693024.6, https://doi.org/10.1007/11693024.6

3. Appel, A., Melliès, P.A., Richards, C., Vouillon, J.: A Very Modal Model of a Modern, Major, General Type System. SIGPLAN Not. 42(1), 109–122 (2007). https://doi.org/10.1145/1190215.1190235, https://doi.org/10.1145/1190215.1190235

4. Appel, A.W., McAllester, D.: An Indexed Model of Recursive Types for Founda-tional Proof-Carrying Code. ACM Trans. Program. Lang. Syst. 23(5), 657–683 (2001). https://doi.org/10.1145/504709.504712, https://doi.org/10.1145/504709.504712

5. Atkey, R., McBride, C.: Productive coprogramming with guarded recursion. In: Proceedings of the 18th ACM SIGPLAN International Conference on Func-tional Programming. pp. 197–208. ICFP ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2500365.2500597

6. Bahr, P., Grathwohl, H.B., Møgelberg, R.E.: The Clocks Are Ticking: No More De-lays! In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–12 (2017). https://doi.org/10.1109/LICS.2017.8005097

7. Bahr, P., Graulund, C., Møgelberg, R.: Simply RaTT: A Fitch-Style Modal Calcu-lus for Reactive Programming without Space Leaks. Proc. ACM Program. Lang. 3(ICFP), 109:1–109:27 (2019). https://doi.org/10.1145/3341713

8. Bahr, P., Graulund, C., Møgelberg, R.: Diamonds are not Forever: Liveness in Re-active Programming with Guarded Recursion (2020), https://arxiv.org/abs/2003.03170, To Appear in POPL’21

9. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press (2008)

10. Berger, U., Matthes, R., Setzer, A.: Martin Hofmann's Case for Non-Strictly Positive Data Types. In: Dybjer, P., Espírito Santo, J., Pinto, L. (eds.) 24th International Conference on Types for Proofs and Programs (TYPES 2018), Leibniz International Proceedings in Informatics (LIPIcs), vol. 130, pp. 1:1–1:22. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2019). https://doi.org/10.4230/LIPIcs.TYPES.2018.1, https://hal.archives-ouvertes.fr/hal-02365814

11. Birkedal, L., Bizjak, A., Clouston, R., Grathwohl, H.B., Spitters, B., Vezzosi, A.: Guarded cubical type theory. Journal of Automated Reasoning 63(2), 211–253 (2019). https://doi.org/10.1007/s10817-018-9471-7

12. Birkedal, L., Clouston, R., Mannaa, B., Møgelberg, R., Pitts, A.M., Spitters, B.: Modal dependent type theory and dependent right ad-joints. Mathematical Structures in Computer Science 30(2), 118–138 (2020). https://doi.org/10.1017/S0960129519000197

13. Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in syn-thetic guarded domain theory: step-indexing in the topos of trees. Logical Methods in Computer Science 8(4) (2012)

14. Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded Dependent Type Theory with Coinductive Types. In: Jacobs, B., Löding, C. (eds.)
Foundations of Software Science and Computation Structures. pp. 20–35. Springer Berlin Heidelberg, Berlin, Heidelberg (2016)

15. Bizjak, A., Møgelberg, R.E.: Denotational semantics for guarded dependent type theory. Mathematical Structures in Computer Science 30(4), 342–378 (2020). https://doi.org/10.1017/S0960129520000080

16. Bradfield, J.C., Walukiewicz, I.: The mu-calculus and Model Checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 871–919. Springer (2018)

17. Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair Reactive Programming. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 361–372. POPL ’14, ACM, New York, NY, USA (2014)

18. Clouston, R., Bizjak, A., Bugge Grathwohl, H., Birkedal, L.: The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science 12(3) (2016)

19. Dreyer, D., Ahmed, A., Birkedal, L.: Logical Step-Indexed Logical Relations. Logical Methods in Computer Science Volume 7, Issue 2 (2011). https://doi.org/10.2168/LMCS-7(2:16)2011, https://lmcs.episciences.org/698

20. Dreyer, D., Neis, G., Rossberg, A., Birkedal, L.: A Relational Modal Logic for Higher-order Stateful ADTs. In: Proceedings POPL’10. pp. 185–198. ACM (2010)

21. Elliott, C., Hudak, P.: Functional Reactive Animation. In: Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming. pp. 263–273. ICFP’97, ACM, New York, NY, USA (1997). https://doi.org/10.1145/258948.258973, http://doi.acm.org/10.1145/258948.258973

22. Freeman, T., Pfenning, F.: Refinement Types for ML. In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. pp. 268–277. PLDI’91, Association for Computing Machinery, New York, NY, USA (1991). https://doi.org/10.1145/113445.113468, https://doi.org/10.1145/113445.113468

23. Fujima, K., Ito, S., Kobayashi, N.: Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes. In: APLAS ’13: Proceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 8301. pp. 17–32. Springer-Verlag, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-319-03542-0_2, https://doi.org/10.1007/978-3-319-03542-0_2

24. Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 492–506. LICS ’20, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3373718.3394736, https://doi.org/10.1145/3373718.3394736

25. Guatto, A.: A Generalized Modality for Recursion. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 482–491. LICS ’18, ACM, New York, NY, USA (2018). https://doi.org/10.1145/3209108.3209148

26. Hofmann, M., Chen, W.: Abstract interpretation from büchi automata. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014. pp. 51:1–51:10. ACM (2014). https://doi.org/10.1145/2603088.2603127, https://doi.org/10.1145/2603088.2603127
Foundations of Software Science and Computation Structures. pp. 20–35. Springer Berlin Heidelberg, Berlin, Heidelberg (2016)

15. Bizjak, A., Møgelberg, R.E.: Denotational semantics for guarded dependent type theory. Mathematical Structures in Computer Science 30(4), 342–378 (2020). https://doi.org/10.1017/S0960129520000080

16. Bradfield, J.C., Walukiewicz, I.: The mu-calculus and Model Checking. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 871–919. Springer (2018)

17. Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair Reactive Programming. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 361–372. POPL ’14, ACM, New York, NY, USA (2014)

18. Clouston, R., Bizjak, A., Bugge Grathwohl, H., Birkedal, L.: The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science 12(3) (2016)

19. Dreyer, D., Ahmed, A., Birkedal, L.: Logical Step-Indexed Logical Relations. Logical Methods in Computer Science Volume 7, Issue 2 (2011). https://doi.org/10.2168/LMCS-7(2:16)2011, https://lmcs.episciences.org/698

20. Dreyer, D., Neis, G., Rossberg, A., Birkedal, L.: A Relational Modal Logic for Higher-order Stateful ADTs. In: Proceedings POPL’10. pp. 185–198. ACM (2010)

21. Elliott, C., Hudak, P.: Functional Reactive Animation. In: Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming. pp. 263–273. ICFP’97, ACM, New York, NY, USA (1997). https://doi.org/10.1145/258948.258973, http://doi.acm.org/10.1145/258948.258973

22. Freeman, T., Pfenning, F.: Refinement Types for ML. In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation. pp. 268–277. PLDI’91, Association for Computing Machinery, New York, NY, USA (1991). https://doi.org/10.1145/113445.113468, https://doi.org/10.1145/113445.113468

23. Fujima, K., Ito, S., Kobayashi, N.: Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes. In: APLAS ’13: Proceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 8301. pp. 17–32. Springer-Verlag, Berlin, Heidelberg (2013). https://doi.org/10.1007/978-3-319-03542-0_2, https://doi.org/10.1007/978-3-319-03542-0_2

24. Gratzer, D., Kavvos, G.A., Nuyts, A., Birkedal, L.: Multimodal dependent type theory. In: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 492–506. LICS ’20, Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3373718.3394736, https://doi.org/10.1145/3373718.3394736

25. Guatto, A.: A Generalized Modality for Recursion. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 482–491. LICS ’18, ACM, New York, NY, USA (2018). https://doi.org/10.1145/3209108.3209148

26. Hofmann, M., Chen, W.: Abstract interpretation from büchi automata. In: Henzinger, T.A., Miller, D. (eds.) Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS ’14, Vienna, Austria, July 14 - 18, 2014. pp. 51:1–51:10. ACM (2014). https://doi.org/10.1145/2603088.2603127, https://doi.org/10.1145/2603088.2603127
27. Hofmann, M., Ledent, J.: A cartesian-closed category for higher-order model checking. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1–12. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005120, https://doi.org/10.1109/LICS.2017.8005120

28. Jaber, G., Riba, C.: Temporal Refinements for Guarded Recursive Types (Jan 2021), https://hal.archives-ouvertes.fr/hal-02512655, full version. Available on HAL (hal-02512655)

29. Jacobs, B.: Categorical Logic and Type Theory. Studies in logic and the foundations of mathematics, Elsevier (2001)

30. Jacobs, B.: Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study. ITA 35(1), 31–59 (2001)

31. Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2016)

32. Jeffrey, A.: LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs. In: Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification. pp. 49–60. PLPV’12, ACM, New York, NY, USA (2012). https://doi.org/10.1145/2103776.2103783, http://doi.acm.org/10.1145/2103776.2103783

33. Jeltsch, W.: An Abstract Categorical Semantics for Functional Reactive Programming with Processes. In: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages Meets Program Verification. pp. 47–58. PLPV’14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2541568.2541573, http://doi.acm.org/10.1145/2541568.2541573

34. Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying functional programs using abstract interpreters. In: International Conference on Computer Aided Verification. pp. 470–485. Springer (2011)

35. Jones, G., Gibbons, J.: Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips. Technical report, University of Auckland (1993)

36. Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018)

37. Kobayashi, K., Nishikawa, T., Igarashi, A., Unno, H.: Temporal Verification of Programs via First-Order Fixpoint Logic. In: Chang, B.E. (ed.) Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11822, pp. 413–436. Springer (2019). https://doi.org/10.1007/978-3-030-32304-2_20, https://doi.org/10.1007/978-3-030-32304-2_20

38. Kobayashi, N., Fedyukovich, G., Gupta, A.: Fold/Unfold Transformations for Fixpoint Logic. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12079, pp. 195–214. Springer (2020). https://doi.org/10.1007/978-3-030-45237-7_12, https://doi.org/10.1007/978-3-030-45237-7_12

39. Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science. pp. 179–188. IEEE (2009)
27. Hofmann, M., Ledent, J.: A cartesian-closed category for higher-order model checking. In: 32nd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2017, Reykjavik, Iceland, June 20-23, 2017. pp. 1-12. IEEE Computer Society (2017). https://doi.org/10.1109/LICS.2017.8005120, https://doi.org/10.1109/LICS.2017.8005120

28. Jaber, G., Riba, C.: Temporal Refinements for Guarded Recursive Types (Jan 2021), https://hal.archives-ouvertes.fr/hal-02512655, full version. Available on HAL (hal-02512655)

29. Jacobs, B.: Categorical Logic and Type Theory. Studies in logic and the foundations of mathematics, Elsevier (2001)

30. Jacobs, B.: Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study. ITA 35(1), 31-59 (2001)

31. Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2016)

32. Jeffrey, A.: LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs. In: Proceedings of the Sixth Workshop on Programming Languages Meets Program Verification. pp. 49-60. PLPV'12, ACM, New York, NY, USA (2012). https://doi.org/10.1145/2103776.2103783, http://doi.acm.org/10.1145/2103776.2103783

33. Jeltsch, W.: An Abstract Categorical Semantics for Functional Reactive Programming with Processes. In: Proceedings of the ACM SIGPLAN 2014 Workshop on Programming Languages Meets Program Verification. pp. 47-58. PLPV'14, ACM, New York, NY, USA (2014). https://doi.org/10.1145/2541568.2541573, http://doi.acm.org/10.1145/2541568.2541573

34. Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: Verifying functional programs using abstract interpreters. In: International Conference on Computer Aided Verification. pp. 470-485. Springer (2011)

35. Jones, G., Gibbons, J.: Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips. Technical report, University of Auckland (1993)

36. Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming 28 (2018)

37. Kobayashi, K., Nishikawa, T., Igarashi, A., Unno, H.: Temporal Verification of Programs via First-Order Fixpoint Logic. In: Chang, B.E. (ed.) Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings. Lecture Notes in Computer Science, vol. 11822, pp. 413-436. Springer (2019). https://doi.org/10.1007/978-3-030-32304-2_20, https://doi.org/10.1007/978-3-030-32304-2_20

38. Kobayashi, N., Fedyukovich, G., Gupta, A.: Fold/Unfold Transformations for Fixpoint Logic. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II. Lecture Notes in Computer Science, vol. 12079, pp. 195-214. Springer (2020). https://doi.org/10.1007/978-3-030-45237-7_12, https://doi.org/10.1007/978-3-030-45237-7_12

39. Kobayashi, N., Ong, C.H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: 2009 24th Annual IEEE Symposium on Logic In Computer Science. pp. 179-188. IEEE (2009)
40. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. SIGPLAN Not. 46(6), 222–233 (2011). https://doi.org/10.1145/1993316.1993525, https://doi.org/10.1145/1993316.1993525

41. Kobayashi, N., Tabuchi, N., Unno, H.: Higher-Order Multi-Parameter Tree Transducers and Recursion Schemes for Program Verification. In: POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 495–508. Association for Computing Machinery, New York, NY, USA (2010). https://doi.org/10.1145/1707801.1706355, https://doi.org/10.1145/1707801.1706355

42. Koskinen, E., Terauchi, T.: Local Temporal Reasoning. In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). CSL-LICS'14, Association for Computing Machinery, New York, NY, USA (2014). https://doi.org/10.1145/2603088.2603138, https://doi.org/10.1145/2603088.2603138

43. Kozen, D.: Results on the propositional $\mu$-calculus. Theoretical Computer Science 27(3), 333–354 (1983), special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982

44. Krishnaswami, N.R.: Higher-order functional reactive programming without space-time leaks. In: Proceedings of ICFP'13. pp. 221–232. ACM, New York, NY, USA (2013)

45. Krishnaswami, N.R., Benton, N.: Ultrametric Semantics of Reactive Programs. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science. pp. 257–266 (2011). https://doi.org/10.1109/LICS.2011.38

46. Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic Termination Verification for Higher-Order Functional Programs. In: Shao, Z. (ed.) Programming Languages and Systems. pp. 392–411. ESOP'14, Springer Berlin Heidelberg, Berlin, Heidelberg (2014)

47. Mac Lane, S., Moerdijk, I.: Sheaves in geometry and logic: A first introduction to topoi theory. Springer (1992)

48. Marin, S.: Modal proof theory through a focused telescope. PhD thesis, Université Paris Saclay (Jan 2018), https://hal.archives-ouvertes.fr/tel-01951291

49. McBride, C., Paterson, R.: Applicative programming with effects. Journal of Functional Programming 18(1) (2008). https://doi.org/10.1017/S0956796807006326

50. Møgelberg, R.E.: A type theory for productive coprogramming via guarded recursion. In: Proceedings of CSL-LICS 2014. CSL-LICS '14, ACM (2014)

51. Murase, A., Terauchi, T., Kobayashi, N., Sato, R., Unno, H.: Temporal Verification of Higher-Order Functional Programs. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 57–68. POPL'16, Association for Computing Machinery, New York, NY, USA (2016). https://doi.org/10.1145/2837614.2837667, https://doi.org/10.1145/2837614.2837667

52. Nakano, H.: A Modality for Recursion. In: Proceedings of LICS'00. pp. 255–266. IEEE Computer Society (2000)

53. Nanjo, Y., Unno, H., Koskinen, E., Terauchi, T.: A Fixpoint Logic and Dependent Effects for Temporal Property Verification. In: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science. pp. 759–768. LICS'18, Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3209108.3209204, https://doi.org/10.1145/3209108.3209204