Guilhem Jaber
email: guilhem.jaber@univ-nantes.fr

Colin Riba
email: colin.riba@ens-lyon.fr

Temporal Refinements for Guarded Recursive Types

Keywords: coinductive types, guarded recursive types, µ-calculus, refinement types, topos of trees

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. We use in a crucial way the connection with set-theoretic semantics to handle liveness properties.

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. [START_REF] Baier | Principles of Model Checking[END_REF]). Typically, modalities like 2 (always) or 3 (eventually) are used to write properties of streams or infinite trees and specifications of programs over such data.

We consider temporal refinement types {A | ϕ}, where A is a standard type of our programming language, and ϕ is a formula of the modal µ-calculus. Using refinement types [24], 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: elements satisfying ψ to one with infinitely many (resp. ultimately all) elements satisfying ϕ. For ϕ a formula over A, [hd]ϕ is a formula over streams of A's which holds on a given stream if ϕ holds on its head element.

It is undecidable whether a given higher-order program satisfies a given inputoutput temporal property written with formulae of the modal µ-calculus [45]. 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 λ-calculus [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF], a higher-order programming language with guarded recursion [START_REF] Nakano | A Modality for Recursion[END_REF]. Guarded recursion is a simple device to control and reason about unfoldings of fixpoints. It can represent coinductive types [START_REF] Møgelberg | A type theory for productive coprogramming via guarded recursion[END_REF] and provides a syntactic compositional productivity check [5].

Safety properties (e.g. [START_REF] Ahmed | Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types[END_REF][hd]ϕ) can be correctly represented with guarded fixpoints, but not liveness properties (e.g. 3[hd]ϕ, [START_REF] Jacobs | Categorical Logic and Type Theory[END_REF][hd]ϕ, [START_REF] Elliott | Functional Reactive Animation[END_REF][hd]ϕ). 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) [START_REF] Elliott | Functional Reactive Animation[END_REF] provides a Curry-Howard correspondence for temporal logics [START_REF] Jeffrey | LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs[END_REF][START_REF] Jeltsch | An Abstract Categorical Semantics for Functional Reactive Programming with Processes[END_REF][START_REF] Cave | Fair Reactive Programming[END_REF] in which logical connectives are reflected as programming constructs. When combining FRP with guarded recursion [48,[START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF], and in particular to handle liveness properties [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF], uniqueness of guarded fixpoints is tempered by specific recursors for temporal types.

Our approach is different from [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF], 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 µ-calculus, in which fixpoints can always be computed in ω-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 [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF], which correctly represents the usual set-theoretic final coalgebras of polynomial coinductive types [START_REF] Møgelberg | A type theory for productive coprogramming via guarded recursion[END_REF].

We provide example programs involving linear structures (colists, streams, fair streams [START_REF] Cave | Fair Reactive Programming[END_REF][START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF]) and branching structures (resumptions à la [48]), for which we prove liveness properties similar to ( ) above. Our system also handles safety properties on breadth-first (infinite) tree traversals à la [START_REF] Jones | Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips[END_REF] and [START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF].

Cons g := λx.λs. fold( x, s ) : A → Str g A → Str g A hd g := λs.π0(unfold s) : Str g A → A tl g := λs.π1(unfold s) : Str g A → Str g A map g := λf.fix(g).λs. Cons g (f (hd g s)) (g (tl g s)) : (B → A) → Str g B → Str g A Fig. [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF]. Constructor, Destructors and Map on Guarded Streams.

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 the Appendices.

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 Str g A over a type A via the guarded recursive definition Str g A = A × Str g 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 E M : A E next(M ) : A E, x : A M : A E 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 :: g s for Cons g a s. Using the fact that the type modality is an applicative functor [54], 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 Str g A that selects those streams whose elements all satisfy ϕ. To do so, we use a temporal modal formula 2[hd]ϕ, and consider the refinement type {Str g A | 2[hd]ϕ}. Suppose for now that we Typed Formulae Provability Refinement Types Subtyping Typing

Σ ϕ : A A ϕ {A | ϕ} T ≤ U E M : T ( §4)
(where ϕ : A, §4) (where ϕ : A, §5) (T , U refinement types, §5)

Table 1. Syntactic Classes and Judgments.

can give the following refinement types to the basic stream operations:

hd g : {Str g A | 2[hd]ϕ} -→ {A | ϕ} tl g : {Str g A | 2[hd]ϕ} -→ {Str g A | 2[hd]ϕ} Cons g : {A | ϕ} -→ {Str g A | 2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
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 g as

map g : ({B | ψ} → {A | ϕ}) -→ {Str g B | 2[hd]ψ} -→ {Str g A | 2[hd]ϕ}
A Manysorted Temporal Logic. Our logical language, taken with minor adaptations from [START_REF] Jacobs | Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study[END_REF], is manysorted : for each type A we have formulae of type A (notation ϕ : A), where ϕ selects inhabitants of A.

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

:= [fold][in 1 ] ).
We also provide a deduction system A ϕ on temporal modal formulae. This deduction system is used to define a subtyping relation T ≤ U between refinement types, with {A | ϕ} ≤ {A | ψ} when A ϕ ⇒ ψ. 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 [47]. In particular, we can form an always modality as 2ϕ := ν α. ϕ ∧ α, with 2ϕ : Str g A if ϕ : Str g A. The formula 2ϕ holds on a stream s = (s i | i ≥ 0), iff ϕ holds on every substream (s i | i ≥ n) for n ≥ 0. If we rather start with ψ : A, one first need to lift it to [hd]ψ : Str g A. Then 2[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 µαϕ. For example, this would give the eventually modality 3ϕ := µα. ϕ ∨ α. With Kozen-style rules, one could then give the following two types to the guarded stream constructor: that is supposed to enforce the existence of an occurrence of b in the stream. Similarly, on colists we would have fix(s).a :: g s of type {CoList g B | 3[nil]}, while 3 [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 λ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 X n : X(n + 1) → 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 (N \ {0}, ≤). The category S of such presheaves is the topos of trees [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF]. For instance, the type 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 , . . . , b n-1 , b n ) to (b 0 , . . . , 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 3[hd][b] cannot describe in S the set of streams that contain at least one occurrence of b. Indeed, the interpretation of 3[hd][b] in S is a sequence (C(n)) n>0 with C(n) ⊆ 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 3[hd][b] is the whole Str g B . More generally, guarded fixpoints have unique solutions in the topos of trees [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF], and 3ϕ = µα. ϕ ∨ ϕ gets the same interpretation as ν α. ϕ ∨ α.

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 [START_REF] Møgelberg | A type theory for productive coprogramming via guarded recursion[END_REF] 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. The Constant Type Modality. Figure 2 represents adjoint functors Γ : S → Set and ∆ : Set → S. To correctly handle least fixpoints µαϕ : A, we would like to see them as subsets of Γ A in 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 Set via the adjunction ∆ Γ . This adjunction induces a comonad ∆Γ on S, which is represented in the guarded λ-calculus of [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF] by the constant type modality . This gives coinductive versions of guarded recursive types, e.g. Str A := Str g A for streams and CoList A := CoList g A for colists, which allow for productive but not causal programs [20, Ex. 1.10.(3)].

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

Approximating Least Fixpoints. For proving liveness properties on functions defined by guarded recursion, one needs to navigate between e.g. [box]3ϕ and 3ϕ, while 3ϕ is in general unsafe. The fixpoint 3ϕ = µα.ϕ ∨ α is alternation-free (see e.g. [17, §4.1]). This implies that 3ϕ can be seen as the supremum of the m ϕ for m ∈ N, where each m ϕ is safe when ϕ is safe. More generally, we can approximate alternation-free µαϕ by their finite unfoldings ϕ m (⊥), à la Kleene. We extend the logic with finite iterations µ k αϕ, where k is an iteration variable, and where µ k αϕ is seen as ϕ k (⊥). Let 3 k ϕ := µ k α. ϕ∨ α. If ϕ is safe then so is 3 k ϕ. For safe ϕ, ψ, we have the following refinement typings for the guarded recursive map g and its coinductive lift map:

map g : ({B | ψ} → {A | ϕ}) → Str g B 3 k [hd]ψ → Str g A 3 k [hd]ϕ map : ({B | ψ} → {A | ϕ}) → {Str B | [box]3[hd]ψ} → {Str A | [box]3[hd]ϕ}
3 The Pure Calculus

Our system lies on top of the guarded λ-calculus of [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF]. We briefly review it here. We consider values and terms from the grammar given in Fig. 3 (left). In ] (M ) where x 1 , . . . , x k is a list of all free variables of M , and similarly for prev ι (M ). We consider the weak call-by-name reduction of [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF], recalled in Fig. 3 (right).

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

A ::= 1 | A + A | A × A | A → A | A | X | Fix(X).A | A
where, (1) in the case Fix(X).A, each occurrence of X in A must be guarded by a , and (2) in the case of A, the type A is closed (i.e. has no free type variable). Guarded recursive types are built with the fixpoint constructor Fix(X).A, which allows for X to appear in A both at positive and negative positions, but only under a . In this paper we shall only consider positive types. Example 3.2. Besides streams (Str g A), colists (CoList g A), conatural numbers (CoNat g ) and infinite binary trees (Tree g A), we consider a type Res g A of resumptions (parametrized by I, O) adapted from [48], and a higher-order recursive type Rou g A, used in Martin Hofmann's breadth-first tree traversal (see e.g. [START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]):

Tree g A := Fix(X). A × ( X × X) CoNat g := Fix(X). 1 + X Res g A := Fix(X). A + (I → (O × X)) Rou g A := Fix(X). 1 + (( X → A) → A)
Some typing rules of the pure calculus are given in Fig. 4, where a pure type A is constant if each occurrence of in A is guarded by a modality. The omitted rules are the standard ones for simple types with finite sums and products ( §A).

E M : A[Fix(X).A/X] E fold(M ) : Fix(X).A E M : Fix(X).A E unfold(M ) : A[Fix(X).A/X] E M : (B → A) E N : B E M N : A E M : A E next(M ) : A x1 : A1, . . . , xk : Ak M : A E Mi : Ai with Ai constant for 1 ≤ i ≤ k E prev [x1 →M1,...,x k →M k ] (M ) : A x1 : A1, . . . , xk : Ak M : A E Mi : Ai with Ai constant for 1 ≤ i ≤ k E box [x1 →M1,...,x k →M k ] (M ) : A E M : A E unbox(M ) : A

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 (ν αϕ). It is extended with least fixpoints (µαϕ) 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 [START_REF] Jacobs | Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study[END_REF], is manysorted : for each pure type A we have formulae ϕ of type A (notation ϕ : A). The formulation rules of formulae are given in Fig. 5.

α : A) ∈ Σ Σ α : A Σ ⊥ : A Σ : A Σ ϕ : A Σ, α : B ϕ : A Σ ϕ : A Σ ψ : A Σ ϕ ⇒ ψ : A Σ ϕ : A Σ ψ : A Σ ϕ ∧ ψ : A Σ ϕ : A Σ ψ : A Σ ϕ ∨ ψ : A Σ ϕ : Ai Σ [πi]ϕ : A0 × A1 Σ ϕ : Ai Σ [ini]ϕ : A0 + A1 Σ ψ : B Σ ϕ : A Σ [ev(ψ)]ϕ : B → A Σ ϕ : A[Fix(X).A/X] Σ [fold]ϕ : Fix(X).A Σ ϕ : A Σ [next]ϕ : A ϕ : A [box]ϕ : A (ν-F) Σ, α : A ϕ : A α Pos ϕ Σ ν αϕ : A (α guarded in ϕ)
:= [fold][π 1 ][π 0 ][next]ϕ and r ϕ := [fold][π 1 ][π 1 ][next]ϕ.
Intuitively, [lbl]ϕ should hold on a tree t over A iff the root label of t satisfies ϕ, and ϕ (resp. r ϕ) should hold on t iff ϕ holds on the left (resp. right) immediate subtree of t.

Formulae have fixpoints ν αϕ. The rules of Fig. 5 thus allow for the formation of formulae with free typed propositional variables (ranged over by α, β, . . . ), and involve contexts Σ of the form α 1 : A 1 , . . . , α n : A n . In the formation of a fixpoint, the side condition "α guarded in ϕ" asks that each occurrence of α 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 α in ϕ. It is defined with relations α Pos ϕ and α Neg ϕ (see App. B). We just mention here that [ev(-)](-) is contravariant in its first argument. Note that [box]ϕ can only be formed for closed ϕ.

Example 4.3. (a) The modality 2 makes it possible to express a range of safety properties. For instance, assuming ϕ, ψ :

Str g A, the formula 2(ψ ⇒ ϕ) is intended to hold on a stream s = (s i | i ≥ 0) iff, for all n ∈ N, if (s i | i ≥ n) satisfies ψ, then (s i | i ≥ n + 1) satisfies ϕ. (b)
The modality 2 has its two CTL-like variants on Tree g A, namely ∀2ϕ := ν α. ϕ ∧ ( α ∧ r α) and ∃2ϕ := ν α. ϕ ∧ ( α ∨ r α). Assuming ψ : A, ∀2[lbl]ψ is intended to hold on a tree t : Tree g A iff all node-labels of t satisfy ψ, while ∃2[lbl]ψ holds on t iff ψ holds on all nodes of some infinite path from the root of t. 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 A (the general case) and a classical theory A c (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, A (c) ϕ is only defined when ϕ : A (and so when ϕ has no free propositional variable).

Name Formulation

[πi] [fold] [next] [ini] [ev(ψ)] [box] [hd] (RM) ψ ⇒ ϕ [ ]ψ ⇒ [ ]ϕ (C) [ ]ϕ ∧ [ ]ψ =⇒ [ ](ϕ ∧ ψ) (N) [ ] (P) [ ]⊥ =⇒ ⊥ (C) (C) (C∨) [ ](ϕ ∨ ψ) =⇒ [ ]ϕ ∨ [ ]ψ (C⇒) ([ ]ψ ⇒ [ ]ϕ) ⇒ [ ](ψ ⇒ ϕ) (C) (C)
Fixpoints ν αϕ are equipped with their usual Kozen axioms [47]. The atomic modalities [π 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 [START_REF] Plotkin | A Framework for Intuitionistic Modal Logics: Extended Abstract[END_REF] (see also e.g. [START_REF] Simpson | The Proof Theory and Semantics of Intuitionistic Modal Logic[END_REF]53]) for [π 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:

B a∈B [a] ∧ b∈B b =a ¬[b]
Definition 4.4 (Modal Theories). For each pure type A, the intuitionistic and classical modal theories A ϕ and A c ϕ (where ϕ : A) are defined by mutual induction:

-The theory 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 A ). -The theory A c is A augmented with the axioms (P) and (C ⇒ ) for [next] and with the axiom (CL) (Fig. 6).

For example, we have

Str g A 2ψ ⇒ (ψ ∧ 2ψ) and Str g A (ψ ∧ 2ψ) ⇒ 2ψ. B ψ ⇒ φ ϕ : A B→A [ev(φ)]ϕ ⇒ [ev(ψ)]ϕ B→A ([ev(ψ0)]ϕ ∧ [ev(ψ1)]ϕ) ⇒ [ev(ψ0 ∨ ψ1)]ϕ A c ((ϕ ⇒ ψ) ⇒ ϕ) ⇒ ϕ (CL) A c ϕ A [box]ϕ A 0 +A 1 [in0] ∨ [in1] ∧ ¬ [in0] ∧ [in1] A 0 +A 1 ([ini] ) ⇒ (¬[ini]ϕ ⇔ [ini]¬ϕ) A ν αϕ ⇒ ϕ[ν αϕ/α] A ψ ⇒ ϕ[ψ/α] A ψ ⇒ ν αϕ
Fig. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]. Modal Axioms and Rules.

T ≤ |T | A ≤ {A | } A ϕ ⇒ ψ {A | ϕ} ≤ {A | ψ} A c ϕ ⇒ ψ { A | [box]ϕ} ≤ { A | [box]ψ} { A | [next]ϕ} ≡ {A | ϕ} {B → A | [ev(ψ)]ϕ} ≡ {B | ψ} → {A | ϕ}

A Temporally Refined Type System

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

T, U ::= A | {A | ϕ} | T + T | T × T | T → T | T | T
where ϕ : A and, in the case of T , the type T has no free type variable. So types are built from (closed) pure types A and temporal refinements {A | ϕ}.

They allow for all the type constructors of pure types.

As a refinement type {A | ϕ} 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 | ϕ} → {B | ψ} is a subtype of A → B. We formalize this with the notion of underlying pure type |T | of a type T . The second ingredient is the modal theory A ϕ of §4. The subtyping rules concerning refinements are given in Fig. 7, where T ≡ U enforces both T ≤ U and U ≤ T . The full set of rules is given in Fig. 17 in §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 [π i ], [in i ],
[fold] and [ev(-)] (but not [next]) have introduction rules extending those of the corresponding term formers. Example 5. [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF]. Since ϕ ⇒ ψ ⇒ (ϕ ∧ ψ) and using two times the rule (MP), we get the first derived rule below, from which we can deduce the second one:

(Pii-I) E Mi : {Ai | ϕ} E M1-i : A1-i E M0, M1 : {A0 × A1 | [πi]ϕ} (Pii-E) E M : {A0 × A1 | [πi]ϕ} E πi(M ) : {Ai | ϕ} (Ev-I) E, x : {B | ψ} M : {A | ϕ} E λx.M : {B → A | [ev(ψ)]ϕ} (Ev-E) E M : {B → A | [ev(ψ)]ϕ} E N : {B | ψ} E M N : {A | ϕ} (Fd-I) E M : {A[Fix(X).A/X] | ϕ} E fold(M ) : {Fix(X).A | [fold]ϕ} (Fd-E) E M : {Fix(X).A | [fold]ϕ} E unfold(M ) : {A[Fix(X).A/X] | ϕ} (Inji-E) E M : {A0 + A1 | [ini]ϕ} E, x : {Ai | ϕ} Ni : U E, x : A1-i N1-i : U E case M of (x.N0|x.N1) : U (∨-E) for i ∈ {0, 1}, E M : {A | ϕ0 ∨ ϕ1} E, x : {A | ϕi} N : U E N [M/x] : U (Inji-I) E M : {Ai | ϕ} E ini(M ) : {A0 + A1 | [ini]ϕ} (MP) E M : {A | ψ ⇒ ϕ} E M : {A | ψ} E M : {A | ϕ} (ExF) E M : {A | ⊥} E N : |U | E N : U (Sub) E M : T T ≤ U E M : U
E M : {A | ϕ} E M : {A | ψ} E M : {A | ϕ ∧ ψ} E M : {A | ϕ} E N : {B | ψ} E M, N : {A × B | [π 0 ]ϕ ∧ [π 1 ]ψ} Example 5.2.
We have the following derived rules:

E M : {Str g A | 2ϕ} E M : {Str g A | ϕ ∧ 2ϕ} and E M : {Str g A | ϕ ∧ 2ϕ} E M : {Str g A | 2ϕ}
Example 5.3. We have Cons g : A → {Str g A | ϕ} → {Str g A | ϕ} as well as tl g : {Str g A | ϕ} → {Str g A | ϕ}.

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

{Str g A | 2[hd]ϕ 0 } -→ {Str g A | 2[hd]ϕ 1 } -→ {Str g A | 2([hd]ϕ 0 ∨ [hd]ϕ 1 )}
for the merge g function which takes two guarded streams and interleaves them:

merge g : Str g A -→ Str g A -→ Str g A := fix(g).λs 0 .λs 1 . (hd g s 0 ) :: g next (hd g s 1 ) :: g (g (tl g s 0 ) (tl g s 1 ))
6 The Full System

The system presented so far has only one form of fixpoints in formulae (ν αϕ).

We now present our full system, which also handles least fixpoints (µαϕ) and thus liveness properties. A key role is played by polynomial guarded recursive types, that we discuss first. [START_REF] Baier | Principles of Model Checking[END_REF]. Extended Formation Rules of Formulae (with α Pos ϕ and α guarded in ϕ).

(µ-F) Σ, α : A ϕ : A Σ µαϕ : A Σ, α : A ϕ : A Σ µ t αϕ : A Σ, α : A ϕ : A Σ ν t αϕ : A Fig.
A ϕ[µαϕ/α] ⇒ µαϕ Strictly Positive and Polynomial Types. Strictly positive types (notation P + , Q + , etc.) are given by

A ϕ[ψ/α] ⇒ ψ A µαϕ ⇒ ψ A θ t+1 αϕ ⇔ ϕ[θ t αϕ/α] A µ 0 αϕ ⇔ ⊥ A ν 0 αϕ ⇔ t ≤ u A µ t αϕ ⇒ µ u αϕ A µ t αϕ ⇒ µαϕ t ≥ u A ν t αϕ ⇒ ν u αϕ A ν αϕ ⇒ ν t αϕ
P + ::= A | X | P + | P + + P + | P + × P + | Fix(X).P + | B → P +
where A, B are (closed) constant pure types. Strictly positive types are a convenient generalization of polynomial types. A guarded recursive type Fix(X).P (X) is polynomial if P (X) is induced by

P (X) ::= A | X | P (X) + P (X) | P (X) × P (X) | B → P (X)
where A, B are (closed) constant pure types. Note that if Fix(X).P (X) is polynomial, X cannot occur on the left of an arrow (→) in P (X). We say that 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 functors of [START_REF] Jacobs | Introduction to Coalgebra: Towards Mathematics of States and Observation[END_REF], which all have final Set-coalgebras (see e.g. [START_REF] Jacobs | Introduction to Coalgebra: Towards Mathematics of States and Observation[END_REF]Cor. 4.6.3]

n i=0 A i × ( X) Bi with A i , B i constant.
The nonstrictly positive recursive type Rou g A of Ex. 3.2, used in Hofmann's breadth-first traversal (see e.g. [START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]), is not polynomial.

The Full Temporal Modal Logic. We assume given a first-order signature of iteration terms (notation t, u, etc.), with iteration variables k, , etc., and for each iteration term t(k 1 , . . . , k m ) with variables as shown, a given primitive recursive function t : N m → N. We assume a term 0 for 0 ∈ N and a term k+1 for the successor function n ∈ N → n + 1 ∈ N.

The formulae of the full temporal modal logic extend those of Fig. 5 with least fixpoints µαϕ and with approximated fixpoints µ t αϕ and ν t αϕ where t is an iteration term. The additional formation rule for formulae are given in Fig. [START_REF] Baier | Principles of Model Checking[END_REF]. We use θ as a generic notation for µ and ν. Least fixpoints µαϕ are equipped with their usual Kozen axioms. In addition, iteration formulae ν t αϕ(α) and µ t αϕ(α) have axioms expressing that they are indeed iterations of ϕ(α) from resp. and ⊥. A fixpoint logic with iteration variables was already considered in [68]. On trees, we have the CTL-like ∃3ϕ := µα. ϕ ∨ ( α ∨ r α) and ∀3ϕ := µα. ϕ ∨ ( α ∧ r α). The formula ∃3ϕ is intended to hold on a tree if there is a finite path which leads to a subtree satisfying ϕ, while ∀3ϕ is intended to hold if every infinite path crosses a subtree satisfying ϕ. 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 µ-calculus. For this fragment, satisfiability is decidable (see e.g. [START_REF] Bradfield | The mu-calculus and Model Checking[END_REF]), as well as the classical theory c by completeness of Kozen's axiomatization [START_REF] Walukiewicz | Completeness of Kozen's Axiomatisation of the Propositional µ-Calculus[END_REF] (see [START_REF] Santocanale | Completeness for flat modal fixpoint logics[END_REF] for completeness results on fragments of the µ-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 [box]ϕ when ϕ is safe. Definition 6.5 (Safe Formula). Say α 1 : A 1 , . . . , α n : A n ϕ : A is safe if (i) the types A 1 , . . . , A n , A are strictly positive, and (ii) for each occurrence in ϕ of a modality [ev(ψ)], the formula ψ is closed, and (iii) each occurrence in ϕ of a least fixpoint (µα(-)) and of an implication (⇒) is guarded by a [box].

Note that the safe restriction imposes no condition on approximated fixpoints θ t α. Recalling that the theory under a [box] is A c , the only propositional connectives accessible to A in safe formulae are those on which A and A c coincide. The Full System. We extend the types of §5 with universal quantification over iteration variables (∀k • T ). The type system of §5 is extended with the rules of Fig. 11.

Example 6. [START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]. The logical rules of Fig. 10 give the following derived typing rules (where β Pos γ):

(µ-I) E M : { A | [box]γ[µ t αϕ/β]} E M : { A | [box]γ[µαϕ/β]} (ν-E) E M : { A | [box]γ[ν αϕ/β]} E M : { A | [box]γ[ν t αϕ/β]} ϕ safe { A | [box]ϕ} ≡ {A | ϕ} ∀k • T ≡ ∀k • T (∀-I) E M : T E M : ∀k • T (∀-CI) E M : T [0/k] E M : T [k+1/k] E M : ∀k • T (ν-I) E M : A [box]γ[ν αψ/β] E M : { A | [box]γ[ν αψ/β]} (∀-E) E M : ∀k • T E M : T [t/k] (µ-E) E M : { A | [box]γ[µαψ/β]} E, x : A [box]γ[µ αψ/β] N : U E N [M/x] : U

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 [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF]. Formally, S is the category of presheaves over (N \ {0}, ≤). In words, the objects of S are indexed sets X = (X(n)) n>0 equipped with restriction maps r X n : X(n + 1) → X(n). Excluding 0 from the indexes is a customary notational convenience ( [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF]). The morphisms from X to Y are families of functions f = (f n :

X(n) → Y (n)) n>0 which commute with restriction, that is f n •r X n = r Y n •f n+1 .
As any presheaf category, S has (pointwise) limits and colimits, and is Cartesian closed (see e.g. [52, §I.6]). We write Γ : S → Set for the global section functor, which takes X to S[1, X], the set of morphisms 1 → X in S, where 1 = ({•}) n>0 is terminal in S.

A typed term E M : T is to be interpreted in S as a morphism

M : |E| -→ |T | where |E| = |T 1 | × • • • × |T n | for E = x 1 : T 1 , . . . , x n : T n .
In particular, a closed term M : T is to be interpreted as a global section M ∈ Γ |T | . The ×/ + / → fragment of the calculus is interpreted by the corresponding structure in S. The modality is interpreted by the functor : S → S of [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF]. 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 next X : X → X as in The guarded fixpoint combinator fix is interpreted by the morphism fix X : X X → X of [13, Thm. 2.4].

X next X X 1 1 X 2 r X 1 o o r X 1 X n r X n-1 o o X n+1 r X n o o r X n o o X 1 X 1 1 o o X n-1 o o X n r X n-1 o o o o {|[πi]ϕ|} := {x ∈ Γ A0 × A1 | πi • x ∈ {|ϕ|}} {|[next]ϕ|} := {next • x ∈ Γ A | x ∈ {|ϕ|}} {|[fold]ϕ|} := {x ∈ Γ Fix(X).A | unfold • x ∈ {|ϕ|}} {|[box]ϕ|} := {x ∈ Γ A | x1(•) ∈ {|ϕ|}} {|[ini]ϕ|} := x ∈ Γ A0 + A1 ∃y ∈ Γ Ai x = ini • y and y ∈ {|ϕ|} {|[ev(ψ)]ϕ|} := x ∈ Γ B → A ∀y ∈ Γ B y ∈ {|ψ|} =⇒ ev • x, y ∈ {|ϕ|}
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 [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF] and §D for the interpretation of prev, box and unbox. Just note that the unit η : Id Set → Γ ∆ is an iso.

Together with an interpretation of guarded recursive types, this gives a denotational semantics of the pure calculus of §3. See [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF][START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF] 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 [55] has shown that for polynomial types such as Str g B with B a constant type, the set of global sections Γ Str g 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 Set : Set → Set in the obvious way.

Theorem 7.1 ( [START_REF] Møgelberg | A type theory for productive coprogramming via guarded recursion[END_REF] (see also [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF])). If Fix(X).P (X) is polynomial, then the set Γ Fix(X).P (X) carries a final Set-coalgebra structure for P Set .

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 ν t αϕ(α) and µ t αϕ(α) (for t closed) are defined to be the interpretations resp. of ϕ t ( ) and ϕ t (⊥), where e.g. ϕ 0 ( ) := and ϕ n+1 ( ) := ϕ(ϕ n ( )). 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 [START_REF] Jacobs | Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study[END_REF] (with sums as in [START_REF] Jacobs | Introduction to Coalgebra: Towards Mathematics of States and Observation[END_REF]) 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 ϕ : A. We sketch it here. First, Sub(X) is the (complete) Heyting algebra of subobjects of an object X of S. Explicitly, we have S = (S(n)) n ∈ Sub(X) iff for all n > 0, S(n) ⊆ X(n) and r X n (t) ∈ S(n) whenever t ∈ S(n + 1). For propositional connectives and fixpoints, the internal -is defined similarly as the external {|-|}, but using (complete) Heyting algebras of subobjects rather than (complete) Boolean algebras of subsets.

As 2), and 3[hd]ϕ can "lie" about the next time step. We let [box]ϕ := ∆({|ϕ|}).

The modality [ev(ψ)] is a bit more complex. For ψ : B and ϕ : A, the formula [ev(ψ)]ϕ is interpreted as a logical predicate in the sense of [32, §9.2 & Prop. 9. 2.4]. The idea is that for a term M : {B → A | [ev(ψ)]ϕ}, the global section ev • M , x ∈ Γ A should satisfy ϕ whenever x ∈ Γ B satisfies ψ. We refer to §D for details.

Our semantics are both correct w.r. 11), which makes available the comonad structure of on [box]ϕ when ϕ is safe. Recall that in safe formulae, implications can only occur under a [box] modality and thus in closed subformulae. It is crucial for Prop. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].3 that infs and sups are pointwise in the subobject lattices of S, so that conjunctions and disjunctions are interpreted as with the usual classical Kripke semantics (see e.g. [START_REF] Lane | Sheaves in geometry and logic: A first introduction to topos theory[END_REF]§VI.7]). This does not hold for implications!

The second key to Prop. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].3 is the following. For L a complete lattice, a Scott cocontinuous function L → L is a Scott continuous function L op → L op , i.e. which preserves codirected infs. For a safe α : A ϕ : A, the poset maps ϕ : Sub( A ) → Sub( A ) and {|ϕ|} : P(Γ A ) → P(Γ A ) are Scott cocontinuous. The greatest fixpoint ν αϕ(α) can thus be interpreted, both in Set and S, using Kleene's Fixpoint Theorem, as the infs of the interpretations of ϕ m ( ) for m ∈ N. This leads to the expected coincidence of the two semantics for safe formulae.

x n {A | ϕ} iff xn(•) ∈ ϕ A (n) x n Fix(X).A iff unfold • x n A[Fix(X).A/X] x n T0 + T1 iff ∃i ∈ {0, 1}, ∃y ∈ Γ |Ti| , x = ini • y and y n Ti x n T0 × T1 iff π0 • x n T0 and π1 • x n T1 x n 1 x n U → T iff ∀k ≤ n, ∀y ∈ Γ |U | , y k U =⇒ ev • x, y k T x n+1 T iff ∃y ∈ Γ |T | , x = next • y and y n T x 1 T x n T iff ∀m > 0, xn(•) m T (where x ∈ Γ | T | ) x n ∀k • T iff x n T [t/k]
for all closed iteration terms t Fig. [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF]. The Realizability Semantics.

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 (ν-I) and (µ-E) of Fig.

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 Cons g a s and write [] g for the empty colist Nil g . Moreover, we use some syntactic sugar for pattern matching, e.g. assuming s :

CoList g A we write case s of ([] g → N |x :: g xs → M ) for case(unfold s) of (y.N [ /y]|y.M [π 0 (y)/x , π 1 (y)/xs]). Most of the append : CoList A -→ CoList A -→ CoList A := λs.λt. boxι(append g (unbox s) (unbox t)) append g : CoList g A → CoList g A → CoList g A := fix(g).λs.λt.case s of | [] g → t | x :: g xs → x :: g (g xs (next t)) sched : Res A -→ Res A -→ Res A := λp.λq. boxι(sched g (unbox p) (unbox q)) sched g : Res g A -→ Res g A -→ Res g A := fix(g).λp.λq. case p of | Ret g a → Ret g a | Cont g k → let h = λi. let o, t = ki in o, g (next q) t in Cont g h diag := λs.boxι diag g (unbox s) : Str(Str A) -→ Str A diag g := diagaux g (λx.x) : Str g (Str A) -→ Str g A diagaux g : (Str A → Str A) -→ Str g (Str A) -→ Str g A := fix(g).λt.λs. Cons g (hd • t)(hd g s) g next(t • tl) (tl g s) fb : CoNat -→ CoNat -→ Str Bool := λc.λm. boxι(fb g (unbox c) (unbox m)) fb g : CoNat g -→ CoNat g -→ Str g Bool := fix(g).λc.λm. case c of | Z g → ff :: g g (next m) next(S g (next m)) | S g n → tt :: g g n (next m) extract : Rou g (CoList g A) -→ CoList g A := fix(g).λc. case c of | Over g → Nil g | Cont g f → f g unfold : Rou g A -→ ( Rou g A → A) -→ A := λc. case c of | Over g → λk. k (next Over g ) | Cont g f → λk. next(f k) bft g := λt. extract (bftaux t Over g ) : Tree g A -→ CoList g A bftaux : Tree g A -→ Rou g (CoList g A) -→ Rou g (CoList g A) := fix(g).λt.λc. Cont λk. (label g t) :: g unfold c k • (g (son g t)) • (g (son g r t))
Table 3. Code of the Examples.

functions of Table 3 are obtained from usual recursive definitions by inserting and next at the right places. We often write ψ → ϕ for [ev(ψ)]ϕ. Table 4 recaps our main examples of refinement typings, all of which (for A, B, O, I constant, I finite and ϕ, ψ safe and smooth) can be derived syntactically for the functions of Table 3. We use intermediate typings requiring iteration terms whenever a 3 is involved. Below, "Γ M satisfies ϕ" means Γ M ∈ {|ϕ|} (modulo Γ ∆ Id Set , see §7). We refer to §E for details.

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

∀k•∀ • CoList g A 3 k [nil] → CoList g A 3 [nil] → CoList g A 3 k+ [nil]
In addition, if the first argument of Γ append has an element which satisfies ϕ, then the result has an element which satisfies ϕ. The same holds if the first argument is finite while the second one has an element which satisfies ϕ.

Map over coinductive streams (with either 2, 3, 32 or 23)

map : ({B | ψ} → {A | ϕ}) -→ {Str B | [box] [hd]ψ} -→ {Str A | [box] [hd]ϕ} Diagonal of coinductive streams of streams (with either 2 or 32) diag : {Str(Str A) | [box] [hd][box]2[hd]ϕ} -→ {Str A | [box] [hd]ϕ}
A fair stream of Booleans (adapted from [START_REF] Cave | Fair Reactive Programming[END_REF][START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF]) [START_REF] Jones | Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips[END_REF] or with Hofmann's algorithm (see e.g. [START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]))

fb : CoNat -→ CoNat -→ Str Bool fb 0 1 : {Str Bool | [box]23[hd][tt] ∧ [box]23[hd][ff]} Append on guarded recursive colists append g : {CoList g A | [¬nil]} -→ CoList g A -→ {CoList g A | [¬nil]} append g : CoList g A -→ {CoList g A | [¬nil]} -→ {CoList g A | [¬nil]} Append on coinductive colists append : {CoList A | [box]3[hd]ϕ} -→ CoList A -→ {CoList A | [box]3[hd]ϕ} append : {CoList A | [box]3[nil]} -→ {CoList A | [box]3[hd]ϕ} -→ {CoList A | [box]3[hd]ϕ} append : {CoList A | [box]3[nil]} -→ {CoList A | [box]3[nil]} -→ {CoList A | [box]3[nil]} Breadth-first tree traversal bft g : {Tree g C | ∀2[lbl]ϑ} -→ {CoList g C | 2[hd]ϑ} (à la
A scheduler of resumptions (adapted from [48])

sched : {Res A | [box]3[Ret]} -→ {Res A | [box]3[Ret]} -→ {Res A | [box]3[Ret]} sched : {Res A | [box]3[now]ψ} -→ {Res A | [box]3[now]ψ} -→ {Res A | [box]3[now]ψ} sched : {Res A | [box]23[Ret]} -→ {Res A | [box]23[Ret]} -→ {Res A | [box]23[Ret]} sched : {Res A | [box]23[out]ϑ} -→ {Res A | [box]23[out]ϑ} -→ {Res A | [box]23[out]ϑ} (where 3 is either ∀3 or ∃3, 2 is either ∀2 or ∃2, and [out] is either [∧out] or [∨out])
Table 4. Some Refinement Typings (functions defined in Table 3).

Example 8.2 (The Map Function on Streams).

The composite modalities 23 and 32 over streams are read resp. as "infinitely often" and "eventually always". Provided with a function f : Γ B → Γ A taking b ∈ Γ B satisfying ψ to f (b) ∈ Γ B satisfying ϕ, the function Γ map on set-theoretic streams returns a stream which infinitely often (resp. eventually always) satisfies ϕ whenever its stream argument infinitely often (resp. eventually always) satisfies ψ.

Example 8.3 (The Diagonal Function). Consider a stream of streams s. We have

s = (s i | i ≥ 0) where each s i is itself a stream s i = (s i,j | j ≥ 0). The diagonal of s is then the stream (s i,i | i ≥ 0). Note that s i,i = hd(tl i (hd(tl i (s))). Indeed, tl i (s) is the stream of streams (s k | k ≥ i), so that hd(tl i (s)) is the stream s i and tl i (hd(tl i (s))) is the stream (s i,k | k ≥ i).
Taking its head thus gives s i,i . In the diag function of Table 3, the auxiliary higher-order function diagaux g iterates the coinductive tl over the head of the stream of streams s. We write • for function composition, so that assuming s : Str g (Str A) and t : Str A → Str A, we have (on the coinductive type Str A), (hd g s) : Str A and

(hd • t) : Str A → A (hd • t)(hd g s) : A (t • tl) : Str A → Str A
The expected refinement types for diag (Table 4) say that if its argument is a stream whose component streams all satisfy 2ϕ, then Γ diag returns a stream whose elements all satisfy ϕ. Also, if the argument of Γ diag is a stream such that eventually all its component streams satisfy 2ϕ, then it returns a stream which eventually always satisfies ϕ. See §E.4 for details.

Example 8.4 (A Fair Stream of Booleans). The non-regular stream (fb 0 1), adapted from [START_REF] Cave | Fair Reactive Programming[END_REF][START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF], is of the form ff

• tt • ff • tt 2 • ff • • • ff • tt m • ff • tt m+1 • ff • • •.
It thus contains infinitely many tt's and infinitely many ff's. We indeed have (see

§E.5 for details) (fb 0 1) : {Str Bool | [box]23[hd][tt] ∧ [box]23[hd][ff]}.
Example 8.5 (Resumptions). The type of resumptions Res g A (see Ex. 3.2) is adapted from [48]. Its guarded constructors are

Ret g := λa. fold(in 0 a) : A -→ Res g A Cont g := λk. fold(in 1 k) : (I → (O × Res g A)) -→ Res g A Ret g (a)
represents a computation which returns the value a : A, while Cont g f, k

(with f, k : I → (O × Res g A))
represents a computation which on input i : I outputs f i : O and continues with ki : Res g A. Given p, q : Res g A, the scheduler (sched g p q), adapted from [48], first evaluates p. If p returns, then the whole computation returns, with the same value. Otherwise, p evaluates to say Cont g f, k . Then (sched g p q) produces a computation which on input i : I outputs f i and continues with (sched g q (ki)), thus switching arguments.

Let I be a finite base type (so that Res g A is finitary polynomial). Let ψ : A, ϑ : O and ϕ : Res g A. We have the following formulae (where i : I):

[Ret] := [fold][in 0 ] [out i ]ϑ := [fold][in 1 ] ([i] → [π 0 ]ϑ) [now]ψ := [fold][in 0 ]ψ i ϕ := [fold][in 1 ] ([i] → [π 1 ][next]ϕ)
The formula [Ret] (resp.

[now]ψ) holds on a resumption which immediately returns (resp. with a value satisfying ψ) and we have Ret

g : A → {Res g A | [Ret]}, Ret g : {A | ψ} → {Res g A | [now]ψ}.
Moreover, the typings

Cont g : {I → (O × Res g A) | [i] → [π 0 ]ϑ} -→ {Res g A | [out i ]ϑ} Cont g : {I → (O × Res g A) | [i] → [π 1 ][next]ϕ} -→ {Res g A | i ϕ} express that [out i ]ϑ : Res g A is satisfied by Cont g f, k if f i satisfies ϑ, and that i ϕ : Res g A is satisfied by Cont g f, k if ki satisfies [next]ϕ.
Since I is a finite base type, it is possible to quantify over its inhabitants. We thus obtain CTL-like variants of 2 and 3 (Ex. 4.3.(b) and Ex. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF].3). Namely:

[∧out]ϑ := ∧ i∈I [out i ]ϑ : Res g A ϕ := ∧ i∈I i ϕ : Res g A [∨out]ϑ := ∨ i∈I [out i ]ϑ : Res g A ϕ := ∨ i∈I i ϕ : Res g ϕ ∀2ϕ := ν α. ϕ∧ α : Res g A ∀3ϕ := µα. ϕ∨ α : Res g A ∃2ϕ := ν α. ϕ∧ α : Res g A ∃3ϕ := µα. ϕ∨ α : Res g A
Our system can prove that Γ sched returns in finite time when so do its arguments, either along some or along any sequence of inputs. We moreover have expected 23 properties for all possible (consistent) combinations of ∃/∀ and [Ret]/[∨out]/[∧out] (Table 4, with ψ : A, ϑ : O safe and smooth). See §E.7.

Example 8.6 (Breadth-First Traversal). The function bft g of Table 3 (where g stands for λx.g x) implements Martin Hofmann's algorithm for breadth-first tree traversal. This algorithm involves the higher-order type Rou g A (see Ex. 3.2) with constructors Over g := fold(in 0 ) : Rou g A and

Cont g := λf.fold(in 1 f ) : ( Rou g A → A) → A → Rou g A
We refer to [START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF] for explanations. Consider a formula ϕ : A. We can lift ϕ to

[Rou]ϕ := ν α. [fold][in 1 ](([next]α → [next]ϕ) → ϕ) : Rou g A
We then easily derive the expected refinement type of bft g (Table 4, where ϑ : C).

Assume that ϑ is safe. On the one hand it is not clear what the meaning of [Rou]ϑ is, because it is an unsafe formula over a non-polynomial type. On the other hand, the type of bft g in Tab. 4 has its standard expected meaning (namely: if all nodes of a tree satisfy ϑ then so do all elements of its traversal) because the types Tree g C, CoList g C are polynomial and the formulae ∀2[lbl]ϑ, 2[hd]ϑ are safe. Hence, our system can prove standard statements via detours through nonstandard ones, which illustrates its compositionality. We have the same typing for a usual breadth-first tree traversal with forests (à la [START_REF] Jones | Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips[END_REF]). See §E.8.

Related Work

Type systems based on guarded recursion have been designed to enforce properties of programs handling coinductive types, like causality [START_REF] Krishnaswami | Ultrametric Semantics of Reactive Programs[END_REF], productivity [5, [START_REF] Møgelberg | A type theory for productive coprogramming via guarded recursion[END_REF][START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF][START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF][START_REF] Guatto | A Generalized Modality for Recursion[END_REF]27], or termination [START_REF] Spies | Transfinite Step-Indexing for Termination[END_REF]. 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 [START_REF] Jeffrey | LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs[END_REF][START_REF] Jeltsch | An Abstract Categorical Semantics for Functional Reactive Programming with Processes[END_REF] to the intuitionistic modal µ-calculus [START_REF] Cave | Fair Reactive Programming[END_REF]. 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 [48], or the absence of time leaks, with the Fitch-style system of [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF]. This more recently lead [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF] to consider liveness properties with an FRP approach based on guarded recursion. In this system, the guarded λ-calculus (presented in a Fitch-style type system) is extended with a delay modality (written ) 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. 3, 32, 23) are uniformly handled with the same -type, which is moreover the expected one in the guarded λ-calculus [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF].

Higher-order model checking (HOMC) [START_REF] Ong | On Model-Checking Trees Generated by Higher-Order Recursion Schemes[END_REF][START_REF]7 The Safe Fragment[END_REF] has been introduced to check automatically that higher-order recursion schemes, a simple form of higher-order programs with finite data-types, satisfy a µ-calculus formula. Automatic verification of higher-order programs with infinite data-types (integers) has been explored for safety [44], termination [50], and more generally ω-regular [START_REF] Murase | Temporal Verification of Higher-Order Functional Programs[END_REF] properties. In presence of infinite datatypes, semi-automatic extensions of HOMC have recently been proposed [START_REF] Watanabe | Reduction from Branching-Time Property Verification of Higher-Order Programs to HFL Validity Checking[END_REF]. In contrast with this paper, most HOMC approaches do not consider input-output behaviors on coalgebraic data. A notable exception is [45,[START_REF] Fujima | Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes[END_REF], but it does not handle higher-order functions (such as map), nor polynomial types such as Str(Str A) (Ex. [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF].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 [66], which can be checked for temporal properties with algorithms based on (HO)MC [START_REF] Hofmann | Abstract interpretation from büchi automata[END_REF][START_REF] Hofmann | A cartesian-closed category for higher-order model checking[END_REF], or, in presence of infinite datatypes, with refinement type systems [START_REF] Koskinen | Local Temporal Reasoning[END_REF][START_REF] Nanjo | A Fixpoint Logic and Dependent Effects for Temporal Property Verification[END_REF]. Our iteration terms can be seen as oracles, as required by [START_REF] Koskinen | Local Temporal Reasoning[END_REF] to handle liveness properties, but we do not know if they allow for the non-regular specifications of [START_REF] Nanjo | A Fixpoint Logic and Dependent Effects for Temporal Property Verification[END_REF]. 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 [69], which also handles universal and existential properties on traces. This framework can handle CTL-like properties of the form ∃/∀-2/3 (with our notation of Ex. 8.5), but not nested combinations of these (as e.g. ∃2∀3 for sched in Ex. 8.5). It moreover does not handle coinductive types.

Conclusion and Future Work

We have presented a refinement type system for the guarded λ-calculus, with refinements expressing temporal properties stated as (alternation-free) µ-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: [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF] 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 [START_REF] Bizjak | Guarded Dependent Type Theory with Coinductive Types[END_REF][START_REF] Birkedal | Guarded cubical type theory[END_REF][START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]27]. 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 [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF][START_REF] Birkedal | Modal dependent type theory and dependent right adjoints[END_REF], since it is not known how to extend delayed substitutions to dependent types while retaining decidability of type-checking [START_REF] Bizjak | Denotational semantics for guarded dependent type theory[END_REF]. Also, it is appealing to investigate the generalization of our approach to sized types [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF], in which guarded recursive types are representable [START_REF] Veltri | Guarded Recursion in Agda via Sized Types[END_REF].

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

{Str g C | 32[hd]ϑ} → {Str g B | 32[hd]ψ} can be postcomposed with one of type {Str g B | 23[hd]ψ} → {Str g A | 23[hd]ϕ} (since 32[hd]ψ ⇒ 23[hd]ψ).
Hence, we expect that some automation is possible for fragments of our logic. In presence of iteration terms, arithmetic extensions of the µ-calculus [START_REF] Kobayashi | Temporal Verification of Programs via First-Order Fixpoint Logic[END_REF]42] 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 {Str g A | 23[hd]ϕ}. This might provide automation for fragments of the guarded λ-calculus. Besides, the combination of refinement types with automatic techniques like predicate abstraction [START_REF] Rondon | Liquid Types[END_REF], abstract interpretation [START_REF] Jhala | HMC: Verifying functional programs using abstract interpreters[END_REF], or SMT solvers [START_REF] Vazou | Refinement Types for Haskell[END_REF][START_REF] Vazou | Liquid Haskell: Haskell as a theorem prover[END_REF] has been particularly successful. More recently, the combination of refinement types inference with HOMC has been investigated [64].

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 [60], that provides a general framework to reason on effectful computations, as shown by interaction trees [START_REF] Xia | Interaction Trees: Representing Recursive and Impure Programs in Coq[END_REF]. 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 [START_REF] Ahmed | Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types[END_REF] for typed higher-order effectful programming languages. Program logics for reasoning on such logical relations [START_REF] Dreyer | Logical Step-Indexed Logical Relations[END_REF][START_REF] Dreyer | A Relational Modal Logic for Higher-order Stateful ADTs[END_REF] uses this representation of step-indexing via guarded recursion. It is also found in Iris [40], 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. A Additional Material for §3 (The Pure Calculus)

(x : A) ∈ E E x : A E, x : B M : A E λx.M : B → A E M : B → A E N : B E M N : A E : 1 E M0 : A0 E M1 : A1 E M0, M1 : A0 × A1 E M : Ai E ini(M ) : A0 + A1 for i ∈ {0, 1}, E M : A0 + A1 E, x : Ai Ni : B E case M of (x.N0|x.N1) : B E M : A0 × A1 E πi(M ) : Ai E, x : A M : A E fix(x).M : A E M : A[Fix(X).A/X] E fold(M ) : Fix(X).A E M : Fix(X).A E unfold(M ) : A[Fix(X).A/X] E M : (B → A) E N : B E M N : A E M : A E next(M ) : A x1 : A1, . . . , xk : Ak M : A E Mi : Ai with Ai constant for 1 ≤ i ≤ k E prev [x1 →M1,...,x k →M k ] (M ) : A x1 : A1, . . . , xk : Ak M : A E Mi : Ai with Ai constant for 1 ≤ i ≤ k E box [x1 →M1,...,x k →M k ] (M ) : A E M : A E unbox(M ) : A
The typing rules for our pure calculus (i.e. the guarded λ-calculus of [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF]) are given in Fig. 14.

B Additional Material for §4 (A Temporal Modal Logic)

Figure 15 presents the definition of the variance predicates α Pos ϕ and α Neg ϕ for the full logical language ( §4 and §6). The intuitionistic propositional deduction rules are given in Fig. 16.

Remark B.1. All modalities ([π i ], [fold], [next], [in i ],
[ev(ψ)] and [box]) satisfy the monotonicity rule (RM) and are thus monotone in the sense of [START_REF] Chellas | Modal Logic: An Introduction[END_REF], from which we borrowed the terminology used in Table 2 (see also [29,[START_REF] Frittella | Monotone Modal Logics & Friends[END_REF]). Assuming the rule (RM), we easily get the following:

(a) Axiom (N) implies the usual necessitation rule:

ϕ [ ]ϕ (RN)
Proof. Indeed, one can derive Proof. Indeed, one has

(N) [ ] ϕ ⇒ ϕ (RM) [ ] ⇒ [ ]ϕ [ ]ϕ (b) Axiom (C) implies the usual axiom (K): [ ](ϕ ⇒ ψ) =⇒ ([ ]ϕ ⇒ [ ]ψ) α Pos α α = β α Pos β α Pos α Pos ⊥ α Pos ϕ α Pos ψ α Pos ϕ ∨ ψ α Pos ϕ α Pos ψ α Pos ϕ ∧ ψ α Neg ψ α Pos ϕ α Pos ψ ⇒ ϕ α Pos ϕ α Pos [πi]ϕ α Pos ϕ α Pos [ini]ϕ α Pos ϕ α Pos [fold]ϕ α Pos ϕ α Pos [next]ϕ α Neg ψ α Pos ϕ α Pos [ev(ψ)]ϕ α Pos ϕ α = β α Pos ν βϕ α Pos ϕ α = β α Pos µβϕ α Pos ϕ α = β α Pos ν t βϕ α Pos ϕ α = β α Pos µ t βϕ α = β α Neg β α Neg α Neg ⊥ α Neg ϕ α Neg ψ α Neg ϕ ∨ ψ α Neg ϕ α Neg ψ α Neg ϕ ∧ ψ α Pos ψ α Neg ϕ α Neg ψ ⇒ ϕ α Neg ϕ α Neg [πi]ϕ α Neg ϕ α Neg [ini]ϕ α Neg ϕ α Neg [fold]ϕ α Neg ϕ α Neg [next]ϕ α Pos ψ α Neg ϕ α Neg [ev(ψ)]ϕ α Neg ϕ α = β α Neg ν βϕ α Neg ϕ α = β α Neg µβϕ α Neg ϕ α = β α Neg ν t βϕ α Neg ϕ α = β α Neg µ t βϕ
(ϕ ⇒ ψ) ∧ ϕ =⇒ ψ (RM) [ ] (ϕ ⇒ ψ) ∧ ϕ =⇒ [ ]ψ (C) [ ](ϕ ⇒ ψ) ∧ [ ]ϕ =⇒ [ ]ψ [ ](ϕ ⇒ ψ) =⇒ ([ ]ϕ ⇒ [ ]ψ) (c) We have the monotonicity axioms [ ](ϕ ∧ ψ) =⇒ [ ]ϕ ∧ [ ]ψ [ ]ϕ ∨ [ ]ψ =⇒ [ ](ϕ ∨ ψ)
In our context, the normal intuitionistic modal logic IK of [START_REF] Plotkin | A Framework for Intuitionistic Modal Logics: Extended Abstract[END_REF] [START_REF] Blackburn | Modal Logic. Cambridge Tracts in Theoretical Computer Science[END_REF]).

is (RM) + (C) + (N) + (P) + (C ∨ ) + (C ⇒ ), while the normal modal logic K is IK + (CL) (see e.g.

C Additional Material for §5 (A Temporally Refined

Type System)

The definition of the subtyping relation ≤ for the full system ( §5 and §6) is given in Fig. 17. [START_REF] Blackburn | Modal Logic. Cambridge Tracts in Theoretical Computer Science[END_REF]. Intuitionistic Propositional Deduction Rules. The underlying pure type |T | of a refinement type T is inductively defined as follows:

A ϕ ∨ ϕ ⇒ ϕ A ϕ ⇒ ϕ ∧ ϕ A ϕ ⇒ ϕ ∨ ψ A ϕ ∧ ψ ⇒ ϕ A ϕ ∨ ψ ⇒ ψ ∨ ϕ A ϕ ∧ ψ ⇒ ψ ∧ ϕ A ϕ ∧ ψ ⇒ θ A ϕ ⇒ (ψ ⇒ θ) A ϕ ⇒ (ψ ⇒ θ) A ϕ ∧ ψ ⇒ θ A ϕ A ϕ ⇒ ψ A ψ A ϕ ⇒ ψ A ψ ⇒ θ A ϕ ⇒ θ A ⊥ ⇒ ϕ A ϕ ⇒ ψ A θ ∨ ϕ ⇒ θ ∨ ψ Fig.
T ≤ T T ≤ U U ≤ V T ≤ V T ≤ U T ≤ U U ≤ T U ≤ T T0 ≤ U0 T1 ≤ U1 T0 × T1 ≤ U0 × U1 T0 ≤ U0 T1 ≤ U1 T0 + T1 ≤ U0 + U1 U0 ≤ T0 T1 ≤ U1 T0 → T1 ≤ U0 → U1 T ≤ |T | A ≤ {A | } A ϕ ⇒ ψ {A | ϕ} ≤ {A | ψ} {B | ψ} → {A | ϕ} ≡ {B → A | [ev(ψ)]ϕ} {A | ϕ} ≡ { A | [next]ϕ} ∀k • T ≡ ∀k • T ϕ safe {A | ϕ} ≡ { A | [box]ϕ} A c ϕ ⇒ ψ { A | [box]ϕ} ≤ { A | [box]ψ}
|A| := A | {A | ϕ} | := A |∀k • T | := |T | |T + U | := |T | + |U | |T × U | := |T | × |U | |U → T | := |U | → |T | | T | := |T | | T | := |T | D Additional Material for §7 (Semantics)
This Appendix presents material that we omitted in §7 for space reasons. We follow roughly the same plan. Most proofs a deferred to App. F. We often use θ as a generic notation for µ and ν.

D.1 The Topos of Trees (Basic Structure)

Note D. [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF]. Given an object X of S and 0 < k ≤ n, we write t↑k for the restriction of t ∈ X(n) into X(k), obtained by composing restriction functions r X i for i = k, . . . , n -1.

Full definitions and proofs of the semantic require the explicit manipulation of some of the structure of S. We refer to [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF][START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF] for details.

First, as in any presheaf category, limits and colimits are computed pointwise. In particular binary sums and products are given by

(X + Y )(n) = X(n) + Y (n) (X × Y )(n) = X(n) × Y (n)
Moreover, exponentials are induced by the Yoneda Lemma (see e.g. [52, §I.6]). Explicitly, given S object X and Y , the exponent Y X at n is the set of all sequences (f ) ≤n of functions f : X( ) → Y ( ) which are compatible with restriction (i.e.

r Y • f +1 = f • r X ).
The morphism fix X : X X → X is defined as

fix X n ((f m ) m≤n ) := (f n • • • • • f 1 )(•) The morphism fix X : X X → X is natural in X. Given f : X × Y → X with exponential transpose f t : Y → X X , the morphism fix X • f t : Y → X is unique such that fix X • f t = f • next X • fix X • f T , id X ([13, Thm. 2.4]).
Since we do not require the explicit constructions, we refer to [START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF] for the interpretation of guarded recursive types Fix(X).A(X) and for the definition of the isos fold : A(Fix(X).A(X)) -→ Fix(X).A(X) unfold :

Fix(X).A(X) -→ A(Fix(X).A(X))

We now have all the structure we need for the denotational semantics of the -free fragment of the pure calculus.

D.2 Global Sections and Constant Objects

As for any presheaf topos, the global section functor Γ : S → Set is right adjoint to the constant object functor ∆ : Set → S (see e.g. [52, §I.6]):

S Γ * * Set ∆ i i
We record the following easy well-known facts for later use.

Lemma D. [START_REF] Ahmed | Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types[END_REF]. Given a set S and given X, Y objects of S, we have in Set:

(1) the unit η : Id Set → Γ ∆ of ∆ Γ is an iso, (2) Γ (X × Y ) Γ X × Γ Y and Γ 1 1 (3) Γ (X + Y ) Γ X + Γ Y (4) Γ (X ∆S ) (Γ X) S (5) Γ ( X) Γ X (via Γ (next))
where all the mentioned isos are natural in X and Y (when applicable).

Proof.

(1) The unit η S of ∆ Γ at S takes a ∈ S to the constant map (n

→ (• → a)) ∈ S[1, ∆S]. Its inverse is the function S[1, ∆S] → S taking a constant map x ∈ S[1, ∆S] to x(0)(•). (2) Since Γ is a right adjoint. (3) Since for any x ∈ S[1, X + Y ] there is some i ∈ {0, 1} such that x(•)(n) is of the form in i (x n ) for all n ∈ N. (4) Using the Cartesian closed structure of S and the adjunction ∆ Γ we have Γ (X ∆S ) = S[1, X ∆S ] S[1 × ∆S, X] S[∆S, X] Set[S, Γ X] (5) We show that x ∈ Γ X → next • x ∈ Γ ( X) is a bijection. We first show surjectivity. Consider x ∈ S[1, X]. Then for each n ∈ N, we have x n+1 (•) ∈ X(n+1) = X(n) with x n+2 (•)↑ = x n+1 (•). This defines a map x ∈ S[1, X] as x n (•) := x n+1 (•). Moreover, (next 0 • x 0 )(•) = • = x 0 (•) and (next n+1 • x n+1 )(•) = x n+1 (•)↑ = x n+2 (•)↑ = x n+1 (•)
We now show injectivity. Let x, y ∈ S[1, X] and assume next • x = next • y : 1 → S X. Then for all n we have x n+1 (•)↑ = y n+1 (•)↑ and thus x n (•) = y n (•).

Following [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF], for a (closed) pure type A, we have

A := ∆Γ A
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>0 describing a unique global section

x n+1 (•) = x n (•) ∈ Γ A .
The term constructor unbox(-) is interpreted as the counit ε of the adjunction ∆ Γ : given E M : A, we let unbox(M ) be the composite

E M -→ A = ∆Γ A ε -→ A
The term constructors box and prev rely on a strong semantic property of constant types, namely that their interpretation lie (modulo isomorphism) in the image of the constant object functor ∆.

Definition D.3 ([20, Def. 2.2]). An object X of S is constant if X ∆S for some set S.
Note that the restriction maps of constant objects are bijections. Similarly as in [20, Def. [START_REF] Ahmed | Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types[END_REF].2], if x ∈ X(n) with X constant, then we write x ∈ X(k) for the unique element of X(k) which is equal to x modulo the bijective restriction maps of X.

Lemma D.4 ([20, Lem. 2.6]). If A is a constant (pure) type, then A is a constant object of S.
We now give the interpretations of box σ (M ) and prev σ (M ) (where σ stands for

[x 1 → M 1 , . . . , x k → M k ]). Assuming in both cases M to be defined, for n > 0 we let box σ (M ) (n) : E (n) -→ ∆Γ A (n) = Γ A γ -→ m → M m M 1 n (γ) , . . . , M k n (γ) prev σ (M ) (n) : E (n) -→ A (n) = A (n + 1) γ -→ M n+1 M 1 n (γ) , . . . , M k n (γ)
where the mismatches between n and m and between n and n + 1 are legal since A 1 , . . . , A k are constant by Lem. D.4.

D.3 External and Internal Semantics: Global Definitions

We can now give the full Set and S interpretations of the logical language. In both cases, for α : A ϕ : A(α), we let

ϕ 0 ( ) := ϕ m+1 ( ) := ϕ(ϕ m ( )) ϕ 0 (⊥) := ⊥ ϕ m+1 (⊥) := ϕ(ϕ m (⊥))
(Recall that θ t αϕ is only allowed when ϕ as at most α as free variable.) Definition D.5 (External Semantics). Consider a formula α 1 : A 1 , . . . , α k : A k ϕ : A without free iteration variable. Assume given a valuation v taking each propositional variable α i for i = 1, . . . , k to a set v(α i ) ∈ P(Γ A i ). We define {|ϕ|} A v ∈ P(Γ A ) by induction on ϕ in Fig. [START_REF] Cave | Fair Reactive Programming[END_REF].

As for the internal S semantics -, we give a global definition, in a form similar to Def. D.5.

Definition D.6 (Internal Semantics). Consider a formula α

1 : A 1 , . . . , α k : A k ϕ : A without free iteration variable. Assume given a valuation v taking each propositional variable α i for i = 1, . . . , k to a subobject v(α i ) of A i . The subobject ϕ A v of
A is defined by induction on ϕ in Fig. [START_REF] Chellas | Modal Logic: An Introduction[END_REF].

The correctness of Def. D.6, namely that we indeed have ϕ A ∈ Sub( A ), as well as the correspondence with the presentation of §7 are discussed in App. D. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]. [START_REF] Cave | Fair Reactive Programming[END_REF]. External Semantics. Remark D. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF]. For closed formulae we can rephrase Def. D.6 as t ∈ ϕ A (n) iff t A n ϕ, where the forcing relation t A n ϕ is inductively defined as follows.

{|⊥|} A v := ∅ {| |} A v := Γ A {|αi|} A v := v(αi) {|ϕ ∨ ψ|} A v := {|ϕ|} A v ∪ {|ψ|} A v {|ϕ ∧ ψ|} A v := {|ϕ|} A v ∩ {|ψ|} A v {|ψ ⇒ ϕ|} A v := Γ A \ {|ψ|} A v ∪ {|ϕ|} A v {|[πi]ϕ|} A 0 ×A 1 v := x ∈ Γ A0 × A1 πi • x ∈ {|ϕ|} A i v {|[ini]ϕ|} A 0 +A 1 v := x ∈ Γ A0 + A1 ∃y ∈ Γ Ai x = ini • y and y ∈ {|ϕ|} A i v {|[fold]ϕ|} Fix(X).A v := x ∈ Γ Fix(X).A unfold • x ∈ {|ϕ|} A[Fix(X).A/X] v {|[ev(ψ)]ϕ|} B→A v := x ∈ Γ B → A ∀y ∈ Γ B , y ∈ {|ψ|} B v =⇒ ev • x, y ∈ {|ϕ|} A v {|[box]ϕ|} A := x ∈ Γ A x1(•) ∈ {|ϕ|} A {|[next]ϕ|} A v := next • x ∈ Γ A x ∈ {|ϕ|} A v {|ν t αϕ(α)|} A v := {|ϕ m ( )|} A v ( t = m) {|µ t αϕ(α)|} A v := {|ϕ m (⊥)|} A v ( t = m) {|ν αϕ|} A v := S S ∈ P(Γ A ) and S ⊆ {|ϕ|} A v[S/α] {|µαϕ|} A v := S S ∈ P(Γ A ) and {|ϕ|} A v[S/α] ⊆ S Fig.
⊥ A v (n) := ∅ A v := A αi A v := v(αi) ϕ ∨ ψ A v (n) := ϕ A v (n) ∪ ψ A v (n) ϕ ∧ ψ A v (n) := ϕ A v (n) ∩ ψ A v (n) ψ ⇒ ϕ A v (n) := t ∈ A (n) ∀k ≤ n, t↑k ∈ ψ A v (k) =⇒ t↑k ∈ ϕ A v (k) [πi]ϕ A 0 ×A 1 v (n) := t ∈ A0 × A1 (n) πi(t) ∈ ϕ A i v (n) [ini]ϕ A 0 +A 1 v (n) := t ∈ A0 + A1 (n) ∃u ∈ Ai (n), t = ini(u) and u ∈ ϕ A i v (n) [fold]ϕ Fix(X).A v (n) := t ∈ Fix(X).A (n) unfoldn(t) ∈ ϕ A[Fix(X).A/X] v (n) [ev(ψ)]ϕ B→A v (n) := t ∈ B → A (n) ∀k ≤ n, ∀u ∈ B (k), u ∈ ψ B v (k) =⇒ (t↑k)(u) ∈ ϕ A v (k) [box]ϕ A (n) := t ∈ A (n) = Γ A t ∈ {|ϕ|} A [next]ϕ A v (1) := 1 [next]ϕ A v (n) := ϕ A v (n -1) (n > 1) ν t αϕ(α) A v := ϕ m ( ) A v ( t = m) µ t αϕ(α) A v := ϕ m (⊥) A v ( t = m) ν αϕ A v := S S ∈ Sub( A ) and S ≤ ϕ A v[S/α] µαϕ A v := S S ∈ Sub( A ) and ϕ A v[S/α] ≤ S
-t A n ⊥. -t A n . -t A n ϕ ∨ ψ iff t A n ϕ or t A n ψ. -t A n ϕ ∧ ψ iff t A n ϕ and t A n ψ. -t A n ψ ⇒ ϕ iff for all k ≤ n, t↑k A k ϕ whenever t↑k A k ψ. -t A0×A1 n [π i ]ϕ iff π i (t) Ai n ϕ. -t A0+A1 n [in i ]ϕ iff there is u ∈ A i (n) such that t = in i (u) and u Ai n ϕ. -t B→A n [ev(ψ)]ϕ iff for all k ≤ n and all u ∈ B (k), (t↑k)(u) A k ϕ whenever u B k ψ. -t Fix(X).A n [fold]ϕ iff unfold • t A[Fix(X).A/X] n ϕ. -t A 0 [next]ϕ. -t A n+1 [next]ϕ iff t A n ϕ. -t A n [box]ϕ iff t ∈ {|ϕ|} A .

D.4 An Open Geometric Morphism

Key properties of the internal semantics of [box] rely on some further facts on the adjunction ∆ Γ . We refer to [START_REF] Lane | Sheaves in geometry and logic: A first introduction to topos theory[END_REF][START_REF] Johnstone | Sketches of an Elephant: A Topos Theory Compendium[END_REF].

The functor ∆ : Set → S preserves limits (in particular, ∆ Γ : S → Set is a geometric morphism). It follows that ∆ preserves monos, so that for each set S the function

A ∈ P(S) -→ ∆A ∈ Sub(∆S)
is a meet preserving (and thus monotone) map. It is easy to see that this map has a posetal left adjoint f ! : Sub(∆S) -→ P(S)

Proof. A subobject A of ∆S is a family of subsets A = (A n ) n with A n ⊆ S.
Hence we can let f ! (A) ∈ P(S) be the set of all a ∈ S such that a ∈ A n for some n > 0. Then assuming f ! (A) ⊆ B for some set B ∈ P(S), it follows that if a ∈ A n then a ∈ f ! (A) ⊆ B so that a ∈ (∆B) n and thus A ≤ ∆B. Conversely, if A ≤ ∆B, then for every a ∈ f ! (A), since a ∈ A n for some n > 0, we must have a ∈ (∆B

) n = B, so that f ! (A) ⊆ B.
As a consequence, the adjoint pair ∆ Γ : S → Set is an open geometric morphism (in the sense of [52, Def. IX. 6.2]), from which it follows that ∆ induces maps of (complete) Heyting algebras P(S) → Sub(∆S) (see e.g. [52, Thm. X.3.1 & Lem. X.3.2]). We state this for later use.

Lemma D. [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF]. For each set S, the functor ∆ induces a map of (complete) Heyting algebras P(S) → Sub(∆S).

This means that the Set interpretation {|ϕ|} ∈ P(Γ A ) can be taken to the subobject ∆ {|ϕ|} ∈ Sub(∆Γ A ) = Sub( A ) in S while respecting the usual Set semantics of logical connectives. In particular, we can allow the logical theory under a [box] to be classical, while the S semantics imposes the ambient logical theory to be intuitionistic.

D.5 Abstract Modalities

We present here some well-known basic material which will help us proving the correctness of the internal and external semantics. Definition D. [START_REF] Baier | Principles of Model Checking[END_REF]. Let C be a category with pullbacks and consider a morphism k : X → C Y .

-The functor k * : C/Y → C/X is defined by pullbacks

A / / k * (g) A g X k / / Y -The functor (∃k) : C/X → C/Y is defined by postcomposition: (g : A → X) -→ (k • g : A → Y )
The following is a basic property of toposes. (1) The map (∃in i ) : Set/S i → Set/(S 0 + S 1 ) induces a map P(S i ) → P(S 0 + S 1 ).

(2) The map (∃in i ) : S/X i → S/(X 0 +X 1 ) induces a map Sub(X i ) → Sub(X 0 + X 1 ).

Proof. Since in both cases the morphism in i is a mono.

Lemma D. [START_REF] Birkedal | Modal dependent type theory and dependent right adjoints[END_REF]. The map S/X → S/ X taking g : Y → X to (g) : Y → X induces a map Sub(X) → Sub( X).

Proof. The functor preserves limits since it has a left adjoint ([13, §2.1]). It thus follows that preserves monos.

D.6 External and Internal Semantics: Local Definitions

Some key properties of the Set and S interpretations are easier to get if one goes through a local presentation, as operations on subobject and powerset lattices, similar to that of -in §7. The goal is to pave the way toward the correctness of both semantics: Lemma D.13 (Lem. 7.2). The following holds w.r.t. the full modal theories of Def. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]

.2. (1) If

A c ϕ then {|ϕ|} = Γ A . (2) If A ϕ then ϕ = A .
The detailed proof of Lem. D.13 is deferred to App. F. [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF]. It relies on the following material.

Internal Semantics We use the material of §D.5 to devise operations on subobject lattices corresponding to our modalities. This formally extends the presentation given in §7.

Definition D.14.

(a) Given S-objects X 0 and X 1 , define (e) Given a set S, define [box] : P(S) → Sub(∆S) as ∆(-).

[π i ] : Sub(X i ) → Sub(X 0 × X 1 ) as π * i , where π i : X 0 × X 1 → S X i is the ith projection. (b) Given S-objects X 0 and X 1 , define [in i ] : Sub(X i ) → Sub(X 0 + X 1 ) as (∃in i ), where in i : X i → S X 0 + X 1 is the ith injection. (c)
We now discuss the case of [ev(ψ)]ϕ, which is actually interpreted as a logical predicate, in the categorical generalization of the usual sense discussed in [32, §9.2 & Prop. 9. 2.4]. We follow here [52, VI.5].

-First, extending the above discussion, for an object X of S, the (Heyting algebra) exponent

(-) ⇒ X (-) : Sub(X) × Sub(X) --→ Sub(X)
is given by

(A ⇒ X B)(n) = {t ∈ X(n) | ∀k ≤ n, t↑k ∈ A(k) =⇒ t↑k ∈ B(k)}
(see e.

A ∈ Sub(X × Y ), the presheaf ∀ Y (A) at n is {t ∈ X(n) | ∀k ≤ n, ∀u ∈ Y (k), (t↑k, u) ∈ A}
We therefore let, for each pure types A and B,

[ev(-)] : Sub( B ) -→ Sub( A ) → Sub( B → A ) take S ∈ Sub( B ) to [ev(S )] := S ∈ Sub( A ) -→ ∀ B π * (S ) ⇒ A B × B ev * (S)
where π : X Y × Y → X Y is a projection. Now, note that we actually have Lemma D. [START_REF] Bizjak | Denotational semantics for guarded dependent type theory[END_REF]. Consider a formula Σ ϕ : A and v as in Def. D.6, such that ϕ v ∈ Sub( A ). We have

(1) [π i ]ϕ v = [π i ] ( ϕ v ) (2) [in i ]ϕ v = [in i ] ( ϕ v ) (3) [fold]ϕ v = [fold] ( ϕ v ) (4) [next]ϕ v = [next] ( ϕ v ) (5) [box]ϕ = [box] ( ϕ ) (6) [ev(ψ)]ϕ v = [ev( ψ v )] ( ϕ v ) for each ψ : B such that ψ ∈ Sub( B ).
Proof.

(1) Since limits are computed pointwise in presheaves, we have

[π i ] ( ϕ Ai )(n) = {(t, u) ∈ A 0 × A 1 (n) × ϕ (n) | u = π i (t)} which is clearly in bijection with [π i ]ϕ A0×A1 (n).
(2) Trivial.

(3) Similar to the case of [π i ].

(4) Trivial.

(5) Trivial. (6) Immediate from the above discussion.

We thus have done almost all the work to obtain the following basic fact.

Lemma D. [START_REF] Blackburn | Modal Logic. Cambridge Tracts in Theoretical Computer Science[END_REF]. Given α 1 : A 1 , . . . , α k : A k ϕ : A, and v taking

α i for i = 1, . . . , k to v(α i ) ∈ Sub( A i ), we have ϕ A v ∈ Sub( A ).
Proof. The proof is by induction on formulae. The interpretation of the propositional connectives follows the corresponding structures in presheaf toposes [52, Prop. I. 8.5]. The cases of the modalities [ ] follow from the induction hypothesis and Lem. D. [START_REF] Bizjak | Denotational semantics for guarded dependent type theory[END_REF]. The cases of θαϕ simply amount to the fact that for presheaf toposes, subobjects lattices are complete ([52, Prop. I. [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF].5]). The cases of θ t αϕ for t an iteration term are trivial.

We now turn to the logical theory. We immediately get from the above:

Corollary D.17.

(1) The maps [π i ] ,

[fold] and [box] are maps of Heyting algebras.

(2) The maps [in i ] preserve ∨, ⊥ and ∧.

(3) The maps [next] preserve ∧, and ∨.

(4) For each object X of S and each fixed S ∈ Sub(X), the map [ev(S)] preserves ∧, .

Proof.

(1) This directly follows from Lem. D.10 and Lem. D.8.

(2) Preservation of ∨, ⊥ follows from that fact that [in i ] is a left adjoint by Lem. D. [START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]. For binary conjunctions, first note that meets in partial orders are given by pullbacks. In a subobject lattice Sub(X i ), this can be expressed as

A ∧ B / / B A / / X i
(where arrows are inclusions maps). Since in i : X i → X 0 + X 1 is a mono, the following is also a pullback in Sub(X 0 + X 1 ):

A ∧ B / / B X i ini A / / X i ini / / X 0 + X 1
(3) Preservation of ∧, follows from the fact that (-) is a right adjoint ([13, §2.1]). As for preservation of ∨, we check the details. Consider an object X of S and subobjects A, B ∈ Sub(X). We have to show (A∨B) = (A)∨ (B). But we have External Semantics We now turn to operations on powerset lattices for the external semantics.

(A ∨ B) 0 = 1 = 1 ∪ 1 = ( (A) ∨ (B)) 0 and (A ∨ B) n+1 = (A ∨ B) n = A n ∪ B n = (A) n+1 ∪ (B) n+1 = ( (A) ∨ (B)) n+1 (
Definition D. [START_REF] Cave | Fair Reactive Programming[END_REF].

(a) Given sets S 0 and S 1 , define {|[π i ]|} : P(S i ) → P(S 0 × S 1 ) as π * i , where π i : S 0 × S 1 → S i is the ith projection.

(b) Given sets S 0 and S 1 , define {|[in i ]|} : P(S i ) → P(S 0 + S 1 ) as (∃in i ), where in i :

S i → S 0 + S 1 is the ith injection. (c) Given a S object X, define {|[next]|} : P(Γ X) → P(Γ X) as ((Γ next) -1 ) * ,
where We trivially have (at appropriate types):

(Γ next) -1 : Γ ( X) → Γ X
{|[π i ]ϕ|} = {|[π i ]|} ({|ϕ|}) {|[in i ]ϕ|} = {|[in i ]|} ({|ϕ|}) {|[next]ϕ|} = {|[next]|} ({|ϕ|}) {|[fold]ϕ|} = {|[fold]|} ({|ϕ|})
Similarly as in Cor. D.17, we obtain the following.

Lemma D. [START_REF] Chellas | Modal Logic: An Introduction[END_REF].

D.7 The Safe Fragment

The property we use on safe formulae for Prop. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].3 is the following. Lemma D. [START_REF] Dreyer | Logical Step-Indexed Logical Relations[END_REF]. The greatest fixpoint of a Scott cocontinuous f : L → L is given by m∈N f m ( ).

Lemma D. [START_REF] Dreyer | A Relational Modal Logic for Higher-order Stateful ADTs[END_REF]. Given a safe formula α : A ϕ(α) : A, the following functions are Scott cocontinuous:

ϕ : Sub( A ) -→ Sub( A ) {|ϕ|} : P(Γ A ) -→ P(Γ A )
The key for Lem. D.22 is the usual fact that codirected infs commute with infs and finite sups, in Set as well as in S. The key case of Prop. 7.3 is that of ν αϕ(α) : A. We have

{|ν αϕ(α)|} = m∈N {|ϕ m ( )|} and ν αϕ(α) = m∈N ϕ m ( )
Given a global section x ∈ Γ ν αϕ(α) , we have

∀n > 0, ∀m ∈ N, x n (•) ∈ ϕ m ( ) (n)
We then easily conclude x ∈ {|ν αϕ(α)|} from {|ϕ m ( )|} = Γ ϕ m ( ) . Note that this relies on the commutation of the universal quantifications over n and m.

The proofs of Lem. D.21, Lem. D. [START_REF] Dreyer | A Relational Modal Logic for Higher-order Stateful ADTs[END_REF] and Prop. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].3 are deferred to App. F.2.

D.8 The Smooth Fragment

The proof of Lem. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].4 is deferred to App. F.3.

D.9 Constant Objects, Again

For the adequacy of the typing rules of the term constructors box and prev, we need to generalize Lem. D.4 ( §D.

2) to refinement types. To this end, it is convenient to extend the notation -to refinement types.

Definition D. [START_REF] Elliott | Functional Reactive Animation[END_REF]. For T is a type without free iteration variables, we define T by induction as follows:

{A | ϕ} := ϕ ∀k • T := n∈N T [n/k] T 0 + T 1 := T 0 + T 1 T 0 × T 1 := T 0 × T 1 U → T := U → T T := T T := ∆Γ T
We can now extend Lem. D.4. We crucially rely on the fact that ∆ preserves limits (see e.g. [START_REF] Johnstone | Sketches of an Elephant: A Topos Theory Compendium[END_REF]Ex. 4. 1.4

]).

Lemma D. 24. If T is a constant type, then T is a constant object of S.

Proof. The proof is by induction on types. The cases of the type constructors +, ×, → are easy and discussed in [20, Lem. 2.6]. In the case of Fix(X).A, since all occurrences of X in A should be guarded by a , and since can only be applied to closed types, it follows that X cannot occur in A. In particular ∆ : P(S) → Sub(∆S) preserves meets and we get

∀k • T = n T [n/k] n ∆S n n ∆f ! ∆S n ∆ ( n f ! ∆S n )
As for refinement types, we show by induction on ϕ : A with A constant that ϕ is a constant object.

Cases of , ⊥, ∧, ∨ and ⇒.

All these cases follow from (the induction hypothesis and) the fact that ∆ induces maps of Heyting algebras on subobject lattices (Lem. D.8). Case of [box]ϕ.

Trivial, since [box]ϕ is in the image of ∆.

unfold * ( ϕ ) [fold]ϕ π / / _ ϕ ∆(Φ) _ A unfold / / B ∆(S)
Since unfold is an iso, the upper arrow π is also an iso, and we are done.

Case of [π

i ]ϕ.
We rely on the description of [π i ]ϕ as [π i ] ( ϕ ) in §D. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]. By induction hypothesis and recalling that ∆ preserves finite products, consider the pullback

π * ( ϕ ) [π i ]ϕ / / _ ϕ ∆(Φ) _ ∆(S 0 ) × ∆(S 1 ) πi / / ∆(S i )
Then one can take the corresponding pullback in Set

Ψ / / _ Φ _ S 0 × S 1 πi / / S i and this implies that [π i ]ϕ ∆(Ψ ) since ∆ preserves finite limits. Case of [in i ]ϕ.
We rely on the description of [in i ]ϕ as [in i ] ( ϕ ) in §D. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]. The result follows from the induction hypothesis and the fact that ∆ preserves finite limits and colimits, as in:

ϕ ∆(Φ) → ∆(S i ) ∆(ini)=ini --→ ∆(S 0 ) + ∆(S 1 )
Case of [ev(ψ)]ϕ.

We rely on the description of [ev(ψ)]ϕ in §D.6, that is

[ev(ψ)]ϕ = ∀ B π * ( ψ ) =⇒ A B × B ev * ( ϕ )
The result then follows from Lem. D. By assumption, the occurrences of α in ϕ should be guarded by a [next].

Since [box] can only be applied to closed formulae, this imposes α not to appear in ϕ. But then the result follows by induction hypothesis.

D.10 Realizability

We detail the steps toward the Adequacy Theorem 7. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF]. Full proofs are deferred to App. F. 4. The first basic result we need about our notion of realizability is that it is monotone w.r.t. step indexes.

Lemma D.25 (Monotonicity of Realizability). Let T be a type without free iteration variables. If x n T then x k T for all k ≤ n.

The correctness of subtyping requires two additional lemmas. The first one concerns the rule [START_REF] Fujima | Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes[END_REF]. For a pure type A and x ∈ Γ A , we have x n A for all n > 0.

T ≤ |T | Lemma D.
Second, we need a result of [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF] for the correctness of the subtyping rules

{B | ψ} → {A | ϕ} ≤ {B → A | [ev(ψ)]ϕ} E, x : {B | ψ} M : {A | ϕ} E λx.M : {B → A | [ev(ψ)]ϕ}
An object X of S is total if all its restriction maps r X n : X n+1 → X n are surjective. Hence, if X is total, then given t ∈ X n for some n > 0, there is a global section x : 1 → S X such that x n (•) = t.

Lemma D.27 ([20,Cor. 3.8]). For a pure type A, the object A is total.

We then obtain the correctness of subtyping as usual. The rules

A ϕ ⇒ ψ {A | ϕ} ≤ {A | ψ} A c ϕ ⇒ ψ { A | [box]ϕ} ≤ { A | [box]ψ}
rely on Lem. D.13 (Lem. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].2), while

ϕ safe {A | ϕ} ≡ { A | [box]ϕ}
is given by Prop. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].3.

Lemma D.28 (Correctness of Subtyping (Lem. 7.6)). Given types T, U without free iteration variable, if x n U and U ≤ T then x n T .

We now have all we need for the Adequacy Theorem 7. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF]. As usual it requires a stronger inductive invariant than the statement of Thm. 7.7. Given a typed term

M : Γ Q -→ Γ P x -→ M • x such that, if y ∈ Γ Q Γ ∆Γ Q = Γ Q satisfies ψ
in the standard sense (i.e. y ∈ {|ϕ|}), then the unique global section Γ M (y) n+1 (•) = Γ M (y) n (•) ∈ Γ P satisfies ϕ in the standard sense (i.e. belongs to {|ϕ|}).

D.11 A Galois Connection

It is common for the classification of temporal properties to identify safety properties with topologically closed sets and to identify liveness properties with topologically dense sets. As any subset of a topological space is the intersection of a closed set with a dense set, this provides a topological decomposition of temporal properties, which furthermore restricts to regular properties on (finitary) polynomial types. We refer to e.g. [START_REF] Baier | Principles of Model Checking[END_REF].

Here, we make explicit the relation between safe formulae on polynomial types (in the sense of Def. 6.5) and safety properties understood as closed subsets of the corresponding final Set-coalgebras (in view of Møgelberg's Theorem [START_REF] Møgelberg | A type theory for productive coprogramming via guarded recursion[END_REF]), for the usual tree (or stream) topology.

First, it might be useful to remember what it means for a global section x ∈ Γ X in S to satisfy a property S, where S ∈ Sub(X) is a subobject of X. Following e.g. [START_REF] Lane | Sheaves in geometry and logic: A first introduction to topos theory[END_REF]51], we say that x ∈ Γ X satisfies a property S ∈ Sub(X) if x factors through S, as in

S _ 1 x / / 5 5 X that is: ∀n > 0, x n (•) ∈ S(n)
Fix an object X of S. There is a Galois connection between the subobjects of X in S and the subsets of Γ X in Set:

Pref Clos : Sub(X) -→ P(Γ X)

where for S ∈ P(Γ X) and B ∈ Sub(X),

Pref(S) : n -→ {x n (•) | x ∈ S} Clos(B) := {x ∈ Γ X | ∀n > 0, x n (•) ∈ B(n)}
Of course, Clos is the restriction of Γ : S → Set to the subobjects of X.

Let us spell out the fact that Pref Clos form a Galois connection. Fix an object X of S. First, it is trivial that the functions Pref : P(Γ X) -→ Sub(X) Clos : Sub(X) -→ P(Γ X) are monotone w.r.t. the orders of the lattices P(Γ X) and Sub(X). Moreover, we have: Lemma D. [START_REF] Hofmann | A cartesian-closed category for higher-order model checking[END_REF]. We have (i) S ⊆ Clos(Pref(S)) for S ∈ P(Γ X).

(ii) Pref(Clos(B)) ⊆ B for B ∈ Sub(X).

Proof.

(i) Given x ∈ S, by definition we have

x n (•) ∈ Pref(S)(n) for all n > 0, so x ∈ Clos(Pref(S)). (ii) Given a ∈ Pref(Clos(B))(n), there is some x ∈ Clos(B) such that a = x n (•). But x ∈ Clos(B) means x k (•) ∈ B(k) for all k > 0, so that a = x n (•) ∈ B(n).
As usual, we trivially get

Pref(S) ≤ B iff S ⊆ Clos(B)
Say that S ∈ P(Γ X) is closed if S = Clos(B) for some B ∈ Sub(X). It is easy to see that S is closed if and only if S = Clos(Pref(S)). Note that S = Clos(Pref(S)) unfolds to

∀x ∈ Γ A , x ∈ S iff ∀n > 0, ∃y ∈ S, x n (•) = y n (•)
When A is a polynomial recursive type, Thm. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF]

E Details of the Examples

E.1 Guarded Streams

The Later Modality on Guarded Streams Example E. [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF]. We have the following basic modal refinement types for Cons g and tl g :

Cons g : A -→ {Str g A | ϕ} -→ {Str g A | ϕ} tl g : {Str g A | ϕ} -→ {Str g A | ϕ}
Proof. We begin with Cons g . Recall that Cons g = λx.λs.fold x, s and that (-

) = [fold][π 1 ][next](-).
The result then follows from the following derivation:

x : A, s : {Str g A | ϕ} s : {Str g A | ϕ}

x : A, s :

{Str g A | ϕ} s : { Str g A | [next]ϕ} x : A, s : {Str g A | ϕ} x, s : {A × Str g A | [π 1 ][next]ϕ} x : A, s : {Str g A | ϕ} fold x, s : {Str g A | [fold][π 1 ][next]ϕ}
As for tl g , recalling that tl g = λs.π 1 (unfold s), the result follows from

s : {Str g A | ϕ} s : {Str g A | [fold][π 1 ][next]ϕ} s : {Str g A | ϕ} unfold s : {A × Str g A | [π 1 ][next]ϕ} s : {Str g A | ϕ} π 1 (unfold s) : { Str g A | [next]ϕ} s : {Str g A | ϕ} π 1 (unfold s) : {Str g A | ϕ}

Destructors of Guarded Streams

Example E. [START_REF] Ahmed | Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types[END_REF]. The types of hd g and tl g can be refined as follows with the always modality 2:

hd g : {Str g A | 2[hd]ϕ} -→ {A | ϕ} tl g : {Str g A | 2[hd]ϕ} -→ {Str g A | 2[hd]ϕ} Proof. Recall that [hd]ϕ = [fold][π 0 ]ϕ.
We begin with the typing of hd g := λs.π 0 (unfold s) :

{Str g A | 2[hd]ϕ} -→ {A | ϕ} We use Str g A 2[hd]ϕ ⇒ [hd]ϕ. s : {Str g A | 2[hd]ϕ} s : {Str g A | 2[hd]ϕ} Str g A 2[hd]ϕ ⇒ [hd]ϕ {Str g A | 2[hd]ϕ} ≤ {Str g A | [hd]ϕ} s : {Str g A | 2[hd]ϕ} s : {Str g A | [hd]ϕ} s : {Str g A | 2[hd]ϕ} unfold s : {A × Str g A | [π 0 ]ϕ} s : {Str g A | 2[hd]ϕ} π 0 (unfold s) : {A | ϕ} λs.π 0 (unfold s) : {Str g A | 2[hd]ϕ} -→ {A | ϕ}
We continue with the typing of tl g := λs.π 1 (unfold s) :

{Str g A | 2[hd]ϕ} -→ {Str g A | 2[hd]ϕ} We use Str g A 2[hd]ϕ ⇒ 2[hd]ϕ. Recall that ϕ = [fold][π 1 ][next]ϕ. s : {Str g A | 2[hd]ϕ} s : {Str g A | 2[hd]ϕ} Str g A 2[hd]ϕ ⇒ 2[hd]ϕ {Str g A | 2[hd]ϕ} ≤ {Str g A | 2[hd]ϕ} s : {Str g A | 2[hd]ϕ} s : {Str g A | 2[hd]ϕ} s : {Str g A | 2[hd]ϕ} unfold s : {A × Str g A | [π 0 ][next]2[hd]ϕ} s : {Str g A | 2[hd]ϕ} π 1 (unfold s) : { Str g A | [next]2[hd]ϕ} s : {Str g A | 2[hd]ϕ} π 1 (unfold s) : {Str g A | 2[hd]ϕ} λs.π 1 (unfold s) : {Str g A | 2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}

Constructor of Guarded Streams

Example E.3. The type of Cons g can be refined as follows with the always modality 2:

Cons g : {A | ϕ} -→ {Str g A | 2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
Proof. We show

Cons g := λx.λs.fold x, s : {A | ϕ} -→ {Str g A | 2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
To this end, we use the following derived rule (see Ex. 5.1):

E M : {A | ϕ} E N : {B | ψ} E M, N : {A × B | [π 0 ]ϕ ∧ [π 1 ]ψ}
Consider the typing context

E := x : {A | ϕ} , s : {Str g A | 2[hd]ϕ}
We know from §E.1 that E fold x, s :

{Str g A | 2[hd]ϕ} Since Str g A ([hd]ϕ ∧ 2[hd]ϕ) ⇒ 2[hd]ϕ, we are done if we show E fold x, s : {Str g A | [hd]ϕ}
But this is trivial:

E x : {A | ϕ} E x, s : {A × Str g A | [π 0 ]ϕ} E fold x, s : {Str g A | [fold][π 0 ]ϕ}

Map over Guarded Streams

Example E.4. We have the following:

map g : ({A | ϕ} → {B | ψ}) -→ {Str g A | 2[hd]ϕ} -→ {Str g B | 2[
hd]ψ} := λf.fix(g).λs.(f (hd g s)) :: g (g (tl g s))

Proof. We proceed as follows, using §E.1 and §E.1:

E s : {Str g A | 2[hd]ϕ} E hd g s : {A | ϕ} E f (hd g s) : {B | ψ} E s : {Str g A | 2[hd]ϕ} E tl g s : {Str g A | 2[hd]ϕ} E g (tl g s) : {Str g B | 2[hd]ψ} E (f (hd g s)) :: g (g (tl g s)) : {Str g B | 2[hd]ψ}
λf.fix(g).λs.(f (hd g s)) :: g (g (tl g s)) : T

where

T := ({A | ϕ} → {B | ψ}) -→ {Str g A | 2[hd]ϕ} -→ {Str g B | 2[hd]ψ} E := f : {A | ϕ} → {B | ψ} , g : ({Str g A | 2[hd]ϕ} → {Str g B | 2[hd]ψ}), s : {Str g A | 2[hd]ϕ}

Merge over Guarded Streams

Example E.5. We have the following:

merge g : {Str g A | 2[ϕ 0 ]} -→ {Str g A | 2[ϕ 1 ]} -→ {Str g A | 2([ϕ 0 ] ∨ [ϕ 1 ]
)} := fix(g).λs 0 .λs 1 .Cons g (hd g s 0 ) next Cons g (hd g s 1 ) (g (tl g s 0 ) (tl g s 1 ))

Proof. Let E be the context g :

{Str g A | 2[ϕ 0 ]} -→ {Str g A | 2[ϕ 1 ]} -→ {Str g A | 2([ϕ 0 ] ∨ [ϕ 1 ])} , s 0 : {Str g A | 2[ϕ 0 ]} , s 1 : {Str g A | 2[ϕ 1 ]} We have E hd g s 0 : {A | ϕ 0 } E hd g s 1 : {A | ϕ 1 } E tl g s 0 : {Str g A | 2[ϕ 0 ]} E tl g s 1 : {Str g A | 2[ϕ 1 ]}
We thus get g (tl g s 0 ) (tl g s 1 ) :

{Str g A | 2([ϕ 0 ] ∨ [ϕ 1 ])}
and we are done since using subtyping we have

Cons g : {A | ϕ 0 } -→ {Str g A | 2([ϕ 0 ] ∨ [ϕ 1 ])} -→ {Str g A | 2([ϕ 0 ] ∨ [ϕ 1 ])} Cons g : {A | ϕ 1 } -→ {Str g A | 2([ϕ 0 ] ∨ [ϕ 1 ])} -→ {Str g A | 2([ϕ 0 ] ∨ [ϕ 1 ])} E.2
(unbox s))) : {Str A | [box]2[hd]ϕ} -→ {Str A | [box]2[hd]ϕ} and s : {Str A | [box] ϕ} s : {Str A | [box] ϕ} s : {Str A | [box] ϕ} unbox s : {Str g A | ϕ} s : {Str A | [box] ϕ} tl g (unbox s) : {Str g A | ϕ} Str A constant s : {Str A | [box] ϕ} prev ι (tl g (unbox s)) : {Str g A | ϕ} s : {Str A | [box] ϕ} box ι (prevι(tl g (unbox s))) : {Str g A | ϕ} ϕ safe s : {Str A | [box] ϕ} box ι (prev ι (tl g (unbox s))) : {Str A | [box]ϕ} λs.box ι (prev ι (tl g (unbox s))) : {Str A | [box] ϕ} -→ {Str A | [box]ϕ}

E.3 Map over Coinductive Streams

We discuss here the cases of

map : ({B | ψ} → {A | ϕ}) -→ {Str B | [box] [hd]ψ} -→ {Str A | [box] [hd]ϕ}
where ψ, ϕ are safe and smooth and where ∈ {2, 3, 32, 23}. The case of 2 is handled as in Ex. 5.4, using that 2[hd]ϕ and 2[hd]ψ are safe. The case of 3 is detailed in Ex. E.7 ( §E.3). The idea is that since 3[hd]ϕ, 3[hd]ψ are smooth and since 3 k [hd]ϕ, 3 k [hd]ψ are safe, we can reduce to typing the guarded map g as

map g : ({B | ψ} → {A | ϕ}) -→ ∀k • Str g B 3 k [hd]ψ -→ Str g A 3 k [hd]ϕ
The case of 32, detailed in Ex. E

T (k) := Str g B 3 k 2[hd]ψ -→ Str g A 3 k 2[hd]ϕ
and assuming f of type {B | ψ} → {A | ϕ}. But this is unfortunately too weak. Similarly as with 3, it is natural to first assume the type ∀k • T (k) for the recursion variable g and then to apply the (∀-CI) rule (Fig. 11) on ∀k • T (k). In the case of T (k+1), we unfold

3 k+1 2[hd]ψ ⇔ 2[hd]ψ ∨ 3 k 2[hd]ψ
and apply the (∨-E) rule (Fig. 8). But in the branch of 2[hd]ψ, giving g the type, say,

Str g B 3 1 2[hd]ψ -→ Str g A 3 1 2[hd]ϕ
is not sufficient to derive

s : {Str g B | 2[hd]ψ} g (tl g s) : {Str g A | 2[hd]ϕ}
The reason is that [next] (and thus ) does not satisfy axiom (P) of Table 2 (see §7). The solution is to use the [ev(-)]/ → modality to encode a kind of "intersection" on arrow types, and to type (map g f ) with

∀k • Str g B → Str g A 3 k 2[hd]ψ → 3 k 2[hd]ϕ ∧ 2[hd]ψ → 2[hd]ϕ
We finally turn to 23. Using that 23[hd]ϕ and 23[hd]ψ are both smooth, we first unfold the 2's using the rules (ν-I) (Fig. 11) and then (ν-E) (Ex. 6.10), thus reducing to We apply the (∀-CI) rule on ∀ • ∀k • U ( , k). The case of ∀k • U (0, k) is trivial since 2 0 ϑ ⇔ . We then apply the (∀-CI) rule, this time on ∀k • U ( +1, k). The case of U ( +1, 0) can be dealt with using the (ExF) rule. In the case of U ( +1, k+1), we conclude with a straightforward case analysis based on the unfoldings

2 +1 3 k+1 [hd]ϑ ⇔ 3 k+1 [hd]ϑ ∧ 2 3 k+1 [hd]ϑ 3 k+1 [hd]ϑ ⇔ [hd]ϑ ∨ 3 k [hd]ϑ
See Ex. E.9 ( §E.3) for details. Just note that since ⇔ (Table 2) we have

2 1 ϑ ⇔ ϑ, so that g : ∀ • ∀k • U ( , k) g : Str g B 3 k [hd]ψ -→ Str g A 3 k [hd]ϕ
The Case of Eventually (3[hd]ϕ)

Example E. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF]. We have the following, for safe and smooth ϕ and ψ:

map : ({B | ψ} → {A | ϕ}) -→ {Str B | [box]3[hd]ψ} -→ {Str A | [box]3[hd]ϕ} = λf.
map g : ({B | ψ} → {A | ϕ}) -→ ∀k • Str g B 3 k [hd]ψ -→ Str g A 3 k [hd]ϕ = λf.fix(g).λs.(f (hd g s)) :: g (g (tl g s)) Let N := (f (hd g s)) :: g (g (tl g s)) M := λs.N T (k) := Str g B 3 k [hd]ψ -→ Str g A 3 k [hd]ϕ E := E f , g : ∀k • T (k)
We show

E M : ∀k • T (k)
We reason by cases on k with the rule

E M : T (0) E M : T (k+1) E M : ∀k • T (k) Case of T (0).
We show

E, s : {Str g B | 3 0 [hd]ψ} N : {Str g A | 3 0 [hd]ϕ} Since 3 0 [ψ] ⇔ ⊥, we conclude with the (ExF) rule E, s : {Str g B | 3 0 [hd]ψ} s : {Str g B | ⊥} E, s : {Str g B | 3 0 [hd]ψ} N : Str g A E, s : {Str g B | 3 0 [hd]ψ} N : {Str g A | 3 0 [hd]ϕ}

Case of T (k+1).

We show

E, s : Str g B 3 k+1 [hd]ψ N : Str g A 3 k+1 [hd]ϕ Using 3 k+1 [hd]ψ ⇔ ([hd]ψ ∨ 3 k [hd]ψ)
we do a case analysis on the refinement type of s.

Str g B 3 k [hd]ψ Since E g : ∀k • Str g B 3 k [hd]ψ -→ Str g A 3 k [hd]ϕ
we have

E g : Str g B 3 k [hd]ψ -→ Str g A 3 k [hd]ϕ
Since moreover by §E.1 we have

Cons g : A -→ Str g A 3 k [hd]ϕ -→ Str g A 3 k [hd]ϕ we deduce that E, s : Str g B 3 k [hd]ψ N : Str g B 3 k [hd]ψ
The

map g : ({B | ψ} → {A | ϕ}) -→ ∀k • Str g B 3 k 2[hd]ψ -→ Str g A 3 k 2[hd]ϕ = λf.fix(g).λs.(f (hd g s)) :: g (g (tl g s)) Let N := (f (hd g s)) :: g (g (tl g s)) M := λs.N T (k) := Str g B → Str g A 3 k 2[hd]ψ → 3 k 2[hd]ϕ ∧ 2[hd]ψ → 2[hd]ϕ E := E f , g : ∀k • T (k)
We show

E M : ∀k • T (k)
We reason by cases on k with the rule

E M : T (0) E M : T (k+1) E M : ∀k • T (k)
Case of T (0).

We have to show

E, s : {Str g B | 2[hd]ψ} N : {Str g A | 2[hd]ϕ} and E, s : {Str g B | 3 0 2[hd]ψ} N : {Str g A | 3 0 2[hd]ϕ}
We only detail the latter since the former can be dealt-with as in §E.1. Since

3 0 2[ψ] ⇔ ⊥
we conclude with the (ExF) rule

E, s : {Str g B | 3 0 2[hd]ψ} s : {Str g B | ⊥} E, s : {Str g B | 3 0 2[hd]ψ} N : Str g A E, s : {Str g B | 3 0 2[hd]ψ} N : {Str g A | 3 0 2[hd]ϕ}

Case of T (k+1).

We show

E, s : {Str g B | 2[hd]ψ} N : {Str g A | 2[hd]ϕ} and E, s : Str g B 3 k+1 2[hd]ψ N : Str g A 3 k+1 2[hd]ϕ
We only detail the latter since the former can be dealt-with as in §E.1. Using

3 k+1 2[hd]ψ ⇔ (2[hd]ψ ∨ 3 k 2[hd]ψ)
we do a case analysis on the refinement type of s.

(Sub)Case of 2[hd]ψ.

We show

E, s : {Str g B | 2[hd]ψ} N : Str g A 3 k+1 2[hd]ϕ Note that 2[hd]ϕ ⇒ 3 k+1 2[hd]ϕ.
We can therefore reduce to E, s :

{Str g B | 2[hd]ψ} N : {Str g A | 2[hd]ϕ}
and we can conclude as in §E.1.

(Sub)Case of 3 k 2[hd]ψ. Since 3 k 2[hd]ϕ ⇒ 3 k+1 2[hd]ϕ, we reduce to showing E, s : Str g B 3 k 2[hd]ψ N : Str g A 3 k 2[hd]ϕ
By §E. [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF] we have

E, s : Str g B 3 k 2[hd]ψ tl g s : Str g B 3 k 2[hd]ψ Since E g : ∀k • Str g B 3 k 2[hd]ψ -→ Str g A 3 k 2[hd]ϕ
we have

E g : Str g B 3 k 2[hd]ψ -→ Str g A 3 k 2[hd]ϕ
Since moreover by §E.1 we have

Cons g : A -→ Str g A 3 k 2[hd]ϕ -→ Str g A 3 k 2[hd]ϕ we deduce that E, s : Str g B 3 k 2[hd]ψ N : Str g B 3 k 2[hd]ψ
The Case of Always Eventually We are thus led to deriving

E f , s : Str B [box]2 3 k [hd]ψ box ι (map g f (unbox s)) : Str A [box]2 3 k [hd]ϕ
where

E f := f : {B | ψ} → {A | ϕ}
Since the formulae 2 3 k [hd]ψ and 2 3 k [hd]ϕ are safe, we are done if we show

map g : ({B | ψ} → {A | ϕ}) -→ ∀k • ∀ • Str g B 2 3 k [hd]ψ -→ Str g A 2 3 k [hd]ϕ = λf
.fix(g).λs.(f (hd g s)) :: g (g (tl g s))

Let N := (f (hd g s)) ::

g (g (tl g s)) M := λs.N T (k, ) := Str g B 2 3 k [hd]ψ -→ Str g A 2 3 k [hd]ϕ E := E f , g : ∀k • ∀ • T (k, )
We show

E M : ∀k • ∀ • T (k, )
We reason by cases on k and . This amounts to the derived rule

E M : T (0, 0) E M : T (0, +1) E M : T (k+1, 0) E M : T (k+1, +1) E M : ∀k • ∀ • T (k, )
Cases of T (u, 0).

We have 2 0 θ ⇔ , and we are done since

E, s : {Str g B | } N : {Str g A | }
Case of T (0, +1).

We have 3 0 [θ] ⇔ ⊥, and we reduce to showing

E, s : Str g B 2 +1 ⊥ N : Str g A 2 +1 ⊥ But since 2 +1 ⊥ ⇒ ⊥, we have E, s : Str g B 2 +1 ⊥ s : {Str g B | ⊥}
and we conclude with the (ExF) rule

E, s : Str g B 2 +1 ⊥ s : {Str g B | ⊥} E, s : Str g B 2 +1 ⊥ N : Str g A E, s : {Str g B | 2 +1 ⊥} N : {Str g A | 2 +1 ⊥} Case of T (k+1, +1).
Using

Str g A 2 +1 θ ⇔ (θ ∧ 2 θ), we show E, s : Str g B 2 +1 3 k+1 [hd]ψ N : Str g A 3 k+1 [hd]ϕ ∧ 2 3 k+1 [hd]ϕ
We consider each conjunct separately.

(Sub)Case of 3 k+1 [hd]ϕ.

We show By §E. [START_REF] Abel | Well-founded recursion with copatterns and sized types[END_REF] we have

E, s : Str g B 2 +1 3 k+1 [hd]ψ N : Str g A 3 k+1 [hd]ϕ Using E, s : Str g B 2 +1 3 k+1 [hd]ψ s : Str g B 3 k+1
E, s : Str g B 3 k [hd]ψ tl g s : Str g B 3 k [hd]ψ Since E g : ∀k • ∀ • Str g B 2 3 k [hd]ψ -→ Str g A 2 3 k [hd]ϕ
we have

E g : Str g B 2 1 3 k [hd]ψ -→ Str g A 2 1 3 k [hd]ϕ
But (θ ∧ ) ⇔ θ, so that 2 1 θ ⇔ θ, and thus

E g : Str g B 3 k [hd]ψ -→ Str g A 3 k [hd]ϕ
Since moreover by §E.1 we have

Cons g : A -→ Str g A 3 k [hd]ϕ -→ Str g A 3 k [hd]ϕ we deduce that E, s : Str g B 3 k [hd]ψ N : Str g B 3 k [hd]ψ
and we are done since

3 k [hd]ϕ ⇒ 3 k+1 [hd]ϕ. (Sub)Case of 2 3 k+1 [hd]ϕ.
We show

E, s : Str g B 2 +1 3 k+1 [hd]ψ N : Str g A 2 3 k+1 [hd]ϕ Since E, s : Str g B 2 +1 3 k+1 [hd]ψ s : Str g B 2 3 k+1 [hd]ψ by §E.1 we have E, s : Str g B 2 +1 3 k+1 [hd]ψ tl g s : Str g B 2 3 k+1 [hd]ψ But now since E g : ∀k • ∀ • Str g B 2 3 k [hd]ψ -→ Str g A 2 3 k [hd]ϕ
we have

E g : Str g B 2 3 k+1 [hd]ψ -→ Str g A 2 3 k+1 [hd]ϕ
and we conclude with §E.1, namely

Cons g : A -→ Str g A 2 3 k+1 [hd]ϕ -→ Str g A 2 3 k+1 [hd]ϕ

E.4 The Diagonal Function

Consider a stream of streams s. We have s = (s i | i ≥ 0) where each s i is itself a stream s i = (s i,j | j ≥ 0). The diagonal of s is then the stream (s i,i | i ≥ 0). Note that s i,i = hd(tl i (hd(tl i (s))). Indeed, tl i (s) is the stream of streams (s k | k ≥ i), so that hd(tl i (s)) is the stream s i and tl i (hd

(tl i (s))) is the stream (s i,k | k ≥ i).
Taking its the head thus gives s i,i .

We implement the diagonal function as follows:

diag := λs.box ι diag g (unbox s) : Str(Str A) -→ Str A diag g := diagaux g id : Str g (Str A) -→ Str g A diagaux g : (Str A → Str A) -→ Str g (Str A) -→ Str g A := fix(g).λt.λs. Cons g (hd • t)(hd g s) g next(t • tl) (tl g s)
The auxiliary higher-order function diagaux g iterates the coinductive tl over the head of the stream of streams s. We write • for function composition, so that assuming s : Str g (Str A) and t : Str A → Str A, we have

(hd g s) : Str A (hd • t) : Str A → A (hd • t)(hd g s) : A (t • tl) : Str A → Str A
This requires the coinductive type Str A. In Ex. E.11 ( §E.4) below, for a safe ϕ we obtain

diag g : {Str g (Str A) | 2[hd][box]2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
This easily follows from the fact that using Ex. 5.3 and Ex. 5.4, we can type diagaux g with

{Str A | [box]2[hd]ϕ} → {Str A | [box]2[hd]ϕ} -→ {Str g (Str A) | 2[hd][box]2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
In Ex. E.12 ( §E.4) we show that for a safe and smooth ϕ, we have

diag : {Str(Str A) | [box]32[hd][box]2[hd]ϕ} -→ {Str A | [box]32[hd]ϕ}
Similarly as for map in §E.3, we reduce to

diagaux g : ∀k • {Str A | [box]2[hd]ϕ} → {Str A | [box]2[hd]ϕ} -→ U (k) where U (k) := {Str g (Str A) → Str g A | ψ 0 (k) ∧ ψ 1 } ψ 0 (k) := 3 k 2[hd][box]2[hd]ϕ → 3 k 2[hd]ϕ ψ 1 := 2[hd][box]2[hd]ϕ → 2[hd]ϕ
The Guarded Diagonal Function

Example E.11 (The Guarded Diagonal Function). For a safe ϕ, we have

diag g : {Str g (Str A) | 2[hd][box]2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
Recall that

diag g : Str g (Str A) -→ Str g A := diagaux g id diagaux g : (Str A → Str A) -→ Str g (Str A) -→ Str g A := fix(g).λt.λs.Cons g (hd • t)(hd g s) g next(t • tl) (tl g s)
Proof. We reduce to

diagaux g : {Str A | [box]2[hd]ϕ} → {Str A | [box]2[hd]ϕ} -→ {Str g (Str A) | 2[hd][box]2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
Let E be the context

g : T , t : {Str A | [box]2[hd]ϕ} -→ {Str A | [box]2[hd]ϕ} , s : {Str g (Str A) | 2[hd][box]2[hd]ϕ}
where T is the type

{Str A | [box]2[hd]ϕ} → {Str A | [box]2[hd]ϕ} -→ {Str g (Str A) | 2[hd][box]2[hd]ϕ} -→ {Str g A | 2[hd]ϕ}
The result directly follows from the following typings, which are themselves given by §E.1, §E.1 and §E.2:

E hd • t : {Str A | [box]2[hd]ϕ} -→ {A | ϕ} E hd g s : {Str A | [box]2[hd]ϕ} E t • tl : {Str A | [box]2[hd]ϕ} -→ {Str A | [box]2[hd]ϕ} E tl g s : {Str g (Str A) | 2[hd][box]2[hd]ϕ}
The

diag g : ∀k • Str g (Str A) 3 k 2[hd][box]2[hd]ϕ -→ Str g A 3 k 2[hd]ϕ
Consider the types

U (k) := {Str g (Str A) → Str g A | ψ 0 ∧ ψ 1 } T (k) := {Str A | [box]2[hd]ϕ} → {Str A | [box]2[hd]ϕ} -→ U (k)
where

ψ 0 := 3 k 2[hd][box]2[hd]ϕ → 3 k 2[hd]ϕ ψ 1 := 2[hd][box]2[hd]ϕ → 2[hd]ϕ We show diagaux g : ∀k • T (k) Let N := Cons g (hd • t)(hd g s) g next(t • tl) (tl g s) M := λg.λs.N E := g : ∀k • T (k)
We reason by cases on k with the rule

E M : T (0) E M : T (k+1) E M : ∀k • T (k) Let E := E, t : {Str A | [box]2[hd]ϕ} -→ {Str A | [box]2[hd]ϕ}
We omit the proof of

E λs.N : {Str g (Str A) → Str g A | [ev(2[hd][box]2[hd]ϕ)]2[hd]ϕ}
since it follows that of §E.4.

Case of T (0).

Since 3 0 θ ⇔ ⊥, we reduce to showing

E λt.λs.N : {Str A | [box]2[hd]ϕ} → {Str A | [box]2[hd]ϕ} -→ {Str g (Str A) | ⊥} -→ {Str g A | 3 0 2[hd]ϕ}
and we conclude using the (ExF) rule.

Case of T (k+1).

We show

E , s : Str g (Str A) 3 k+1 2[hd][box]2[hd]ϕ N : Str g A 3 k+1 2[hd]ϕ Using 3 k+1 θ ⇐⇒ θ ∨ 3 k θ
we reason by cases on the refinement of s. This leads to two subcases.

(Sub)Case of 2[hd][box]2[hd]ϕ.
We show

E , s : {Str g (Str A) | 2[hd][box]2[hd]ϕ} N : Str g A 3 k+1 2[hd]ϕ Since 2[hd]ϕ ⇒ 3 k+1 2[hd]ϕ, we can reduce to E , s : {Str g (Str A) | 2[hd][box]2[hd]ϕ} N : {Str g A | 2[hd]ϕ}
which is proved as in §E.4.

(Sub)Case of 3 k 2[hd][box]2[hd]ϕ.
We show

E , s : Str g (Str A) 3 k 2[hd][box]2[hd]ϕ N : Str g A 3 k 2[hd]ϕ Let E := E , s : Str g (Str A) 3 k 2[hd][box]2[hd]ϕ
Note that E g : T (k), so that by §E. [START_REF] Ahmed | Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types[END_REF] we have

E g next(t • tl) : Str g (Str A) 3 k 2[hd][box]2[hd]ϕ → Str g A 3 k 2[hd]ϕ
Using §E.1, we derive

E s : Str g (Str A) 3 k 2[hd][box]2[hd]ϕ E tl g s : Str g (Str A) 3 k 2[hd][box]2[hd]ϕ E g next(t • tl) (tl g s) : Str g A 3 k 2[hd]ϕ E Cons g (hd • t)(hd g s) g next(t • tl) (tl g s) : Str g A 3 k 2[hd]ϕ

E.5 Fair Streams

We discuss here an adaptation of the fair streams of [START_REF] Cave | Fair Reactive Programming[END_REF][START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF]. We rely on the basic datatypes presented in §E.5. In §E.5 we discuss a function

fb : CoNat -→ CoNat -→ Str Bool
such that, writing 0 for Z and 1 for (S Z) (see Ex. E.15), the non-regular stream (fb 0 1), adapted from [START_REF] Cave | Fair Reactive Programming[END_REF][START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF], is of the form ff tt ff tt tt ff tt tt tt ff tt tt tt tt ff . . .

This stream thus contains infinitely many tt's and infinitely many ff's. This is expressed with the formula [box]

fb g : CoNat g -→ {CoNat g | [S]} -→ {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])} fb g : ∀k • ∀ • CoNat g 3 [Z] → CoNat g 3 +1 [Z] → Str g Bool 2 k 3 k+ [hd][ff]
A Fair Stream of Booleans Example E. [START_REF] Bradfield | The mu-calculus and Model Checking[END_REF].

fb : CoNat -→ CoNat -→ Str Bool := λc.λm. box ι (fb g (unbox c) (unbox m)) fb g : CoNat g -→ CoNat g -→ Str g Bool := fix(g).λc.λm. case c of | Z g → ff :: g g (next m) next(S g (next m)) | S g n → tt :: g g n (next m)
Example E. [START_REF] Cave | Fair Reactive Programming[END_REF].

fb : {CoNat | [box]3[Z]} -→ CoNat -→ {Str Bool | [box]3[hd][ff]} fb g : ∀k • CoNat g 3 k [Z] -→ CoNat g -→ Str g Bool 3 k [hd][ff] Proof. Let T (k) := CoNat g 3 k [Z] -→ CoNat g -→ Str g Bool 3 k [hd][ff]
and assume

g : ∀k • T (k) Let M (g, c, m) := case c of | Z g → ff :: g g (next m) next(S g (next m)) | S g n → tt :: g g n (next m)
We show λc.λm.M (g, c, m) : ∀k • T (k)

We apply the (∀-CI) rule on ∀k. This leads to two cases.

Case of T (0). We get the result from the (ExF) rule since

3 0 [Z] ⇔ ⊥ Case of T (k+1). We show M (g, c, m) : Str g Bool 3 k+1 [hd][ff] assuming c : CoNat g 3 k+1 [Z] m : CoNat g Using 3 k+1 [Z] ⇔ [Z] ∨ 3 k [Z]
we reason by cases on the refinement type of c. This leads to two subcases.

(Sub)Case of [Z]. We apply the (Inj 0 -E) rule on the refinement type of (unfold c). Since

[hd][ff] ⇒ 3 k+1 [hd][ff]
the result follows from the fact that ff ::

g g (next m) next(S (next m)) : {Str g Bool | [hd][ff]} (Sub)Case of 3 k [Z].
We have

unfold c : 1 + CoNat g [in 1 ][next]3 k [Z]
By applying the (Inj 1 -E) rule on the refinement type of (unfold c), we are left with showing tt :: g g n (next m) :

Str g Bool 3 k+1 [hd][ff]
assuming n :

CoNat g 3 k [Z] Using 3 k [hd][ff] ⇒ 3 k+1 [hd][ff]
we are done since g n (next m) :

Str g Bool 3 k [hd][ff]
Example E. [START_REF] Chellas | Modal Logic: An Introduction[END_REF]. Consider a function

f : N × N -→ N such that -1 ≤ f (k + 1, + 1) -f (k, + 2) ≤ f (k + 1, + 1) -+ 1 ≤ f (k + 1, + 1) -f (k, + 1) ≤ f (k + 1, + 1)
for instance f (k, ) = k + . Then we can give the following refined type to fb g :

∀k•∀ • CoNat g 3 [Z] -→ CoNat g 3 +1 [Z] -→ Str g Bool 2 k 3 f(k, ) [hd][ff] Proof. Let U (k, ) := {CoNat g → CoNat g → Str g Bool | ϕ(k, ) ∧ ψ( )} ϕ(k, ) := 3 [Z] → 3 +1 [Z] → 2 k 3 f(k, ) [hd][ff] ψ( ) := 3 [Z] → → 3 [hd][ff]
and assume g :

∀k • ∀ • U (k) Let M (g, c, m) := case c of | Z g → ff :: g g (next m) next(S g (next m)) | S g n → tt :: g g n (next m) We show λc.λm.M (g, c, m) : ∀k • ∀ • U (k)
First, proceeding similarly as in Ex. E. [START_REF] Cave | Fair Reactive Programming[END_REF],

λc.λm.M (g, c, m) : ∀ • CoNat g → CoNat g → Str g Bool 3 [Z] → → 3 [hd][ff] Let T (k, ) := CoNat g 3 [Z] -→ CoNat g 3 +1 [Z] -→ Str g Bool 2 k 3 f(k, ) [hd][ff] We show λc.λm.M (g, c, m) : ∀k • ∀ • T (k)
We apply the (∀-CI) rule on ∀k. In the case of ∀ • T (0, ), the result is trivial since

2 0 3 f(0, ) [hd][ff] ⇔
In the case of ∀ • T (k+1, ), we apply the (∀-CI) rule, this time on ∀ . The case of T (k+1, 0) is dealt-with using the (ExF) rule since

3 0 [Z] ⇔ ⊥
In the case of T (k+1, +1), we show

M (g, c, m) : Str g Bool 2 k+1 3 f(k+1, +1) [hd][ff] assuming c : CoNat g 3 +1 [Z] m : CoNat g 3 +2 [Z]
We apply the typing rule for case (Fig. 4). This leads to two branches, one for (unfold c) = fold(in 0 ) (denoted Z g ), and one for (unfold c) = fold(in

1 n) (denoted S g n).
Case of Z g . We have to show

ff :: g g (next m) next(S (next m)) : Str g Bool 2 k+1 3 f(k+1, +1) [hd][ff]
We have

2 k+1 3 f(k+1, +1) [hd][ff] ⇔ 3 f(k+1, +1) [hd][ff] ∧ 2 k 3 f(k+1, +1) [hd][ff]
and we consider each conjunct separately.

(Sub)Case of

3 f(k+1, +1) [hd][ff].
We have

ff :: g g (next m) next(S (next m)) : {Str g Bool | [hd][ff]}
and as f (k + 1, + 1) ≥ 1 we are done with

[hd][ff] ⇒ 3 f(k+1, +1) [hd][ff] (Sub)Case of 2 k 3 f(k+1, +1) [hd][ff]. Since m : CoNat g 3 +2 [Z] S g (next m) : CoNat g 3 +3 [Z]
we have

g (next m) next(S (next m)) : Str g Bool 2 k 3 f(k, +2) [hd][ff] so that ff :: g g (next m) next(S (next m)) : Str g Bool 2 k 3 f(k, +2) [hd][ff]
But since f (k, + 2) ≤ f (k + 1, + 1), we have

3 f(k, +2) [hd][ff] ⇒ 3 f(k+1, +1) [hd][ff]
and we obtain

ff :: g g (next m) next(S (next m)) : Str g Bool 2 k 3 f(k+1, +1) [hd][ff]
Case of S g n.

We have to show tt ::

g g n (next m) : Str g Bool 2 k+1 3 f(k+1, +1) [hd][ff] assuming n : CoNat g 3 [Z]
We have

2 k+1 3 f(k+1, +1) [hd][ff] ⇔ 3 f(k+1, +1) [hd][ff] ∧ 2 k 3 f(k+1, +1) [hd][ff]
and we consider each conjunct separately.

(Sub)Case of

3 f(k+1, +1) [hd][ff]. Using g : CoNat g → CoNat g → Str g Bool 3 [Z] → → 3 [hd][ff]
we get tt ::

g g n (next m) : Str g Bool 3 +1 [hd][ff]
and the result follows from the fact that

+ 1 ≤ f (k + 1, + 1) (Sub)Case of 2 k 3 f(k+1, +1) [hd][ff]. Since ≤ + 1, we have n : CoNat g 3 +1 [Z]
and thus

g n (next m) : Str g Bool 2 k 3 f(k, +1) [hd][ff]
so that tt ::

g g n (next m) : Str g Bool 2 k 3 f(k, +1) [hd][ff]
But since f (k, + 1) ≤ f (k + 1, + 1) we have

3 f(k, +1) [hd][ff] ⇒ 3 f(k+1, +1) [hd][ff]
and we obtain tt ::

g g n (next m) : Str g Bool 2 k 3 f(k+1, +1) [hd][ff]
Example E. [START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF]. We have

fb Z (S Z) : {Str Bool | [box]23[hd][ff]} Proof. Recall that fb : CoNat -→ CoNat -→ Str Bool := λc.λm. box ι (fb g (unbox c) (unbox m))
We show

fb : ∀ • CoNat [box]3 [Z] -→ CoNat [box]3 +1 [Z] -→ {Str Bool | [box]23[hd][ff]}
We apply the (∀-I) rule. Assume

c : CoNat [box]3 [Z] m : CoNat [box]3 +1 [Z]
Since the formulae 3 [Z] and 3 +1 [Z] are safe we have c :

CoNat g 3 [Z] m : CoNat g 3 +1 [Z]
and thus (unbox c) :

CoNat g 3 [Z] (unbox m) : CoNat g 3 +1 [Z]
Now, it follows from Ex. E.19 that

fb g (unbox c) (unbox m) : Str g Bool 2 k 3 f(k, ) [hd][ff] so that box ι (fb g (unbox c) (unbox m)) : Str g Bool 2 k 3 f(k, ) [hd][ff]
Since the formula

2 k 3 f(k, ) [hd][ff] is safe we have box ι (fb g (unbox c) (unbox m)) : Str Bool [box]2 k 3 f(k, ) [hd][ff]
The (µ-I) rule then gives

box ι (fb g (unbox c) (unbox m)) : Str Bool [box]2 k 3[hd][ff]
and the (ν-I) rule gives

box ι (fb g (unbox c) (unbox m)) : {Str Bool | [box]23[hd][ff]}
The result then follows from the fact that [START_REF] Dreyer | Logical Step-Indexed Logical Relations[END_REF]. We have

Z : {CoNat | [box]3 1 [Z]} S Z : {CoNat | [box] 3 1 [Z]} Example E.
fb g : CoNat g -→ {CoNat g | [S]} -→ {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])} Proof. Let T := {CoNat g → CoNat g → Str g Bool | ϕ ∧ ψ} ϕ := [S] → → [hd][tt] ψ := → [S] → 2 ([hd][tt] ∨ [hd][tt])
and assume g :

T Let M (g, c, m) := case c of | Z g → ff :: g g (next m) next(S g (next m)) | S g n → tt :: g g n (next m)
We show λc.λm.M (g, c, m) : T First, by using the (Inj 1 -E) rule we easily get

λc.λm.M (g, c, m) : {CoNat g → CoNat g → Str g Bool | [S] → → [hd][tt]} It remains to show λc.λm.M (g, c, m) : {CoNat g → CoNat g → Str g Bool | → [S] → 2 ([hd][tt] ∨ [hd][tt])} Assume c : CoNat g m : {CoNat g | [S]}
We apply the typing rule for case (Fig. 4). This leads to two branches, one for (unfold c) = fold(in 0 ) (denoted Z g ), and one for (unfold c) = fold(in

1 n) (denoted S g n).
Case of Z g . We have to show

ff :: g g (next m) next(S (next m)) : {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])}
We have

2 ([hd][tt] ∨ [hd][tt]) ⇔ ([hd][tt] ∨ [hd][tt]) ∧ 2 ([hd][tt] ∨ [hd][tt])
and we consider each conjunct separately.

(Sub)Case of ([hd][tt] ∨ [hd][tt]). Since m : {CoNat g | [S]} g : ({CoNat g | [S]} -→ CoNat g -→ {Str g Bool | [hd][tt]}) we get g (next m) next(S (next m)) : {Str g Bool | [hd][tt]}
and the result follows.

(Sub)Case of 2 ([hd][tt] ∨ [hd][tt]).
Since

S g (next m) : {CoNat g | [S]} g : (CoNat g -→ {CoNat g | [S]} -→ {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])}) we get g (next m) next(S (next m)) : {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])}
and the result follows. Case of S g n.

We have to show tt ::

g g n (next m) : {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])} assuming n : CoNat g
We have

2 ([hd][tt] ∨ [hd][tt]) ⇔ ([hd][tt] ∨ [hd][tt]) ∧ 2 ([hd][tt] ∨ [hd][tt])
and we consider each conjunct separately.

(Sub)Case of (

[hd][tt] ∨ [hd][tt]).
We have tt ::

g g n (next m) : {Str g Bool | [hd][tt]} (Sub)Case of 2 ([hd][tt] ∨ [hd][tt]). Since m : {CoNat g | [S]} g : (CoNat g -→ {CoNat g | [S]} -→ {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])})
we get

g (next m) next(S (next m)) : {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])}
and the result follows.

Example E. [START_REF] Dreyer | A Relational Modal Logic for Higher-order Stateful ADTs[END_REF]. We have

fb Z (S Z) : {Str Bool | [box]23[hd][tt]}
Proof. By Ex. E.21 we have

fb g (unbox Z) (unbox (S Z)) : {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])} so that fb Z (S Z) : {Str g Bool | 2 ([hd][tt] ∨ [hd][tt])} Since the formula 2 ([hd][tt] ∨ [hd][tt]) is safe we get fb Z (S Z) : {Str Bool | [box]2 ([hd][tt] ∨ [hd][tt])}
Now, the result follows from the fact that

([hd][tt] ∨ [hd][tt]) ⇒ 3[hd][tt]
The following uses the rule

B→A ([ev(ψ 0 )]ϕ ∧ [ev(ψ 1 )]ϕ) ⇒ [ev(ψ 0 ∨ ψ 1 )]ϕ
Example E. [START_REF] Elliott | Functional Reactive Animation[END_REF]. We have

fb g : CoNat g -→ {CoNat g | [S]} -→ {Str g Bool | [hd][tt] ∨ [hd][tt]} Proof.
Let T be the type

{CoNat g → CoNat g → Str g Bool | [S] → → [hd][tt] ∧ [Z] → [S] → [hd][tt]} Note that T ≤ CoNat g -→ {CoNat g | [S]} -→ {Str g Bool | [hd][tt] ∨ [hd][tt]} Assume g : T Let M (g, c, m) := case c of | Z g → ff :: g g (next m) next(S g (next m)) | S g n → tt :: g g n (next m)
We show λc.λm.M (g, c, m) : T

We consider each conjunct separately.

Case of

[S] → → [hd][tt]. Assume c : {CoNat g | [S]}
Applying the (Inj 1 -E) rule, we are done since tt ::

g g n (next m) : {Str g Bool | [hd][tt]} assuming n : CoNat g Case of [Z] → [S] → [hd][tt]. Assume c : {CoNat g | [Z]} m : {CoNat g | [S]}
Applying the (Inj 0 -E) rule, we are left with showing ff :: g g (next m) next(S (next m)) :

{Str g Bool | [hd][tt]}
But the result is trivial since

g : {CoNat g → CoNat g → Str g Bool | [S] → → [hd]tt} A Scheduler
Example E. 24.

sched : Str Bool -→ Str A -→ Str B -→ Str(A + B) := λb.λs.λt. box ι (sched g (unbox b) (unbox s) (unbox t)) sched g : Str g Bool -→ Str g A -→ Str g B -→ Str g (A + B) := fix(g).λb.λs.λt. case (hd g b) of | tt → (in 0 (hd g s)) :: g g (tl g b) (tl g s) (tl g t) | ff → (in 1 (hd g t)) :: g g (tl g b) (tl g s) (tl g t)
Example E. [START_REF] Frittella | Monotone Modal Logics & Friends[END_REF]. We can give the following refinement types to sched :

{Str Bool | [box]23[hd][tt]} -→ Str A -→ Str B -→ {Str(A + B) | [box]23[hd][in 0 ] } {Str Bool | [box]23[hd][ff]} -→ Str A -→ Str B -→ {Str(A + B) | [box]23[hd][in 1 ] } Proof.
Direct, using the following Ex. E. [START_REF] Fujima | Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes[END_REF].

Example E. [START_REF] Fujima | Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes[END_REF]. We can give the following refinement types to sched g :

∀k • ∀ • Str g Bool 2 k 3 [hd][tt] -→ Str g A -→ Str g B -→ Str g (A + B) 2 k 3 [hd][in 0 ] ∀k • ∀ • Str g Bool 2 k 3 [hd][ff] -→ Str g A -→ Str g B -→ Str g (A + B) 2 k 3 [hd][in 1 ]
Proof. We only discuss the first type, since the second one is completely similar. Let T (k, ) be the type

Str g Bool 2 k 3 [hd][tt] -→ Str g A -→ Str g B -→ Str g (A + B) 2 k 3 [hd][in 0 ]
and assume g :

∀k • ∀ • T (k, ) Let M (g, b, s, t) := case (hd g b) of | tt → (in 0 (hd g s)) :: g g (tl g b) (tl g s) (tl g t) | ff → (in 1 (hd g t)) :: g g (tl g b) (tl g s) (tl g t) We show λb.λs.λt.M (g, b, s, t) : ∀k • ∀ • T (k, )
We apply the (∀-CI) rule on ∀k. In the case of ∀ • T (0, ), the result is trivial since

2 0 3 [hd][in 0 ] ⇔
As for ∀ • T (k+1, ), we apply the (∀-CI) rule, this time on ∀ . In the case of T (k+1, 0), since

2 k+1 3 0 [hd][tt] ⇔ 3 0 [hd][tt] ∧ 2 k 3 0 [hd][tt] and 3 0 [hd][tt] ⇔ ⊥ we get 2 k+1 3 0 [hd][tt] ⇔ ⊥
and we can conclude using the (ExF) rule. It remains to deal with the case of T (k+1, +1). We have to show

M (g, b, s, t) : Str g (A + B) 2 k+1 3 +1 [hd][in 0 ] assuming b : Str g Bool 2 k+1 3 +1 [hd][tt] s : Str g A t : Str g B
We have

2 k+1 3 +1 [hd][in 0 ] ⇔ 3 +1 [hd][in 0 ] ∧ 2 k 3 +1 [hd][in 0 ]
and we consider each conjunct separately.

Case of 3 +1

[hd][in 0 ] . Since 2 k+1 3 +1 [hd][tt] ⇔ 3 +1 [hd][tt] ∧ 2 k 3 +1 [hd][tt]
we have b :

Str g Bool 3 +1 [hd][tt] Using 3 +1 [hd][tt] ⇔ [hd][tt] ∨ 3 [hd][tt]
we reason by cases on the refinement type of b.

(Sub)Case of [hd][tt].
We apply the (Inj 0 -E) rule on b and we are done since (in 0 (hd g s)) :: g g (tl g b) (tl g s) (tl g t) :

{Str g (A + B) | [hd][in 0 ] } (Sub)Case of 3 [hd][tt].
We have tl g b :

Str g Bool 3 [hd][tt]
We apply the case-elimination rule on b. In both branches, since (by subtyping) g has type

Str g Bool 2 1 3 [hd][tt] -→ Str g A -→ Str g B -→ Str g (A + B) 2 1 3 [hd][in 0 ]
and since, according to Table 2,

2 1 θ ⇔ θ we get g (tl g b) (tl g s) (tl g t) : Str g (A + B) 3 [hd][in 0 ] so that (-) :: g g (tl g b) (tl g s) (tl g t) : Str g (A + B) 3 [hd][in 0 ]
and we are done since

3 [hd][in 0 ] ⇒ 3 +1 [hd][in 0 ] Case of 2 k 3 +1 [hd][in 0 ] . Since 2 k+1 3 +1 [hd][tt] ⇔ 3 +1 [hd][tt] ∧ 2 k 3 +1 [hd][tt]
we have b :

Str g Bool 2 k 3 +1 [hd][tt]
so that tl g b :

Str g Bool 2 k 3 +1 [hd][tt]
We apply the case-elimination rule on b. In both branches, since (by subtyping) g has type

Str g Bool 2 k 3 +1 [hd][tt] -→ Str g A -→ Str g B -→ Str g (A + B) 2 k 3 +1 [hd][in 0 ]
we get g (tl g b) (tl g s) (tl g t) :

Str g (A + B) 2 k 3 +1 [hd][in 0 ] so that (-) :: g g (tl g b) (tl g s) (tl g t) : Str g (A + B) 2 k 3 +1 [hd][in 0 ] E.

Colists

We detail here the refinement types given to the guarded and coinductive append functions on colists in Table 4. We present some basic material in §E. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]. The append function itself is detailed in §E.6, and we give sharper refinements with iteration terms in §E. [START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]. We begin in §E.6 with an overview of the main examples on colists.

Overview The cases of

append g : {CoList g A | [¬nil]} -→ CoList g A -→ {CoList g A | [¬nil]} append g : CoList g A -→ {CoList g A | [¬nil]} -→ {CoList g A | [¬nil]}
are detailed in Ex. E. [START_REF] Jacobs | Many-Sorted Coalgebraic Modal Logic: a Model-theoretic Study[END_REF].

We now discuss

append : {CoList A | [box][fin]} -→ {CoList A | [box][fin]} -→ {CoList A | [box][fin]}
which says that append takes finite colists to a finite colist. Recall that [fin] = 3[nil]. Details are given in Ex. E. [START_REF] Jeffrey | LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs[END_REF]. The other refinement types for append are detailed in Ex. E.36 and Ex. E. [START_REF] Jhala | HMC: Verifying functional programs using abstract interpreters[END_REF].

We refer here to the code of the append function as defined in Table 3 and Ex. E. [START_REF] Jacobs | Categorical Logic and Type Theory[END_REF]. First, since 3[nil] is smooth, we can apply the rule (µ-E) (Fig. 11) twice and reduce to

E box ι (append g (unbox s) (unbox t)) : {CoList A | [box]3[nil]} where E assumes s of type CoList A [box]3 k [nil] and t of type CoList A [box]3 [nil] .
Using the derived rule (µ-I) (Ex. 6.10), we further reduce to

E box ι (append g (unbox s) (unbox t)) : CoList A [box]3 k+ [nil]
Now, since the formulae 3 t [nil] are safe, by subtyping (Fig. 11) we have

E s : CoList A 3 k [nil] and E t : CoList A 3 [nil]
and we can reduce to showing that the guarded append g has type ∀k • ∀ • T (k, ), where

T (k, ) := CoList g A 3 k [nil] -→ CoList g A 3 [nil] -→ CoList g A 3 k+ [nil]
Let N (g, s, t) be such that append g = fix(g).λs.λt.N (g, s, t). We show

λs.λt.N (g, s, t) : ∀k • ∀ • T (k, )
in a typing context (leaved implicit) which assumes g of type ∀k • ∀ • T (k, ).

We apply the (∀-CI) rule on ∀k • ∀ • T (k, ). Since 3 0 [nil] ⇔ ⊥, the branch of ∀ •T (0, ) can be dealt with using the (ExF) rule. In the branch of ∀ •T (k+1, ), we apply the (∀-I) rule. We are thus left with showing

N (g, s, t) : CoList g A 3 k+ +1 [nil]
assuming further s :

CoList g A 3 k+1 [nil] and t : CoList g A 3 [nil] . We unfold 3 k+1 [nil] as 3 k+1 [nil] ⇔ [nil] ∨ 3 k [nil]
Using the (∨-E) rule, we have two cases for the refinement type of s. In the case

of {CoList A | [nil]}, since [nil] = [fold][in 0 ] , we have (unfold s) : [in 0 ]
. Thanks to the (Inj 0 ) rule, we are left with showing

t : CoList A 3 [nil] t : CoList A 3 k+1+ [nil]
But we are done since ≤ k+ +1 so that

3 [nil] ⇒ 3 k+1+ [nil] Assume now that s has type CoList A 3 k [nil] . By unfolding 3 k+ +1 [nil] we reduce to showing N (g, s, t) : CoList g A 3 k+ [nil]
Since, on colists, (-

) = [fold][in 1 ][π 1 ][next](-)
, we can apply the (Inj 1 -E) rule on (unfold s). This amounts to showing

Cons g x (g xs (next t)) : CoList A 3 k+ [nil]
where, since

(unfold s) : 1 + A × CoList g A [in 1 ][π 1 ][next]3 k [nil]
we can assume xs :

CoList g A 3 k [nil]
. By subtyping and (∀-E) we have g : T (k, ), so that

g xs (next t) : CoList A 3 k+ [nil]
and we conclude by the analogue of Ex. 5.3 for colists. The other typings for append are dealt with similarly. Let us finally just mention that the type of append g can be sharpened to

∀k•∀ • CoList g A 3 k [nil] -→ CoList g A 3 +1 [nil] -→ CoList g A 3 k+ [nil]
reflecting that on finite colists, append g removes one constructor Nil g from its arguments (see Ex. E.38).

Case of [nil].

We thus have

unfold(s) : {1 + A × CoList g A | [in 0 ] }
We apply the (Inj 0 -E) rule and get the result by

t : CoList g A 2 fin [hd]ϕ Case of [hd]ϕ ∧ 2 fin [hd]ϕ.
We thus have s :

CoList g A [hd]ϕ ∧ 2 fin [hd]ϕ
Since the modalities [fold] and [in 1 ] preserve ∧ this gives

s : CoList g A [fold][in 1 ] [π 0 ]ϕ ∧ [π 1 ][next]2 fin [hd]ϕ so that unfold(s) : 1 + A × CoList g A [in 1 ] [π 0 ]ϕ ∧ [π 1 ][next]2 fin [hd]ϕ
We then apply the (Inj 1 -E) rule. Assume

y : A × CoList g A [π 0 ]ϕ ∧ [π 1 ][next]2 fin [hd]ϕ and let x := π 0 (y) : {A | ϕ} xs := π 1 (y) : CoList g A 2 fin [hd]ϕ
Then Ex. E.31 easily gives

Cons g x (g xs (next t)) : CoList g A 2 fin [hd]ϕ
Example E. [START_REF] Jeffrey | LTL Types FRP: Linear-time Temporal Logic Propositions As Types, Proofs As Functional Reactive Programs[END_REF].

append : {CoList A | [box]3[nil]} -→ {CoList A | [box]3[nil]} -→ {CoList A | [box]3[nil]} append g : ∀k • ∀ • CoList g A 3 k [nil] -→ CoList g A 3 [nil] -→ CoList g A 3 k+ [nil] Proof. Let T (k, ) := CoList g A 3 k [nil] -→ CoList g A 3 [nil] -→ CoList g A 3 k+ [nil]
and assume g :

∀k • ∀ • T (k, ) Let M (g, s, t) := case s of | Nil g → t | Cons g x xs → Cons g x (g xs (next t))
We show λs.λt.M (g, s, t)

: ∀k • ∀ • T (k, )
We apply the (∀-CI) rule on ∀k. This leads to two cases.

Case of ∀ • T (0, ).

Apply the (∀-I) rule on ∀ and assume s :

{CoList g A | 3 0 [nil]} Since 3 0 [nil] ⇔ ⊥
the result follows using the rule (ExF). Case of ∀ • T (k+1, ).

Apply the (∀-I) rule on ∀ and assume s :

CoList g A 3 k+1 [nil] t : CoList g A 3 [nil]
We have to show

M (g, s, t) : CoList g A 3 k+1+ [nil] Using 3 k+1 [nil] ⇔ [nil] ∨ 3 k [nil]
we apply the (∨-E) rule on the refinement type of s. This leads to two subcases.

(Sub)Case of [nil].

We have unfold(s) :

{1 + A × CoList g A | [in 0 ] } Since ≤ k+1 + , the result then follows by applying the (Inj 0 -E) rule. (Sub)Case of 3 k [nil].
We have unfold(s) :

1 + A × CoList g A [in 1 ][π 1 ][next]3 k [nil]
Using the (Inj 1 -E) rule we are left with showing

Cons g x (g xs (next t)) : CoList g A 3 (k+ )+1 [nil]
where x := π 0 (y) : A xs := π 1 (y) :

CoList g A 3 k [nil] assuming y : A × CoList g A [π 1 ][next]3 k [nil]
We have g xs (next t) :

CoList g A 3 k+ [nil]
It follows that

Cons g x (g xs (next t)) : CoList g A 3 k+ [nil]
and we are done since

3 k+ [nil] ⇒ 3 (k+ )+1 [nil]
Example E. [START_REF] Jeltsch | An Abstract Categorical Semantics for Functional Reactive Programming with Processes[END_REF]. Assuming ϕ : A,

append : {CoList A | [box]3[hd]ϕ} -→ CoList A -→ {CoList A | [box]3[hd]ϕ} append g : ∀k • CoList g A 3 k [hd]ϕ -→ CoList g A -→ CoList g A 3 k [hd]ϕ
where, in the case of append, ϕ : A is safe and smooth.

Proof.

Let

T (k) := CoList g A 3 k [hd]ϕ -→ CoList g A -→ CoList g A 3 k [hd]ϕ and assume g : ∀k • T (k) Let M (g, s, t) := case s of | Nil g → t | Cons g x xs → Cons g x (g xs (next t))
We show λs.λt.M (g, s, t)

: ∀k • T (k)
We apply the (∀-CI) rule on ∀k. This leads to two cases.

Case of T (0). Assume s :

{CoList g A | 3 0 [hd]ϕ} Since 3 0 [hd]ϕ ⇔ ⊥
the result follows using the rule (ExF).

Case of T (k+1).

Assume s :

CoList g A 3 k+1 [hd]ϕ t : CoList g A Using 3 k+1 [hd]ϕ ⇔ [hd]ϕ ∨ 3 k [hd]ϕ
we apply the (∨-E) rule on the refinement type of s. This leads to two subcases.

(Sub)Case of [hd]ϕ.

We have unfold(s) : We have

{1 + A × CoList g A | [in 1 ][π 0 ]
unfold(s) : 1 + A × CoList g A [in 1 ][π 1 ][next]3 k [hd]ϕ
Using the (Inj 1 -E) rule we are left with showing

Cons g x (g xs (next t)) : CoList g A 3 k+1 [hd]ϕ
where x := π 0 (y) : A xs := π 1 (y) :

CoList g A 3 k [hd]ϕ assuming y : A × CoList g A [π 1 ][next]3 k [hd]ϕ
We have g xs (next t) :

CoList g A 3 k [hd]ϕ
It follows that

Cons g x (g xs (next t)) : CoList g A 3 k [hd]ϕ
and we are done since

3 k [hd]ϕ ⇒ 3 k+1 [hd]ϕ
Example E. [START_REF] Jhala | HMC: Verifying functional programs using abstract interpreters[END_REF]. Assuming ϕ : A, we have

append : {CoList A | [box]3[nil]} -→ {CoList A | [box]3[hd]ϕ} -→ {CoList A | [box]3[hd]ϕ} append g : ∀k • ∀ • CoList g A 3 k [nil] -→ CoList g A 3 [hd]ϕ -→ CoList g A 3 k+ [hd]ϕ
where, in the case of append, ϕ : A is safe and smooth.

where

x := π 0 (y) : A xs := π 1 (y) :

CoList g A 3 k [nil] assuming y : A × CoList g A [π 1 ][next]3 k [nil]
We have g xs (next t) :

CoList g A 3 k+ [hd]ϕ
It follows that

Cons g x (g xs (next t)) : CoList g A 3 k+ [hd]ϕ
and we are done since

3 k+ [hd]ϕ ⇒ 3 (k+ )+1 [hd]ϕ
Sharper Refinements for the Append Function on Colists

Example E. [START_REF] Johnstone | Sketches of an Elephant: A Topos Theory Compendium[END_REF].

append g : ∀k • ∀ • CoList g A 3 k [nil] -→ CoList g A 3 +1 [nil] -→ CoList g A 3 k+ [nil] Proof. Let T (k, ) := CoList g A 3 k [nil] -→ CoList g A 3 +1 [nil] -→ CoList g A 3 k+ [nil]
and assume g :

∀k • ∀ • T (k, ) Let M (g, s, t) := case s of | Nil g → t | Cons g x xs → Cons g x (g xs (next t))
We show λs.λt.M (g, s, t)

: ∀k • ∀ • T (k, )
We apply the (∀-CI) rule on ∀k. This leads to two cases.

Case of ∀ • T (0, ).

Apply the (∀-I) rule on ∀ and assume s :

{CoList g A | 3 0 [nil]} Since 3 0 [nil] ⇔ ⊥
the result follows using the rule (ExF).

Case of ∀ • T (k+1, ).

Apply the (∀-I) rule on ∀ and assume s :

CoList g A 3 k+1 [nil] t : CoList g A 3 +1 [nil]
We have to show M (g, s, t) :

CoList g A 3 k+1+ [nil] Using 3 k+1 [nil] ⇔ [nil] ∨ 3 k [nil]
we apply the (∨-E) rule on the refinement type of s. This leads to two subcases.

(Sub)Case of [nil].

We have unfold(s) :

{1 + A × CoList g A | [in 0 ] }
Since +1 ≤ k+1+ , the result then follows by applying the (Inj

0 -E) rule. (Sub)Case of 3 k [nil].
We have

unfold(s) : 1 + A × CoList g A [in 1 ][π 1 ][next]3 k [nil]
Using the (Inj 1 -E) rule we are left with showing

Cons g x (g xs (next t)) : CoList g A 3 k+1+ [nil]
where x := π 0 (y) : A xs := π 1 (y) :

CoList g A 3 k [nil] assuming y : A × CoList g A [π 1 ][next]3 k [nil]
We have g xs (next t) :

CoList g A 3 k+ [nil]
It follows that

Cons g x (g xs (next t)) : CoList g A 3 k+ [nil]
and we are done since

3 k+ [nil] ⇒ 3 k+1+ [nil]
Example E. [START_REF] Jones | Linear-time Breadth-first Tree Algorithms: An Exercise in the Arithmetic of Folds and Zips[END_REF]. Assuming ϕ : A, we have

append g : ∀k • ∀ • CoList g A 3 k [nil] -→ CoList g A 3 +1 [hd]ϕ -→ CoList g A 3 k+ [hd]ϕ (Sub)Case of 3 k [nil].
We have unfold(s) :

1 + A × CoList g A [in 1 ][π 1 ][next]3 k [nil]
Using the (Inj 1 -E) rule we are left with showing Cons g x (g xs (next t)) : CoList g A 3 k+1+ [hd]ϕ where x := π 0 (y) : A xs := π 1 (y) :

CoList g A 3 k [nil] assuming y : A × CoList g A [π 1 ][next]3 k [nil]
We have g xs (next t) :

CoList g A 3 k+ [hd]ϕ
It follows that

Cons g x (g xs (next t)) : CoList g A 3 k+ [hd]ϕ
and we are done since

3 k+ [hd]ϕ ⇒ 3 k+1+ [hd]ϕ E.

Resumptions

This example is adapted from [48]. 42. Let ψ : A be a safe and smooth formula and let ϕ ∈ {[Ret], [now]ψ}. We have

sched g : Res g A -→ Res g A -→ Res g A := fix(g).λp.λq. case p of | Ret g a → Ret g a | Cont g k → let h = λi. let o, t = ki in o, g (next q) t in Cont g h Example E.
sched : {Res A | [box]∃3ϕ} -→ {Res A | [box]∃3ϕ} -→ {Res A | [box]∃3ϕ} sched : {Res A | [box]∀3ϕ} -→ {Res A | [box]∀3ϕ} -→ {Res A | [box]∀3ϕ} sched g : ∀k • ∀ • Res g A ∃3 k ϕ -→ Res g A ∃3 ϕ -→ Res g A ∃3 k+ ϕ sched g : ∀k • ∀ • Res g A ∀3 k ϕ -→ Res g A ∀3 ϕ -→ Res g A ∀3 k+ ϕ Proof. Let 3 ∈ {∃3, ∀3} and
T (k, ) := Res g A 3 k ϕ -→ Res g A 3 ϕ -→ Res g A 3 k+ ϕ and assume g : ∀k • ∀ • T (k, ) Let M (g, p, q) := case p of | Ret g a → Ret g a | Cont g k → let h = λi. let o, t = ki in o, g (next q) t in Cont g h We show λp.λq.M (g, p, q) : ∀k • ∀ • T (k, )
We apply the (∀-CI) rule on ∀k. In the case of ∀ • T (0, ), we get the result using the (ExF) rule since 3 0 ϕ ⇔ ⊥

As for ∀ • T (k+1, ), we apply the (∀-I) rule on ∀ . We have to show M (g, p, q) : Res g A 3 k+ +1 ϕ assuming p :

Res g A 3 k+1 ϕ q : Res g A 3 ϕ Using ∃3 k+1 ϕ ⇔ ϕ ∨ ∃3 k ϕ ∀3 k+1 ϕ ⇔ ϕ ∨ ∀3 k ϕ
we reason by cases on the refinement type of p. We apply the (∨-E) rule on the refinement type of p. So let i ∈ I and assume p :

Case of

Res g A i ∃3 k ϕ
We have

unfold p : A + (O × Res g A) I [in 1 ] [i] → [π 1 ][next]∃3 k ϕ
We apply the (Inj 1 -E) rule on the refinement type of p. Let

N (g, k, q) := let h = λi. let o, t = ki in o, g (next q) t in Cont g h We show N (g, k, q) : Res g A i ∃3 k+ ϕ assuming k : (O × Res g A) I [i] → [π 1 ][next]∃3 k ϕ Assuming i : {I | [i]} we thus have ki : O × Res g A [π 1 ][next]∃3 k ϕ It follows that π 0 (ki) , g (next q) (π 1 (ki)) : O × Res g A [π 1 ][next]∃3 k+ ϕ and thus λi. π 0 (ki) , g (next q) (π 1 (ki)) : (O × Res g A) I [i] → [π 1 ][next]∃3 k+ ϕ Now we are done since i ∃3 k+ ϕ = [fold][in 1 ] [i] → [π 1 ][next]∃3 k+ ϕ and Cont g = λh. fold(in 1 h) Case of ∀3 k ϕ. Using ∀3 k+ +1 ϕ ⇔ ϕ ∨ ∀3 k+ ϕ for each i ∈ I we show M (g, p, q) : Res g A i ∀3 k+ ϕ So let i ∈ I. Since p : Res g A ∃3 k ϕ
We have

unfold p : A + (O × Res g A) I [in 1 ] [i] → [π 1 ][next]∃3 k ϕ
and we conclude similarly as in the case of ∃3 k ϕ.

Example E. [START_REF]7 The Safe Fragment[END_REF] Proof. We show that we can give the following refinement type to sched g :

∀k•∀ 0 •∀ 1 • Res g A 2 k 3 0 [out]ϑ -→ Res g A 2 k 3 1 [out]ϑ -→ Res g A 2 k 3 0 + 1 [out]ϑ
Let T (k, 0 , 1 ) be the type

Res g A 2 k 3 0 [out]ϑ -→ Res g A 2 k 3 1 [out]ϑ -→ Res g A 2 k 3 0 + 1 [out]ϑ and assume g : ∀k • ∀ 0 • ∀ 1 • T (k, 0 , 1 ) Let M (g, p, q) := case p of | Ret g a → Ret g a | Cont g k → let h = λi. let o, t = ki in o, g (next q) t in Cont g h We show λp.λq.M (g, p, q) : ∀k • ∀ 0 • ∀ 1 • T (k, 0 , 1 )
We apply the (∀-CI) rule on ∀k. The case of ∀ 0 • ∀ 1 • T (0, 0 , 1 ) is trivial since

2 0 3 0+ 1 [out]ϑ ⇔ As for ∀ 0 • ∀ 1 • T (k+1, 0 , 1 )
, we apply the (∀-CI) rule, this time on ∀ 0 . In the case of ∀ 1 • T (k+1, 0, 1 ), since 2 k+1 3 0 [out]ϑ is of the form

3 0 [out]ϑ ∧ ψ while 3 0 [out]ϑ ⇔ ⊥
we can conclude using the (ExF) rule. It remains to deal with the case of ∀ 1 • T (k+1, 0 +1, 1 ). We apply the (∀-I) rule on ∀ 1 . We show

M (g, p, q) : Res g A 2 k+1 3 0+ 1+1 [out]ϑ assuming p : Res g A 2 k+1 3 0+1 [out]ϑ q : Res g A 2 k+1 3 1 [out]ϑ
We will apply the (Inj 1 -E) rule on (unfold p) and show

N (g, k, q) : Res g A 2 k+1 3 0+ 1+1 [out]ϑ
where N (g, k, q) := let h = λi. let o, t = ki in o, g (next q) t in Cont g h and under suitable assumption on the refinement type of k. We have

∀2 k+1 3 0+ 1+1 [out]ϑ ⇔ 3 0+ 1+1 [out]ϑ ∧ ∀2 k 3 0+ 1+1 [out]ϑ ∃2 k+1 3 0+ 1+1 [out]ϑ ⇔ 3 0 + 1 +1 [out]ϑ ∧ ∃2 k 3 0+ 1+1 [out]ϑ
and we consider each conjunct separately.

Cases of 3 0+ 1+1 [out]ϑ.

We have p : We show N (g, k, q) :

Res g A 3 0+1 [out]ϑ Using ∃3 0+1 [out]ϑ ⇔ [out]ϑ ∨ ∃3 0 [out]ϑ ∀3 0+1 [out]ϑ ⇔ [out]ϑ ∨ ∀3 0 [out
Res g A ∃3 0+ 1 [out]ϑ
We apply the (∨-E) rule on the refinement type of p. So let i ∈ I and assume p :

Res g A i ∃3 0 [out]ϑ This amounts to k : (O × Res g A) I [i] → [π 1 ][next]∃3 0 [out]ϑ Assuming i : {I | [i]} we thus have ki : O × Res g A [π 1 ][next]∃3 0 [out]ϑ
since (by subtyping) g has type

Res g A 2 1 ∃3 0 [out]ϑ -→ Res g A 2 1 ∃3 1 [out]ϑ -→ Res g A 2 1 ∃3 0+ 1 [out]ϑ
and since, according to Table 2,

2 1 θ ⇔ θ it follows that π 0 (ki) , g (next q) (π 1 (ki)) : O × Res g A [π 1 ][next]∃3 0+ 1 [out]ϑ
We thus get λi. π 0 (ki) , g (next q) (π 1 (ki)) : (O × Res g A)

I [i] → [π 1 ][next]∃3 0+ 1 [out]ϑ
Now we are done since

i ∃3 0+ 1 [out]ϑ = [fold][in 1 ] [i] → [π 1 ][next]∃3 0+ 1 [out]ϑ and Cont g = λh. fold(in 1 h) (Sub)Case of ∀3 0 [out]ϑ. We show N (g, k, q) : Res g A ∀3 0 + 1 [out]ϑ
Hence, for each i ∈ I we have to show

N (g, k, q) : Res g A i ∀3 0 + 1 [out]ϑ So let i ∈ I. Since p : Res g A i ∀3 0 [out]ϑ we have k : (O × Res g A) I [i] → [π 1 ][next]∀3 0 [out]ϑ
and we conclude similarly as in the case of

∃3 0 [out]ϑ. Case of ∀2 k 3 0 + 1 +1 [out]ϑ.
For each i ∈ I we have to show

N (g, k, q) : Res g A i ∀2 k 3 0+ 1+1 [out]ϑ So let i ∈ I. Since p : Res g A i ∀2 k 3 0+1 [out]ϑ we have k : (O × Res g A) I [i] → [π 1 ][next]∀2 k 3 0+1 [out]ϑ Assuming i : {I | [i]} we thus have ki : O × Res g A [π 1 ][next]∀2 k 3 0+1 [out]ϑ
and it follows that

λi. π 0 (ki) , g (next q) (π 1 (ki)) : (O × Res g A) I [i] → [π 1 ][next]∀2 k 3 0 + 1 +1 [out]ϑ Now we are done since i ∀2 k ∃3 0+ 1+1 [out]ϑ = [fold][in 1 ] [i] → [π 1 ][next]∀2 k ∃3 0+ 1+1 [out]ϑ and Cont g = λh. fold(in 1 h) Case of ∃2 k 3 0 + 1 +1 [out]ϑ.
We have to show

N (g, k, q) : Res g A ∃2 k 3 0+ 1+1 [out]ϑ
We apply the (∨-E) rule on the refinement type of p. So let i ∈ I and assume p :

Res g A i ∃2 k 3 0+1 [out]ϑ
We have

k : (O × Res g A) I [i] → [π 1 ][next]∃2 k 3 0+1 [out]ϑ
and we conclude similarly as in the case of ∀2 k 3 0+ 1+1 [out]ϑ.

Example E. 44. Let 2 ∈ {∀2, ∃2} and 3 ∈ {∀3, ∃3}. We have

sched : {Res A | [box]23[Ret]} -→ {Res A | [box]23[Ret]} -→ {Res A | [box]23[Ret]} Proof.
We show that we can give the following refinement type to sched g :

∀k•∀ 0 •∀ 1 • Res g A 2 k 3 0 [Ret] -→ Res g A 2 k 3 1 [Ret] -→ Res g A 2 k 3 0+ 1 [Ret]
Let T (k, 0 , 1 ) be the type

Res g A 2 k 3 0 [Ret] -→ Res g A 2 k 3 1 [Ret] -→ Res g A 2 k 3 0+ 1 [Ret]
and assume g :

∀k • ∀ 0 • ∀ 1 • T (k, 0 , 1 ) Let M (g, p, q) := case p of | Ret g a → Ret g a | Cont g k → let h = λi. let o, t = ki in o, g (next q) t in Cont g h We show λp.λq.M (g, p, q) : ∀k • ∀ 0 • ∀ 1 • T (k, 0 , 1 )
We apply the (∀-CI) rule on ∀k. The case of ∀ 0 • ∀ 1 • T (0, 0 , 1 ) is trivial since

2 0 3 0+ 1 [Ret] ⇔ As for ∀ 0 • ∀ 1 • T (k+1, 0 , 1 )
, we apply the (∀-CI) rule, this time on ∀ 0 . In the case of ∀ 1 • T (k+1, 0, 1 ), since 2 k+1 3 0 [Ret] is of the form

3 0 [Ret] ∧ ψ while 3 0 [Ret] ⇔ ⊥
we can conclude using the (ExF) rule. It remains to deal with the case of ∀ 1 • T (k+1, 0 +1, 1 ). We apply the (∀-I) rule on ∀ 1 . We show

M (g, p, q) : Res g A 2 k+1 3 0+ 1+1 [Ret] assuming p : Res g A 2 k+1 3 0+1 [Ret] q : Res g A 2 k+1 3 1 [Ret]
We have

∀2 k+1 3 0+ 1+1 [Ret] ⇔ 3 0+ 1+1 [Ret] ∧ ∀2 k 3 0+ 1+1 [Ret] ∃2 k+1 3 0+ 1+1 [Ret] ⇔ 3 0+ 1+1 [Ret] ∧ ∃2 k 3 0+ 1+1 [Ret]
and we consider each conjunct separately.

Cases of 3 0+ 1+1 [Ret].
We have p :

Res g A 3 0 +1 [out]ϑ Using ∃3 0+1 [Ret] ⇔ [Ret] ∨ ∃3 0 [Ret] ∀3 0+1 [Ret] ⇔ [Ret] ∨ ∀3 0 [Ret]
we reason by cases on the refinement type of p. In the case of [Ret], apply the (Inj 0 -E) rule on (unfold p), and we conclude similarly as in Ex. E.42. In the other cases, we apply the (Inj 1 -E) rule on (unfold p) and show N (g, k, q) :

Res g A 3 0+ 1+1 [Ret]
where N (g, k, q) := let h = λi. let o, t = ki in o, g (next q) t in Cont g h and under suitable assumption on the refinement type of k. We can then conclude similarly as in Ex. E. [START_REF]7 The Safe Fragment[END_REF].

Cases of 2 k 3 0+ 1+1 [Ret].
We apply the (Inj 1 -E) rule on (unfold p) and show

N (g, k, q) : Res g A 2 k+1 3 0 + 1 +1 [Ret]
where N (g, k, q) := let h = λi. let o, t = ki in o, g (next q) t in Cont g h and under suitable assumption on the refinement type of k. We can then conclude similarly as in Ex. E. [START_REF]7 The Safe Fragment[END_REF].

Example E. 47 : [START_REF] Krishnaswami | Ultrametric Semantics of Reactive Programs[END_REF]. Note that we have, at type CoList g (Tree g A),

Tree g A -→ {CoList g A | [¬nil]} bftaux g : {CoList g (Tree g A) | [¬nil]} -→ {CoList g A | [¬nil]} Example E.
[¬nil] ∧ 2 fin [hd]∀2[lbl]ϕ ⇔ [¬nil] ∧ [nil] ∨ [hd]∀2[lbl]ϕ ∧ 2 fin [hd]∀2[lbl]ϕ ⇔ [¬nil] ∧ [nil] ∨ [¬nil] ∧ [hd]∀2[lbl]ϕ ∧ 2 fin [hd]∀2[lbl]ϕ
Since the modality [fold] preserves ∧ and ⊥ (Table 2), we have

[¬nil] ∧ [nil] ⇒ ⊥
We apply the (∨-E) rule on the refinement type of s. The branch of [¬nil] ∧ [nil] is dealt-with using the rule (ExF). It remains to handle the case of

s : CoList g (Tree g A) [¬nil] ∧ [hd]∀2[lbl]ϕ ∧ 2 fin [hd]∀2[lbl]ϕ
Since the modalities [fold] and [in 1 ] preserve ∧ we have

unfold(s) : 1 + Tree g A × CoList g (Tree g A) [in 1 ] [π 0 ]ϕ ∧ [π 1 ][next]2 fin [hd]∀2[lbl]ϕ
Using the typing rule (Inj 1 -E) (Fig. 8) and Ex. E. [START_REF] Koskinen | Local Temporal Reasoning[END_REF]

A := Fix(X). 1 + (( X → A) → A) so that Rou g (CoList g A) := Fix(X). 1 + (( X → CoList g A) → CoList g A)
The constructors of Rou g A are

Over g := fold(in 0 ) : Rou g A Cont g := λf.fold(in 1 f ) : ( Rou g A → A) → A → Rou g A
We can thus apply the (Inj 1 -E) rule, which leads us to showing

f (λx. g x) : {B | ϕ} assuming f : {( Rou g B → B) → B | ([next][Rou]ϕ → [next]ϕ) → ϕ} that is f : ( {Rou g B | [Rou]ϕ} → {B | ϕ}) -→ {B | ϕ}
But this is trivial, by assumption on the type of g.

Example E. 53. Assuming ϕ : A we have

unfold : Rou g A -→ Rou g A -→ {A | ϕ} -→ {A | ϕ} Proof. Assume c : Rou g A k : Rou g A -→ {A | ϕ} f : {Rou g A | [Rou]ϕ} -→ {A | ϕ} -→ {A |
A | ∀2[lbl]ψ} -→ Rou g (CoList g A) -→ {Rou g (CoList g A) | [Rou]2[hd]ψ} Let T := {Tree g A | ∀2[lbl]ψ} -→ Rou g (CoList g A) -→ {Rou g (CoList g A) | [Rou]2[hd]ψ} and assume g : T t : {Tree g A | ∀2[lbl]ϕ} c : Rou g (CoList g A) Case of B ψ ⇒ φ ϕ : A B→A [ev(φ)]ϕ ⇒ [ev(ψ)]ϕ
Let x ∈ Γ B → A and assume that x ∈ {|[ev(φ)]ϕ|}. Let furthermore y ∈ Γ B such that y ∈ {|ψ|}. We have to show ev • x, y ∈ {|ϕ|}. By induction hypothesis we have y ∈ {|ψ ⇒ φ|}, so that y ∈ {|φ|}. But this implies ev

• x, y ∈ {|ϕ|} since x ∈ {|[ev(φ)]ϕ|}. Case of B→A ([ev(ψ 0 )]ϕ ∧ [ev(ψ 1 )]ϕ) ⇒ [ev(ψ 0 ∨ ψ 1 )]ϕ Let x ∈ Γ B → A and assume that x ∈ {|([ev(ψ 0 )]ϕ ∧ [ev(ψ 1 )]ϕ)|}. Let furthermore y ∈ Γ B such that y ∈ {|ψ 0 ∨ ψ 1 |}.
A0+A1 [in 0 ] ∨ [in 1 ] ∧ ¬ [in 0 ] ∧ [in 1 ] Consider x ∈ Γ A 0 + A 1 Γ A 0 + Γ A 1 (via Lem. D .
2). Hence x = in i (y) for some y ∈ Γ A i and we have x ∈ {|[in i ] |}. Moreover, since the injections in 0 and in 1 have disjoint images, we have {|

[in 0 ] ∧ [in 1 ] |} = ∅ so x ∈ {|¬([in 0 ] ∧ [in 1 ] )|}. Case of A0+A1 [in i ] ⇒ (¬[in i ]ϕ ⇔ [in i ]¬ϕ) Let x ∈ Γ A 0 + A 1 Γ A 0 + Γ A 1
, and assume x ∈ {|[in i ] |}, so that x = in i (y) for some (unique) y ∈ Γ A i . We show

x ∈ {|¬[in i ]ϕ ⇒ [in i ]¬ϕ|} and x ∈ {|[in i ]¬ϕ ⇒ ¬[in i ]ϕ|}
For the former, assume x / ∈ {|[in i ]ϕ|}. Since y is unique such that x = in i (y), we have y / ∈ {|ϕ|}. But this implies y ∈ {|¬ϕ|} and we are done. For the latter, assume x ∈ {|[in i ]¬ϕ|}. Assume toward a contradiction that x ∈ {|[in i ]ϕ|}. Since y is unique such that x = in i (y), we have both y / ∈ {|ϕ|} and y ∈ {|ϕ|}, a contradiction.

Cases of

A ν 0 αϕ ⇔ A ν t+1 αϕ ⇔ ϕ[ν t αϕ/α] A µ 0 αϕ ⇔ ⊥ A µ t+1 αϕ ⇔ ϕ[µ t αϕ/α] By definition of {|θ t αϕ|}. Cases of t ≥ u A ν t αϕ ⇒ ν u αϕ t ≤ u A µ t αϕ ⇒ µ u αϕ
These cases follows from Lem. F.4 (in θ t αϕ we assume that α is positive in ϕ) and the definition of {|θ t αϕ|}.

Cases of

A ν αϕ ⇒ ϕ[ν αϕ/α] A ψ ⇒ ϕ[ψ/α] A ψ ⇒ ν αϕ A ϕ[µαϕ/α] ⇒ µαϕ A ϕ[ψ/α] ⇒ ψ A µαϕ ⇒ ψ
By Lem. F.4 and the Knaster-Tarski Theorem.

Cases of

A µ t αϕ(α) ⇒ µαϕ(α) A ν αϕ(α) ⇒ ν t αϕ(α)
We

+ = Q + 0 × Q + 1 .
Then we are done since by induction hypothesis

x ∈ {|[π i ]ϕ|} ( D 1 , . . . , D k ) iff π i • x ∈ {|ϕ|} ( D 1 , . . . , D k ) iff π i • x ∈ {|ϕ|} (D 1 , . . . , D k ) iff ∀S 1 ∈ D 1 , . . . , S k ∈ D k , π i • x ∈ {|ϕ|} (D 1 , . . . , D k ) iff ∀S 1 ∈ D 1 , . . . , S k ∈ D k , x ∈ {|[π i ]ϕ|} (D 1 , . . . , D k ) iff x ∈ {|[π i ]ϕ|} (D 1 , . . . , D k ) Case of [in i ]ϕ.
Let D 1 ⊆ P(Γ P + 1 ), . . . , D k ⊆ P(Γ P + k ) be codirected. Let x ∈ Γ P + and write

P + = Q + 0 + Q + 1 . By Lem. D.
) iff ∀S 1 ∈ D 1 , . . . , S k ∈ D k , x ∈ {|[in i ]ϕ|} (D 1 , . . . , D k ) iff x ∈ {|[in i ]ϕ|} (D 1 , . . . , D k ) Case of [next]ϕ.
Let D 1 ⊆ P(Γ P + 1 ), . . . , D k ⊆ P(Γ P + k ) be codirected. Let x ∈ Γ P + and write P + = Q + . By Lem. D.2, we have x = next • y for some unique y ∈ Γ Q + . Then we are done since by induction hypothesis we have

x ∈ {|[next]ϕ|} ( D 1 , . . . , D k ) iff y ∈ {|ϕ|} ( D 1 , . . . , D k ) iff y ∈ {|ϕ|} (D 1 , . . . , D k ) iff ∀S 1 ∈ D 1 , . . . , S k ∈ D k , y ∈ {|ϕ|} (D 1 , . . . , D k ) iff ∀S 1 ∈ D 1 , . . . , S k ∈ D k , x ∈ {|[next]ϕ|} (D 1 , . . . , D k ) iff x ∈ {|[next]ϕ|} (D 1 , . . . , D k ) Case of [fold]ϕ.
This case is dealt-with similarly as that of [π i ].

Case of [box]ϕ.

Trivial since ϕ is required to be closed. Case of [ev(ψ)]ϕ.

Note that ψ is assumed to be closed since [ev(ψ)]ϕ is safe. Let D 1 ⊆ P(Γ P + 1 ), . . . , D k ⊆ P(Γ P + k ) be codirected. Let x ∈ Γ P + and write P + = R + → Q + . Then we are done since by induction hypothesis we have

x ∈ {|[ev(ψ)]ϕ|} ( D 1 , . . . , D k ) iff ∀y ∈ {|ψ|} , ev • x, y ∈ {|ϕ|} ( D 1 , . . . , D k ) iff ∀y ∈ {|ψ|} , ev • x, y ∈ {|ϕ|} (D 1 , . . . , D k ) iff ∀S 1 ∈ D 1 , . . . , S k ∈ D k , ∀y ∈ {|ψ|} , ev • x, y ∈ {|ϕ|} (S 1 , . . . , S k ) iff ∀S 1 ∈ D 1 , . . . , S k ∈ D k , x ∈ {|[ev(ψ)]ϕ|} (S 1 , . . . , S k ) iff x ∈ {|[ev(ψ)]ϕ|} (D 1 , . . . , D k ) Cases of θ t αϕ.
By induction hypothesis, the function

{|ϕ|} : P(Γ P + 1 )ו • •×P(Γ P + k )×P(Γ P + ) -→ P(Γ P + ), v, S -→ {|ϕ|} v[S/α]
is Scott-cocontinuous. Hence by Lem. F.

)(n). But this implies t / ∈ ϕ ∨ ψ (A 1 , . . . , A k )(n), a contradiction. Case of [π i ]ϕ.
Let D 1 ⊆ Sub( P + 1 ), . . . , D k ⊆ Sub( P + k ) be codirected. We show that for all n > 0 we have

[π i ]ϕ ( D 1 , . . . , D k )(n) = [π i ]ϕ (D 1 , . . . , D k )(n)
and this goes similarly as for {|-|}.

Case of [in

i ]ϕ.
Let D 1 ⊆ Sub( P + 1 ), . . . , D k ⊆ Sub( P + k ) be codirected. We show that for all n > 0 we have

[in i ]ϕ ( D 1 , . . . , D k )(n) = [in i ]ϕ (D 1 , . . . , D k )(n)
and this goes similarly as for {|-|} since the pointwise maps (in j ) n : Q

+ j (n) → Q + 0 (n) + Q + 1 (n) are injective. Case of [next]ϕ.
Let D 1 ⊆ Sub( P + 1 ), . . . , D k ⊆ Sub( P + k ) be codirected. Write P + = Q + . We show that for all n > 0 we have

[next]ϕ ( D 1 , . . . , D k )(n) = [next]ϕ (D 1 , . . . , D k )(n) The result is trivial if n = 1. For n > 1, it reduces to ϕ ( D 1 , . . . , D k )(n -1) = ϕ (D 1 , . . . , D k )(n -1)
which follows from the induction hypothesis.

Case of [fold]ϕ.

This case is handled similarly as that of [π i ].

Case of [box]ϕ.

Trivial since ϕ is required to be closed.

Case of ψ ⇒ ϕ. This case cannot occur since ψ ⇒ ϕ is not safe. Case of [π i ]ϕ.

Let x ∈ Γ P + and write

P + = Q + 0 × Q + 1 .
Then we are done since (π i • x) n (•) = π i (x n (•)) so that by induction hypothesis we have

x ∈ {|[π i ]ϕ|} iff π i • x ∈ {|ϕ|} iff ∀n > 0, (π i • x) n (•) ∈ ϕ (n) iff ∀n > 0, x n (•) ∈ [π i ]ϕ (n) Case of [in i ]ϕ.
Let x ∈ Γ P + and write

P + = Q + 0 + Q + 1 .
By Lem. D.2, we have x = in j • y for some unique j ∈ {0, 1} and y ∈ Γ Q + j . Then we are done since x n (•) = (in j • y) n (•) = in j (y n (•)) so that by induction hypothesis we have

x ∈ {|[in i ]ϕ|} iff j = i and y ∈ {|ϕ|} iff j = i and ∀n > 0, y n (•) ∈ ϕ (n) iff ∀n > 0, x n (•) ∈ [in i ]ϕ (n) Case of [next]ϕ.
Let x ∈ Γ P + and write P + = Q + . By Lem. D. Recall that ϕ is required to be closed. Also, by definition we have

(•) = y n-1 (•), so that x n (•) ∈ [next]ϕ (n) = ϕ (n -1). Assume conversely that x n (•) ∈ [next]ϕ (n) for all n > 0.
[box]ϕ A (n) := t ∈ A (n) = Γ A t ∈ {|ϕ|} A {|[box]ϕ|} A := x ∈ Γ A x 1 (•) ∈ {|ϕ|} A It follows that given x ∈ Γ A , we have x ∈ {|[box]ϕ|} A iff x 1 (•) ∈ {|ϕ|} A iff ∀n > 0, x n (•) ∈ {|ϕ|} A iff ∀n > 0, x n (•) ∈ [box]ϕ A (n)
Case of [ev(ψ)]ϕ. This case cannot occur since P + is assumed to be strictly positive.

Case of [ev(ψ)]ϕ.

Since [ev(ψ)]ϕ is smooth, the formula ψ is closed and we have Q + = B → R + where B is constant. Since B is constant, by Lem. D.4 there is a set A such that B ∆A, so that Γ B A by Lem. D.2. Moreover, it follows from Lem. D.24 that ψ is also constant, so there is a set S such that ψ ∆S. Now, by induction hypothesis we have Γ ψ = {|ψ|}. Since Γ ∆ Id Set (Lem. D.2), it follows that ψ ∆ {|ψ|}. We then have

x ∈ {|[ev(ψ)]ϕ|} iff ∀y ∈ Γ B (y ∈ {|ψ|} =⇒ ev • x, y ∈ {|ϕ|}) and t ∈ [ev(ψ)]ϕ (n) iff ∀k ≤ n, ∀u ∈ A (u ∈ {|ψ|} =⇒ (t↑k)(u) ∈ ϕ (k)) iff ∀u ∈ A (u ∈ {|ψ|} =⇒ ∀k ≤ n, (t↑k)(u) ∈ ϕ (k)) Given x ∈ Γ B → R + and y ∈ Γ B , for all 0 < k ≤ n we have (ev • x, y ) n (•)↑k = (x n (•)↑k)(y k (•))
Since {|ϕ|} Γ ϕ by induction hypothesis, we are done with

x ∈ {|[ev(ψ)]ϕ|} iff ∀y ∈ Γ B (y ∈ {|ψ|} =⇒ ev • x, y ∈ {|ϕ|}) iff ∀y ∈ Γ B (y ∈ {|ψ|} =⇒ ∀n > 0, (ev • x, y ) n (•) ∈ ϕ (n)) iff ∀y ∈ Γ B (y ∈ {|ψ|} =⇒ ∀n > 0, ∀k ≤ n, ((ev • x, y ) n (•))↑k ∈ ϕ (k)) iff ∀y ∈ Γ B (y ∈ {|ψ|} =⇒ ∀n > 0, ∀k ≤ n, (x n (•)↑k)(y k (•)) ∈ ϕ (k)) iff ∀u ∈ A (u ∈ {|ψ|} =⇒ ∀n > 0, ∀k ≤ n, (x n (•)↑k)(u) ∈ ϕ (k)) iff ∀n > 0, ∀u ∈ A (u ∈ {|ψ|} =⇒ ∀k ≤ n, (x n (•)↑k)(u) ∈ ϕ (k)) iff ∀n > 0, x n (•) ∈ [ev(ψ)]ϕ
Cases of θ t αϕ(α).

Assume α 1 : P + 1 , . It then directly follows that for all x ∈ Γ P + , we have

x ∈ m∈N {|ϕ m |} (Γ (S 1 ), . . . , Γ (S k ), ) iff ∀n > 0, x n (•) ∈ m∈N ϕ m (S 1 , . . . , S k , )(n)
and we conclude by Lem. F.9 and Lem. F. [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF].

Case of µαϕ.

This case cannot occur since µαϕ is not safe.

F.3 The Smooth Fragment

Assume for this §F.3 that the set of propositional variables is partitionned into two infinite sets {α ν , β ν , . Lemma F.11. If ϕ is alternation-free, then ϕ can be formed with the rules of Fig. 5 and Fig. 9, but with the rules (ν-F) and (µ-F) replaced respectively by

Σ ν , α ν : A ϕ : A Σ ν ν α ν ϕ : A Σ µ , α µ : A ϕ : A Σ µ µα µ ϕ : A
where in both cases α θ is guarded in ϕ, and α θ as well as all variables of Σ θ are positive in ϕ.

Proof. By induction on ϕ. The only relevant cases are θαϕ. Since the two cases are similar, we only discuss that of Σ ν αϕ : A. First, since ν αϕ is alternationfree, we can assume that all variables declared in Σ are positive in ϕ. Moreover, since ν αϕ is alternation-free, then so is ϕ. By induction hypothesis Σ can be split into Σ µ , Σ ν and we have Σ µ , Σ ν , α : A ϕ : A Assume toward a contradiction that Σ µ cannot be made empty. This means that there is some variable β µ which does occur in ϕ, and such that β µ must occur in the context of a µ rule for some subformula of ϕ. But then β µ occurs free in ν αϕ under two fixpoints of different kinds, a contradiction. It follows that we can assume Σ µ empty. Similarly, α can be assumed to be gfp variable, since otherwise it would occur free under a lfp in ν αϕ.

Lemma F.12 (Lem. 7.4). Let α 1 : P + 1 , . . . , α k : P + k , α : Q + ϕ : P + be a smooth formula and let v be a valuation taking each propositional variable α i for i = 1, . . . , k to a set v(α i ) ∈ P(Γ P + i ). Consider the function {|ϕ|} : P(Γ Q + ) -→ P(Γ P + ), S -→ {|ϕ|} v[S/α] Then, if α is positive in ϕ (i.e. α Pos ϕ):

• if α is a gfp variable, then {|ϕ|} is Scott-cocontinuous,

• if α is a lfp variable, then {|ϕ|} is Scott-continuous, if α is negative in ϕ (i.e. α Neg ϕ), then {|ϕ|} is antimonotone and

• takes meets of codirected sets to joins of directed sets if α is a gfp variable,

• takes joins of directed sets to meets of codirected sets if α is a lfp variable.

Proof. The proof is by induction on formation of formulae α 1 : P + 1 , . . . , α k : P + k , α : Q + ϕ : P + . Monotonicity and antimonotonicity follow from Lem. F.4. Note that since formulae of the form [box]ϕ are necessarily closed, nothing has to be proved for these. Some cases are already handled by Lem. D.22 (Lem. F.9), and we do not repeat them. We omit the valuation v when possible.

Cases of α, , ⊥.

Trivial. Case of ϕ ∧ ψ (monotone).

Preservation of codirected meets is trivial (see Lem. Since A is finite, we can then reason similarly as in the cases of conjunction (∧) above. Cases of θ t βϕ.

We have α 1 : P + 1 , . . . , α k : P + k , α : Q + , β : P + ϕ : P + with β Pos ϕ. Let v be a valuation. Since for S ⊆ Γ Q + and m ∈ N we have {|θ m+1 βϕ|} v (S) = {|ϕ[θ m βϕ/β]|} v (S) it follows from Lem. D.22 (Lem. F.9), that the function {|θ t βϕ|} v is monotone (resp. antimonotone) if α Pos ϕ (resp. α Neg ϕ). We can then reason as in Lem. D.22 (Lem. F.9). Case of ν βϕ.

We have α 1 : P + 1 , . . . , α k : P + k , α : Q + , β : P + ϕ : P + where the involved variables are gfp variables and are positive in ϕ. The result is then proved exactly the same way as in Lem. D.22 (Lem. F.9).

Case of µβϕ.

The result is proved the same way as in Lem. F.9 (replacing codirected meets by directed joins and Scott cocontinuity by Scott continuity). Proof. By induction on the definition of .

x = next•y for some y ∈ Γ A . But then y n-1 A by induction hypothesis, so that x n A. Case of Fix(X).A.

Let x ∈ Γ Fix(X).A . It follows by induction on A from the induction hypothesis on n and the guardedness of X in A that unfold•x n A[Fix(X).A/X], and we are done. Case of T .

Let x ∈ Γ T . Given n > 0, we have x n (•) ∈ Γ T , so that x n (•) m T for all m > 0 by induction hypothesis. But this implies x n T .

Lemma F.15 (Correctness of Subtyping (Lem. D.28)). Given types T, U without free iteration variable, if x n U and U ≤ T then x n T .

Proof. By induction on U ≤ T .

Cases of

T ≤ T T ≤ U U ≤ V T ≤ V Trivial.

Cases of

T 0 ≤ U 0 T 1 ≤ U 1 T 0 × T 1 ≤ U 0 × U 1 T 0 ≤ U 0 T 1 ≤ U 1 T 0 + T 1 ≤ U 0 + U 1 U 0 ≤ T 0 T 1 ≤ U 1 T 0 → T 1 ≤ U 0 → U 1 T ≤ U T ≤ U

  map : ({B | ψ} → {A | ϕ}) -→ {Str B | 23[hd]ψ} -→ {Str A | 23[hd]ϕ} map : ({B | ψ} → {A | ϕ}) -→ {Str B | 32[hd]ψ} -→ {Str A | 32[hd]ϕ} ( ) These types mean that given f : B → A s.t. f (b) satisfies ϕ if b satisfies ψ, the function (map f ) takes a stream with infinitely many (resp. ultimately all)

  Cons g : {A | ϕ} -→ Str g A -→ {Str g A | 3[hd]ϕ} Cons g : A -→ {Str g A | 3[hd]ϕ} -→ {Str g A | 3[hd]ϕ} 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 Cons g , we could type the stream with constant value a, defined as fix(s).a :: g s, with the type {Str g B | 3[hd][b]}

Fig. 2 .

 2 Fig. 2. Internal and External Semantics

Fig. 3 .

 3 Fig. 3. Syntax and Operational Semantics of the Pure Calculus.

Example 3. 1 .

 1 We can code a finite base type B = {b 1 , . . . , b n } as a sum of unit types n i=1 1 = 1 + (• • • + 1), where the ith component of the sum is intended to represent the element b i of B. At the term level, the elements of B are represented as compositions of injections in j1 (in j2 (. . . in ji )). For instance, Booleans are represented by Bool := 1 + 1, with tt := in 0 ( ) and ff := in 1 ( ).

Fig. 4 .

 4 Fig. 4. Typing Rules of the Pure Calculus (excerpt).

Example 4. 1 .

 1 Given a finite base type B = {b 1 , . . . , b n } as in Ex. 3.1, with element b i represented by in j1 (in j2 (. . . in ji )), the formula [in j1 ][in j2 ] . . . [in ji ] represents the singleton subset {b k } of B. On Bool, we have the formulae [tt] := [in 0 ] and [ff] := [in 1 ] representing resp. tt and ff.

(

Fig. 5 .

 5 Fig. 5. Formation Rules of Formulae (where A, B are pure types).

Fig. 7 .

 7 Fig. 7. Subtyping Rules (excerpt).

Fig. 8 .

 8 Fig. 8. Typing Rules for Refined Modal Types.

Fig. 10 .

 10 Fig.[START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]. Extended Modal Axioms and Rules (with A a pure type and θ either µ or ν ).

Definition 6 . 2 (

 62 Full Modal Theories). The full intuitionistic and classical modal theories (still denoted A and A c ) 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 3ϕ := µα. ϕ ∨ α and ϕ U ψ := µα. ψ ∨ (ϕ ∧ α).

Fig. 11 .

 11 Fig. 11. Extended (Sub)Typing Rules for Refinement Types (where k is not free in E in (∀-I) & (∀-CI), is fresh in (ν-I) & (µ-E), θαψ and γ are smooth, and β Pos γ).

Fig. 12 .

 12 Fig. 12. External Semantics (for closed formulae).

Fig. 14 .

 14 Fig. 14. Typing Rules of the Pure Calculus (full version).

Fig. 15 .

 15 Fig.[START_REF] Bizjak | Denotational semantics for guarded dependent type theory[END_REF]. Positive and Negative Occurrences for the Full Logical Language.

Fig. 17 .

 17 Fig.[START_REF] Bradfield | The mu-calculus and Model Checking[END_REF]. Subtyping Rules (full version).

Fig. 19 .

 19 Fig. 19. Internal Semantics.

  Lemma D.10 ([52, Thm. IV.7.2]). Let T be a topos and fix a map k : X → T Y . The functor (∃k) is left adjoint to k * : T /Y → T /X. Moreover, k * has a right adjoint (∀k) and preserves exponentials, and thus preserves subobjects.Lemma D.11.

  Given a locally contractive functor T on S, define [fold] : Sub(T (Fix(T ))) → Sub(Fix(T )) as unfold * , where we have unfold : Fix(T ) → S T (Fix(T )). (d) Given a S-object X, define [next] : Sub(X) → Sub( X) as (-).

  g. [52, Prop. I.[START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF].5]).-Second, it follows from Lem. D.10 that for objects X, Y of S, taking the pullback of the evaluation map ev : X Y × Y → X gives a map of subobjects, as in ev * (A) / / A X Y × Y ev / / X which in particular preserves limits and colimits. -Third, in the internal logic of S, universal quantification over an object Y w.r.t. a predicate A ∈ Sub(X ×Y ) is given (again via Lem. D.10) by the right adjoint ∀ Y := ∀(π) to π * , where π is the projection X × Y → X ([52, §VI.5, p. 300]). Moreover, via the Kripke-Joyal semantics for a presheaf topos ([52, §VI.7, p. 318]), for

  4) This directly follows from Lem. D.10, via Lem. D.15 and the definition of [ev(-)] .

  is the inverse of Γ (next) (Lem. D.2). (d) Given a locally contractive functor T on S, define {|[fold]|} : P(Γ (T (Fix(T )))) → P(Γ Fix(T )) as Γ (unfold) * , where unfold : Fix(T ) → S T (Fix(T )).

( 1 )

 1 The functions {|[π i ]|}, {|[next]|}, {|[fold]|} are maps of Boolean algebras. (2) The function {|[in i ]|} preserves ∨, ⊥ and ∧.

Definition D. 20 (

 20 Scott Cocontinuity). Let L be a complete lattice. A set S ⊆ L is codirected if it is non-empty and for all a, b ∈ S, there is somec ∈ S such that c ≤ a, b. A function f : L → L is Scott cocontinuous if it is monotone and preserves infs of codirected sets (for S ⊆ L codirected, we have f ( S) = f (S)).In other words, a Scott cocontinuous function L → L is a Scott continuous function L op → L op .

  Then A is constant by induction hypothesis and we are done since Fix(X).A A in this case. The case of T is trivial. As for ∀k • T , since |T | is constant, we have |T | ∆S for some set S. By induction hypothesis for each n ∈ N we have T [n/k] ∆S n for some set S n with ∆S n ∈ Sub( |T | ). Note that ∆S n can be seen as a subobject of ∆S. Recall from §D.4 the posetal left adjoint f ! : Sub(∆S) -→ P(S) of the map ∆ : X ∈ P(S) -→ ∆X ∈ Sub(∆S)

x 1 :

 1 T 1 , . . . , x k : T k M : T and global sections u 1 ∈ Γ |T 1 | , . . . , u k ∈ Γ |T k | , we obtain a global sectionM • u 1 , . . . , u k : 1 -→ |T |We introduce some notation to manipulate these global sections. Given a typingcontext E = x 1 : T 1 , . . . , x k : T k we write ρ |= E if ρ takes each x i for i = 1, . . . , k to some ρ(x i ) ∈ Γ |T i | . Given a typing judgment E M : T , we let M ρ := M • ρ(x 1 ), . . . , ρ(x k ) Given ρ |= E and n > 0, write ρ n E if ρ(x i ) n T i for all i = 1, . . . , k. Thm.7.7 is proved under the following form. Theorem D.29 (Adequacy (Thm. 7.7)). Let E, T have free iteration variables among , and let m ∈ N. If E M : T and ρ |= E, then ∀n > 0, ρ n E[ /m] =⇒ M ρ n T [ /m] Corollary D.30. (1) Consider a closed term M : {A | ϕ} with ϕ safe. Then M : 1 → S A ∈ {|ϕ|}. (2) Consider a closed term M : {A | ψ} → {A | ϕ}, with ϕ, ψ safe. Then M induces a function Γ M taking x ∈ {|ψ|} to Γ M = M • x ∈ {|ϕ|}. Corollary D.30 of course extends to any arity. As a consequence of Cor. D.30 and Møgelberg's Theorem 7.1 [55], for a closed term M : { P | [box]ϕ} with P polynomial, the unique global section M n+1 (•) = M n (•) ∈ Γ P satisfies ϕ in the standard sense (i.e. M n+1 (•) = M n (•) ∈ {|ϕ|}). Moreover a function, say M : { Q | [box]ψ} → { P | [box]ϕ} with Q, P polynomial induces a Setfunction Γ

box ι map g 2 β

 2 f (unbox s) : Str A [box]2 3[hd]ϕ assuming f : {B | ψ} → {A | ϕ} and s : Str B [box]2 3[hd]ψ . Then, since 3[hd]ϕ, 3[hd]ψ are smooth, we can unfold the 3's using the rules (µ-E) and (µ-I) with the non-trivial smooth context γ(β) := Since the formulae 2 3 k [hd]ψ and 2 3 k [hd]ϕ are safe, we can reduce to showing λs. (f (hd g s)) :: g (g (tl g s)) : ∀ • ∀k • U ( , k) U ( , k) := Str g B 2 3 k [hd]ψ -→ Str g A 2 3 k [hd]ϕ assuming f : {B | ψ} → {A | ϕ} and g : ∀ • ∀k • U ( , k).

  λs.box ι map g f (unbox s) Proof. Since 3[hd]ϕ and 3[hd]ψ are both smooth, we can first reduce to E f , s : Str B [box]3 k [hd]ψ box ι (map g f (unbox s)) : Str A [box]3 k [hd]ϕ where E f := f : {B | ψ} → {A | ϕ} Since the formulae 3 k [hd]ψ and 3 k [hd]ϕ are safe, we are done if we show

Example E. 9 .

 9 (23[hd]ϕ) We have the following, for safe and smooth ϕ and ψ:map : ({B | ψ} → {A | ϕ}) -→ {Str B | [box]23[hd]ψ} -→ {Str A | [box]23[hd]ϕ} := λf.λs.box ι map g f (unbox s)Note E.[START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]. We let3 t ϕ := µ t α.ϕ ∨ α 2 t ϕ := ν t α.ϕ ∧ α Proof.We start in the same spirit as in §E.3 and §E.3. Using that 23[hd]ϕ and 23[hd]ψ are both smooth, we first unfold the 2 using the rules (ν-I) and (ν-E). Then, since 3[hd]ϕ and 3[hd]ψ are both smooth, we can unfold the 3 using the rules (µ-E) and (µ-I) with the non-trivial smooth context γ(β) := 2 β

  [hd]ψ and 3 k+1 [hd]ψ ⇔ ([hd]ψ ∨ 3 k [hd]ψ) we do a case analysis on the refinement type of s. (SubSub)Case of [hd]ψ. Since (by §E.1) E, s : {Str g B | [hd]ψ} hd g s : {Str g B | [hd]ψ} we easily deduce that E, s : {Str g B | [hd]ψ} N : {Str g A | [hd]ϕ} and we are done since [hd]ϕ ⇒ 3 k+1 [hd]ϕ. (SubSub)Case of 3 k [hd]ψ.

  ϕ} Using the (Inj 1 -E) rule we are left with showing Cons g x (g xs (next t)) : CoList g A 3 k+1 [hd]ϕ where x := π 0 (y) : {A | ϕ} xs := π 1 (y) : CoList g A assuming y : {A × CoList g A | [π 0 ]ϕ} We have Cons g x (g xs (next t)) : {CoList g A | [hd]ϕ} and we are done since [hd]ϕ ⇒ 3 k+1 [hd]ϕ (Sub)Case of 3 k [hd]ϕ.

  Fix a constant type O and a finite base type I. Let Res A := Res g A Res g A := Fix(X).A + (O × X) I and Ret g := λa. fold(in 0 a) : A -→ Res g A Cont g := λk. fold(in 1 k) : (O × Res g A) I -→ Res g A Example E.40 (A Scheduler on Resumptions). sched : Res A -→ Res A -→ Res A := λp.λq. box ι (sched g (unbox p) (unbox q))

  [Ret]. We have unfold p : {A + (O × Res g A) I | [in 0 ] } We apply the (Inj 0 -E) rule on p and we are done since Ret g a : {Res g A | [Ret]} assuming a : A Case of [now]ψ. We have unfold p : {A + (O × Res g A) I | [in 0 ]ψ} We apply the (Inj 0 -E) rule on p and we are done since Ret g a : {Res g A | [now]ψ} assuming a : {A | ψ} Case of ∃3 k ϕ.

  ]ϑ we reason by cases on the refinement type of p. (Sub)Cases of [out]ϑ. We show N (g, k, q) : {Res g A | [out]ϑ} We handle the cases of [∨out] and [∧out] separately. (SubSub)Case of [∨out].We apply the (∨-E) rule on the refinement type of p. So let i ∈ I and assume p :{Res g A | [out i ]ϑ}This amounts tok : {(O × Res g A) I | [i] → [π 0 ]ϑ} Hence assuming i : {A | [i]}we haveπ 0 (ki) , g (next q) (π 1 (ki)) : {O × Res g A | [π 0 ]ϑ} It follows that λi. π 0 (ki) , g (next q) (π 1 (ki)) : {(O × Res g A) I | [i] → [π 0 ]ϑ}and we are done sinceCont g = λh. fold(in 1 h) (SubSub)Case of [∧out].For each i ∈ I we have to showN (g, k, q) : {Res g A | [out i ]ϑ} So let i ∈ I. Since p : {Res g A | [out i ]ϑ} we have k : {(O × Res g A) I | [i] → [π 0 ]ϑ} and we conclude similarly as in the case of [∨out]. (Sub)Case of ∃3 0 [out]ϑ.

  bft g : Tree A -→ {CoList g A | [inf]} bftaux g : {CoList g (Tree A) | [¬nil]} -→ {CoList g A | [inf]} Example E.50. Assuming ϕ : A, bft g : {Tree g A | ∀2[lbl]ϕ} -→ {CoList g A | 2[hd]ϕ} Proof. Thanks to Ex. E.30 and Ex. E.31, we can reduce to showing bftaux g : CoList g (Tree g A) [¬nil] ∧ 2 fin [hd]∀2[lbl]ϕ -→ {CoList g A | 2[hd]ϕ} Let T := CoList g (Tree g A) [¬nil] ∧ 2 fin [hd]∀2[lbl]ϕ -→ {CoList g A | 2[hd]ϕ} and assume g : T s : CoList g (Tree g A) [¬nil] ∧ 2 fin [hd]∀2[lbl]ϕ

  show by induction on m ∈ N that {|µ m αϕ(α)|} ⊆ {|µαϕ(α)|} and {|ν αϕ(α)|} ⊆ {|ν m αϕ(α)|} The base case m = 0 is trivial since {|µ 0 αϕ(α)|} = {|⊥|} and {|ν 0 αϕ(α)|} = {| |} For the induction step we have {|µ m+1 αϕ(α)|} = {|ϕ(µ m αϕ(α))|} and {|ν m+1 αϕ(α)|} = {|ϕ(ν m αϕ(α)|} So the induction hypothesis together with Lem. F.4 gives {|µ m+1 αϕ(α)|} ⊆ {|ϕ(µαϕ(α))|} and {|ϕ(ν αϕ(α))|} ⊆ {|ϕ(ν m αϕ(α))|} and we are done since by the Knaster-Tarski Theorem, we have {|ϕ(µαϕ(α))|} = {|µαϕ(α)|} and {|ϕ(ν αϕ(α))|} = {|ν αϕ(α)|} It remains to show the converse direction {|ϕ ∨ ψ|} (D 1 , .

2 ,

 2 we have x = in j • y for some unique j ∈ {0, 1} and y ∈ Γ Q + j . Then we are done since by induction hypothesis we have x ∈ {|[in i ]ϕ|} ( D 1 , . . . , D k ) iff j = i and y ∈ {|ϕ|} ( D 1 , . . . , D k ) iff j = i and y ∈ {|ϕ|} (D 1 , . . . , D k ) iff j = i and ∀S 1 ∈ D 1 , . . . , S k ∈ D k , y ∈ {|ϕ|} (D 1 , . . . , D k

D. 22 (

 22 Lem. F.9)). As for the preservation of directed joins, let D ⊆ P(Γ Q + ) be directed. Then by induction hypothesis we have{|ϕ ∧ ψ|} ( D) = {|ϕ|} (D) ∩ {|ψ|} (D) ⊇ {|ϕ ∧ ψ|} (D)For the converse inclusion, consider some x both in {|ϕ|} (D) and {|ψ|} (D).Hence there are S, S ∈ D such that x ∈ {|ϕ|} (S) and x ∈ {|ψ|} (S ). Now since D is directed and by monotonicity, there is some S ∈ D such that x ∈ {|ϕ|} (S ) ∩ {|ψ|} (S ). Case of ϕ ∧ ψ (antimonotone).That {|ϕ ∧ ψ|} turns directed joins into codirected meets is trivial (as codirected meets commute over binary meets) and omitted. Let us show that {|ϕ ∧ ψ|} turns codirected meets into directed joins. So let D ⊆ P(Γ Q + ) be codirected. Then by induction hypothesis we have{|ϕ ∧ ψ|} ( D) = {|ϕ|} (D) ∩ {|ψ|} (D) ⊇ {|ϕ ∧ ψ|} (D)We then conclude as for preservation of directed joins in the monotone case. Given x both in {|ϕ|} (D) and {|ψ|} (D), there are S, S ∈ D such that x ∈ {|ϕ|} (S) and x ∈ {|ψ|} (S ). Now since D is codirected there is some S ∈ D such that S ⊆ S ∩ S , and by antimonotonicity we have x ∈ {|ϕ|} (S ) ∩ {|ψ|} (S ).Case of ϕ ∨ ψ (monotone).Preservation of codirected meets is handled in Lem. D.22 (Lem. F.9) while preservation of directed join is trivial.Case of ϕ ∨ ψ (antimonotone).That {|ϕ ∨ ψ|} turns codirected meets into directed joins is trivial (as directed joins commute over binary joins) and omitted. Let us show that {|ϕ ∨ ψ|} turns directed joins into codirected meets. So let D ⊆ P(Γ Q + ) be directed.By induction hypothesis we have{|ϕ ∨ ψ|} ( D) = {|ϕ|} (D) ∪ {|ψ|} (D) ⊆ {|ϕ ∨ ψ|} (D)We can then conclude similarly as in Lem. D.22 (Lem. F.9). Let x ∈ {|ϕ ∨ ψ|} (D) and assume toward a contradiction that there are S, S ∈ D such that x / ∈ {|ϕ|} (S) and x / ∈ {|ψ|} (S ). Then since D is directed, there is some S ∈ D such that S ∪ S ⊆ S , and by antimonotonicity we get x / ∈ {|ϕ ∨ ψ|} (S ), a contradiction.Case of ψ ⇒ ϕ.With the classical semantics, the interpretation of ⇒ can be decomposed into ∨ and ¬, where {|¬ϕ|} is the complement of {|ϕ|} (at the appropriate type). Let α be positive in ϕ and negative in ψ, with α : Q + ϕ, ψ : P + , and let furthermore by D and D (of the appropriate type) be resp. directed and codirected. We then trivially have {|¬ϕ|} ( D) = P(Γ P + ) \ {|ϕ|} ( D) = P(Γ P + ) \ {|ϕ|} (D) = (P(Γ P + ) \ {|ϕ|} (D)) {|¬ϕ|} ( D ) = P(Γ P + ) \ {|ϕ|} ( D ) = P(Γ P + ) \ {|ϕ|} (D ) = (P(Γ P + ) \ {|ϕ|} (D )) {|¬ψ|} ( D) = P(Γ P + ) \ {|ψ|} ( D) = P(Γ P + ) \ {|ψ|} (D) = (P(Γ P + ) \ {|ψ|} (D)) {|¬ψ|} ( D ) = P(Γ P + ) \ {|ψ|} ( D ) = P(Γ P + ) \ {|ψ|} (D ) = (P(Γ P + ) \ {|ψ|} (D ))Cases of [π i ]ϕ, [in i ]ϕ, [next]ϕ and [fold]ϕ. These modalities are handled similarly as in Lem. D.22 (Lem. F.9). Case of [ev(ψ)]ϕ. Since [ev(ψ)]ϕ is smooth, the formula ψ is closed and we have Q + = B → R + with B a finite base type. Since B is constant, by Lem. D.4 there is a finite set A such that B ∆A, so that Γ B A by Lem. D.2. Now, given x ∈ Γ P + and S ⊆ Γ Q + we have x ∈ {|[ev(ψ)]ϕ|} (S) iff ∀y ∈ A (y ∈ {|ψ|} =⇒ ev • x, y ∈ {|ϕ|} (S))

F. 4

 4 RealizabilityLemma F.13 (Monotonicity of Realizability (Lem. D.25)). Let T be a type without free iteration variables. If x n T then x k T for all k ≤ n.

  Let x : 1 → S ∆Γ U such that x n U , so that x n (•) m U for all m > 0. By induction hypothesis we get x n (•) m T for all m > 0 and we are done.Case ofT ≤ |T | By Lem. D.[START_REF] Fujima | Practical Alternating Parity Tree Automata Model Checking of Higher-Order Recursion Schemes[END_REF].Case ofA ≤ {A | } Trivial Case of A ϕ ⇒ ψ {A | ϕ} ≤ {A | ψ}By Lem. F.5 (Lem. D.[START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF].(2)).Let x : 1 → S ∆Γ A . Since ϕ is safe we have {|ϕ|} A = Clos( ϕ A ) by Prop. F.10 (Prop.7.3). Then we are done since:x n {A | ϕ} iff x n (•) m {A | ϕ} for all m > 0 iff (x n (•)) m (•) ∈ ϕ A (m) for all m > 0 iff x n (•) ∈ {|ϕ|} A iff x n (•) ∈ [box]ϕ A (n) iff x n { A | [box]ϕ} Case of A c ϕ ⇒ ψ { A | [box]ϕ} ≤ { A | [box]ψ}By Lem. F.2 (Lem. D.[START_REF] Birkedal | First steps in synthetic guarded domain theory: step-indexing in the topos of trees[END_REF].(1)).

Theorem F. 16 (

 16 Adequacy (Thm. D.29)). Let E, T have free iteration variables among , and let m ∈ N. If E M : T and ρ |= E, then ∀n > 0, ρ n E[ /m] =⇒ M ρ n T [ /m] Proof. The proof is by induction on typing derivations. We implicitly use Lem. D.2 whenever required. We omit iteration variables when possible. Case of E, x : T M : T E fix(x).M : T Let ρ |= E and write y := fix(x).M ρ ∈ Γ T . Note that y = M [next(fix(x).M )/x] ρ = M ρ[next•y/x]We show by induction on n > 0 that ρ n E implies y n T . In the base case n = 1, since next • y 1 T , we have ρ[next • y/x] 1 E, x : T , so that the induction hypothesis on typing derivations gives y = M ρ[next•y/x] 1 T . As for induction step, assume ρ n+1 E. By Monotonicity of Realizability (Lem. F.13), we have ρ n E, and the induction hypothesis on n gives y n T . It follows that next • y n+1 T , so that ρ[next • y/x] n+1 E, x : T and the induction hypothesis on typing derivations gives y= M ρ[next•y/x] n+1 T . Case of E M : T E next(M ) : T Let ρ |= E and write x := next(M ) ρ ∈ Γ T . Let n > 0 such that ρ n T .If n = 1 then we trivially have x 1 T . Assume n > 1. Write y := M ρ , so that x = next • y. By Monotonicity of Realizability (Lem. F.13), we have ρ n-1 E, so that the induction hypothesis on typing derivations gives y n-1 T and we are done.Case ofx 1 : T 1 , . . . , x k : T k M : T E M 1 : T 1 . . . E M k : T k E box [x1 →M1,...,x k →M k ] (M ) : T (T 1 , . . . , T k constant) Let ρ |= E and write x := box σ (M ) ρ where σ = [x 1 → M 1 , . . . , x k → M k ].Let n > 0 such that ρ n E. We show x n T , i.e. that x m (•) m T for all m > 0. Fix m > 0. We have by definitionx m (•) : -→ M M 1 m (ρ m (•)) , . . . , M k m (ρ m (•))For i = 1, . . . , k, since the type T i is constant, we have byLem. D.24 thatM i m (ρ m (•)) = M i (ρ (•)) for all > 0, so thatx m (•) = -→ M M 1 (ρ (•)) , .. . , M k (ρ (•)) Now, by induction hypothesis, since ρ n E by assumption, for each i = 1, . . . , k we have M i ρ n T i and since T i is constant, by Lem. D.24 this implies M i ρ T i for all > 0. By induction hypothesis again, this in turn gives M • M 1 ρ , . . . , M k ρT for each > 0. But then we are done sincex m (•) = -→ M M 1 (ρ (•)) , . . . , M k (ρ (•)) = M • M 1 ρ , . . . , M k ρ Case of E M : T E unbox(M ) : T Let ρ |= E and write x := unbox(M ) ρ . Let n > 0 such that ρ n E. By induction hypothesis we get M ρ n T , that is ( M ρ ) m (•) m T for all m > 0, so in particular ( M ρ ) n (•) n T . But now we are done since x m (•) = ( M ρ ) n (•) m (•) for each m > 0. Case of x 1 : T 1 , . . . , x k : T k M : T E M 1 : T 1 . . . E M k : T k E prev [x1 →M1,...,x k →M k ] (M ) : T (T 1 , . . . , T k constant) Let ρ |= E and write x := box σ (M ) ρ where σ = [x 1 → M 1 , . . . , x k → M k ].Let n > 0 such that ρ n E. We show x n T . If n = 1 then the result trivially holds. Assume n > 1. For each m > 0, we have by definitionx m (•) = M m+1 M 1 m (ρ m (•)) , . . . , M k m (ρ m (•))For i = 1, . . . , k, since the type T i is constant, we have by Lem. D.24 thatM i m (ρ m (•)) = M i m+1 (ρ m+1 (•)), so that x m (•) = M m+1 M 1 m+1 (ρ m+1 (•)) , . . . , M k m+1 (ρ m+1 (•))and it follows thatx = next • M • M 1 ρ , .. . , M k ρ Now, by induction hypothesis, since ρ n E by assumption, for each i = 1, . . . , k we have M i ρ n T i and since T i is constant, by Lem. D.24 this implies M i ρ n-1 T i . By induction hypothesis again, this in turn gives M • M 1 ρ , . . . , M k ρ n-1 T and we are done. Case of E M : T T ≤ U E M : U By Lem. D.28 (Lem. F.15). Case of E M : {A | ψ ⇒ ϕ} E M : {A | ψ} E M : {A | ϕ} Let ρ |= E and write x := M ρ ∈ Γ A . Let n > 0 such that ρ n E. By induction hypothesis, the right premise gives x n (•) ∈ ψ A (n) and the left premise implies x n(•) ∈ ϕ A (n). Case of for i ∈ {0, 1}, E M : {A | ϕ 0 ∨ ϕ 1 } E, x : {A | ϕ i } N : U E N [M/x] : U Let ρ |= Eand write y := M ρ ∈ Γ A and z := N ρ[y/x] ∈ Γ |U | . Let n > 0 and assume ρ n E. By induction hypothesis we have y ∈ ϕ i for some i ∈ {0, 1}. It follows that ρ[y/x] n E, x : {A | ϕ i }, from which we get z n B by induction hypothesis. Case of E M : {A | ⊥} E N : |U | E N : U Let ρ |= E and write x := M ρ ∈ Γ A . Let n > 0 such that ρ n E. By induction hypothesis, the left premise gives x n (•) ∈ ⊥ (n) = ∅, a contradiction. Hence ρ n E, and the result follows.Case ofE M i : {A i | ϕ} E M 1-i : A 1-i E M 0 , M 1 : {A 0 × A 1 | [π i ]ϕ} Let ρ |= E. Write y 0 := M 0 ρ ∈ Γ A 0 , y 1 := M 1 ρ ∈ Γ A 1 , and x := M 0 , M 1 ρ = y 0 , y 1 .Let n > 0 such that ρ n E. By induction hypothesis on typing derivations we have (yi ) n (•) ∈ ϕ . But since π i (x n (•)) = (y i ) n (•), this gives x n (•) ∈ [π i ]ϕ . Case of E M : {A 0 × A 1 | [π i ]ϕ} E π i (M ) : {A i | ϕ} Let ρ |= E. Write y := M ρ ∈ Γ A 0 × A 1 and x := π i (M ) ρ = π i • y. Let n > 0 such that ρ n E.By induction hypothesis on typing derivations we have y n (•) ∈ [π i ]ϕ , so that π i (y n (•)) ∈ ϕ . But then we are done sincex n (•) = π i (y n (•)).Case ofE M : {A i | ϕ} E in i (M ) : {A 0 + A 1 | [in i ]ϕ} Let ρ |= E. Write y := M ρ ∈ Γ A i , and x := in i (M ) ρ = in i •y. Let n > 0 such that ρ n E.Hence by induction hypothesis on typing derivations we havey n (•) ∈ ϕ . But since x n (•) = in i (y n (•)), this implies x n (•) ∈ [in i ]ϕ .Case ofE M : {A 0 + A 1 | [in i ]ϕ} E, x : {A i | ϕ} N i : U E, x : A 1-i N 1-i : U E case M of (x.N 0 |x.N 1 ) : U Let ρ |= E. Write y := M ρ ∈ Γ A 0 + A 1 Γ A 0 + Γ A 1 .Hence y = in j • z for some (unique) j ∈ {0, 1} and z ∈ Γ A j . Let n > 0 such that ρ n E. By induction hypothesis, the left premise givesy n (•) ∈ [in i ]ϕ (n), so that y n (•) = in i (u) for some u ∈ ϕ (n). But this implies j = i and u = z n (•), so that z n {A i | ϕ}. It follows that ρ[z/x] n E, x : {A i | ϕ},and the induction hypothesis on typing derivations gives N i ρ[z/x] n U . But then we are done sincecase M of (x.N 0 |x.N 1 ) ρ = N i ρ[z/x] Case of E, x : {B | ψ} M : {A | ϕ} E λx.M : {B → A | [ev(ψ)]ϕ} Let ρ |= E. Write y := λx.M ρ ∈ Γ B → A . Let n > 0 such that ρ n E. We show y n (•) ∈ [ev(ψ)]ϕ (n). So let k ≤ n and u ∈ Γ B (k) such that u ∈ ψ (k). By[START_REF] Clouston | The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types[END_REF] Cor. 3.8] there is some z ∈ Γ B such that z k (•) = t. By Monotonicity of Realizability (Lem. F.13), we have ρ k E, so that ρ[z/x] k E, x : {B | ψ}. The induction hypothesis on typing derivations thus gives ( M ρ[z/x] ) k (•) ∈ ϕ , and we are done since (yk (•))(z k (•)) = ( M ρ[z/x] ) k (•). Case of E M : {B → A | [ev(ψ)]ϕ} E N : {B | ψ} E M N : {A | ϕ} Let ρ |= E. Write y := M ρ ∈ Γ B → A , z := N ρ ∈ Γ B and x := M N ρ = ev • y, z . Let n > 0 such that ρ n E.By induction on typing derivations, the right premise gives z n (•) ∈ ψ (n), so that the left premise gives (y n (•))(z n (•)) ∈ ϕ (n). But then we are done sincex n (•) = (y n (•))(z n (•)). Case of E M : {A[Fix(X).A/X] | ϕ} E fold(M ) : {Fix(X).A | [fold]ϕ} Let ρ |= E. Write y := M ρ ∈ Γ A[Fix(X).A/X] and x := fold(M ) ρ = fold • y. Let n > 0 such that ρ n E. By induction hypothesis on typing derivations we have y n (•) ∈ ϕ . But then we are done since unfold n (x n (•)) = y n (•). Case of E M : {Fix(X).A | [fold]ϕ} E unfold(M ) : {A[Fix(X).A/X] | ϕ} Let ρ |= E. Write y := M ρ ∈ Γ Fix(X).A and x := unfold(M ) ρ = unfold • y. Let n > 0 such that ρ n E. By induction hypothesis on typing derivations we have y n (•) ∈ [fold]ϕ . Hence unfold n (y n (•)) ∈ ϕ and we are done since x n (•) = unfold n (y n (•)).Cases ofE M : T [0/ ] E M : T [ +1/ ] E M : ∀ • T ( not free in E) E M : T E M : ∀ • T ( not free in E) Let ρ |= Eand write x := M ρ ∈ Γ |T | . Let n > 0 and assume ρ n E. Let m ∈ N. We have to show M n T [m/ ]. Since does not occur free in E, we have ρ n E[m / ] for all m ∈ N. For both rules we can conclude from the induction hypothesis. Case of E M : ∀ • T E M : T [t/ ] Let ρ |= E and write x := M ρ ∈ Γ |T | . Let n > 0 and assume ρ n E. By induction hypothesis we have x n T [m/ ] for m = t and the result follows. Cases of E M : A [box]γ[ν αϕ/β] β Pos γ E M : { A | [box]γ[ν αϕ/β]} E M : { A | [box]γ[µαϕ/β]} E, x : A [box]γ[µ αϕ/β] N : U β Pos γ E N [M/x] : U where is not free in E, U, γ, and γ, ϕ are smooth. First, since ϕ is smooth by Lem. 7.4 we have {|ν αϕ(α)|} = m∈N {|ϕ m ( )|} and {|µαϕ(α)|} = m∈N {|ϕ m ( )|} Moreover, since β is positive in γ and γ is smooth, it follows from Lem. F.12 (Lem. 7.4) that {|γ|} is continuous and cocontinuous in β. We thus get {|γ[ν αϕ(α)/β]|} = m∈N {|γ[ϕ m ( )/β]|} and {|γ[µαϕ(α)/β]|} = m∈N {|γ[ϕ m ( )/β]|} and the result follows.

  . . , x k in M . We use the following conventions of [20]: box(M ) and prev(M ) (without indicated substitution) stand resp. for box [] (M ) and prev [] (M ) i.e. bind no variable of M . Moreover, box ι (M ) stands for box [x1 →x1,...,x k →x k

Table 2 .

 2 Modal Axioms and Rules. Types are omitted in and (C) marks axioms assumed for c but not for . Properties of the non-atomic [hd] and are derived.

  The formula [¬nil] = [fold][in 1 ] is safe. Moreover: Definition 6.7 (Smooth Formula). A formula α 1 : A 1 , . . . , α n : A n ϕ : A is smooth if (i) the types A 1 , . . . , A n , A are finitary strictly positive, and (ii) for each occurrence in ϕ of a modality [ev(ψ)], the formula ψ is closed, and (iii) ϕ is alternation-free: for θ, θ ∈ {µ, ν}, (1) if θβ 0 ψ 0 is a subformula of ϕ, and θ β 1 ψ 1 is a subformula of ψ 0 s.t. β 0 occurs free in ψ 1 , then θ = θ , (2) if some α i occurs in two subformulae θβ 0 ψ 0 and θ β 1 ψ 1 of ϕ, then θ = θ , and (3) if some α i occurs in a subformula θ βψ of ϕ, then α i Pos ψ.

	Our notion of alternation freedom is adapted from [17], in which propositional
	(fixpoint) variables are always positive. Note that the smooth restriction imposes
	no further conditions on approximated fixpoints θ t α. In the smooth fragment,
	greatest and least fixpoints can be thought about resp. as
		ϕ m ( )	and	ϕ m (⊥)
		m∈N	m∈N
	Iteration terms allow for formal reasoning about such unfoldings. Assuming t =
	m ∈ N, the formula ν t αϕ(α) (resp. µ t αϕ(α)) can be read as ϕ m ( ) (resp.
	ϕ m (⊥)). This gives the rules (ν-I) and (µ-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. [17, §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 µ-calculus.
	In particular, the alternation-free fragment contains all the flat fixpoints of [63]
	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. [17, §2.2]).
	Example 6.9. Any formula without fixpoint nor [ev(-)] is smooth. It ϕ is smooth,
	then so are [hd]ϕ, [lbl]ϕ and ϕ for	∈ {2, ∀2, ∃2, 3, ∃3, ∀3}.
	Example 6.6. Any formula without fixpoint nor [ev(-)] is equivalent in c to a
	safe one. It ϕ is safe, then so are [hd]ϕ, [lbl]ϕ, as well as ϕ (for ∈ {2, ∀2, ∃2})
	and [box] ϕ (for	∈ {3, ∃3, ∀3}).

  t. the full modal theories of Def. 6.2. Lemma 7.2. If A c ϕ then {|ϕ|} = {| |}. If A ϕ then ϕ = .

	The Safe Fragment. For α (positive and) guarded in ϕ, the internal semantics
	of θαϕ is somewhat meaningless because S has unique guarded fixpoints [13,
	§2.5]. In particular, the typing fix(s).Cons g a s : {Str g A | 3[ϕ]} for arbitrary
	a : A and ϕ : Str g A (extending §2) is indeed verified by the S semantics -.
	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 ϕ : A is safe then {|ϕ|} = Γ ϕ .
	Proposition 7.3 gives the subtyping rule { A | [box]ϕ} ≡ {A | ϕ} (Fig.

  [START_REF] Birkedal | Guarded cubical type theory[END_REF]. |} = m∈N {|ϕ m ( )|} (resp. {|µαϕ(α)|} = m∈N {|ϕ m (⊥)|}). Given a type T without free iteration variable, a global section x ∈ Γ |T | and n > 0, we define the realizability relation x n T by induction on lexicographicaly ordered pairs (n, T ) in Fig.13.Lemma 7.[START_REF] Bahr | The Clocks Are Ticking: No More Delays![END_REF]. Given types T, U without free iteration variable, if x n U and U ≤ T then x n T .

	Lemma 7.4. Given a closed smooth ν αϕ(α) : A (resp. µαϕ(α) : A), the func-
	tion {|ϕ|} : P(Γ A ) → P(Γ A ) is Scott-cocontinuous (resp. Scott-continuous).
	We have {|ν αϕ(α)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). Theorem 7.7 (Adequacy). If M : T , where T has no free iteration variable,
	then M	n T for all n > 0.
	By Thm. 7.7, a program M : B → A induces a set-theoretic function Γ M :
	Γ B → Γ A , x → M •x. When B and A are polynomial (e.g. streams Str g B,
	Str g A with B, A constant), Møgelberg's Thm. 7.1 says that Γ 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 : {Str B | [box]ψ} → {Str A | [box]ϕ}, then (modulo
	Γ ∆	Id Set ) given a stream x that satisfies ψ (i.e. x ∈ {|ψ|}) the stream
	Γ M (x) satisfies ϕ (i.e. Γ M (x) ∈ {|ϕ|}). See §8 for examples.

  Case of [next]ϕ. This case cannot occur since A is constant. Case of [fold]ϕ. In this case, we have A = Fix(X).B. Since X is guarded in B, it must not occur in B, and we have A B via unfold. Moreover B is constant, with say B ∆S and by induction hypothesis, [ϕ] is a constant subobject of B , say [ϕ] ∆Φ. Now, [fold]ϕ lies in the pullback diagram

  8 and the fact that ∆ thus preserves universal quantifications (see e.g. [52, Thm. X.3.1 & Lem. X.3.2]). Cases of θ t αϕ and θαϕ.

  .1 thus says that S is closed if and only if S is closed for the corresponding usual tree (or stream) topology. Since Prop.[START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].3 can be formulated as {|ϕ|} = Clos( ϕ ) it indeed says that {|ϕ|} is closed for the usual topology.We finally briefly elaborate on this in view of the coincidence of the S and Set semantics for safe formulae (Prop. 7.3). Let us consider the cases of 2[hd]ϕ and 3[hd]ϕ on guarded streams Str g B. Assume that ϕ is safe. The equality {|2[hd]ϕ|} = Γ 2[hd]ϕ implies that the usual Set semantics of 2[hd]ϕ is in the image of Γ . But a subset of Γ Str g B which is in the image of Γ is necessarily a closed set w.r.t. the usual product topology on streams in Set, i.e. a safety property. Formulae of the form 2[hd]ϕ define safety properties on streams, but liveness properties of the form 3[hd]ϕ are not closed (for non-trivial ϕ), and thus cannot be in the image of Γ .

  Operations on Coinductive StreamsExample E.6 (Operations on Coinductive Streams). For a safe ϕ of the appropriate type, we have

	Proof.
	Case of hd.
	Recall that
	hd : Str A -→ A
	:= λs.hd g (unbox s)
	We have

hd : {Str A | [box]2[hd]ϕ} -→ {A | ϕ} tl : {Str A | [box]2[hd]ϕ} -→ {Str A | [box]2[hd]ϕ} tl : {Str A | [box] ϕ} -→ {Str A | [box]ϕ} s : {Str A | [box]2[hd]ϕ} s : {Str A | [box]2[hd]ϕ} 2[hd]ϕ safe s : {Str A | [box]2[hd]ϕ} s : {Str g A | 2[hd]ϕ} s : {Str A | [box]2[hd]ϕ} unbox s : {Str g A | 2[hd]ϕ} s : {Str A | [box]2[hd]ϕ} hd g (unbox s) : {A | ϕ} λs.hd g (unbox s) : {Str A | [box]2[hd]ϕ} -→ {A | ϕ}

Cases of tl. Recall that tl : Str A -→ Str A := λs.box ι (prev ι (tl g (unbox s))) We have s : {Str A | [box]2[hd]ϕ} s : {Str A | [box]2[hd]ϕ} s : {Str A | [box]2[hd]ϕ} unbox s : {Str g A | 2[hd]ϕ} s : {Str A | [box]2[hd]ϕ} tl g (unbox s) : {Str g A | 2[hd]ϕ} Str A constant s : {Str A | [box]2[hd]ϕ} prev ι (tl g (unbox s)) : {Str g A | 2[hd]ϕ} s : {Str A | [box]2[hd]ϕ} box ι (prev ι (tl g (unbox s))) : {Str g A | 2[hd]ϕ} 2[hd]ϕ safe s : {Str A | [box]2[hd]ϕ} box ι (prevι(tl g (unbox s))) : {Str A | [box]2[hd]ϕ} λs.box ι (prev ι (tl g

  .8 ( §E.3), is more involved. Since 32[hd]ϕ, 32[hd]ψ are smooth and 3 k 2[hd]ϕ, 3 k 2[hd]ψ are safe, we similarly reduce to showing (map g f ) : ∀k • T (k) where

  Case of Eventually Always (32[hd]ϕ)Example E.[START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF]. We have the following, for safe and smooth ϕ and ψ: Since 32[hd]ϕ and 32[hd]ψ are both smooth, we can first reduce toE f , s : Str B [box]3 k 2[hd]ψ box ι (map g f (unbox s)) : Str A [box]3 k 2[hd]ϕwhereE f := f : {B | ψ} → {A | ϕ}Since the formulae 3 k 2[hd]ψ and 3 k 2[hd]ϕ are safe, we are done if we show

map : ({B | ψ} → {A | ϕ}) -→ {Str B | [box]32[hd]ψ} -→ {Str A | [box]32[hd]ϕ} = λf.λs.box ι map g f (unbox s)

Proof.

  . Let ϑ : O be a safe and smooth formula. Furthermore, let 2 ∈ {∀2, ∃2}, 3 ∈ {∀3, ∃3} and [out] ∈ {[∧out], [∨out]}. We have sched : {Res A | [box]23[out]ϑ} -→ {Res A | [box]23[out]ϑ} -→ {Res A | [box]23[out]ϑ}

  . Tree g A → CoList g A := λt.bftaux g [t] g bftaux g : CoList g (Tree g A) → CoList g A := fix(g).λs. case s of | Nil g → Nil g | Cons g x xs → (label g x) :: g g next(append g ) xs [(son g x), (son g r x)] g , y 1 , . . . , y n ] g := next(Cons g ) y 0 next[y 1 , . . . , y n ] g

	bft	: Tree A → CoList A
		:= λt. box ι (bft g (unbox t))
	bft g : where	[] g	:= next([] g )
	[y 0 Example E.48.
			bft g

  we are left with showing v ::g g next(append g ) xs [ , r] g : {CoList g A | 2[hd]ϕ}wherexs := π 1 y : CoList g (Tree g A) 2 fin [hd]∀2[lbl]ϕ v := label g (π 0 y) : {A | ϕ} := son g (π 0 y) : {Tree g A | ∀2[lbl]ϕ} r := son g r (π 0 y) : {Tree g A | ∀2[lbl]ϕ} assuming y : Tree g A × CoList g (Tree g A) [π 0 ]ϕ ∧ [π 1 ][next]2 fin [hd]∀2[lbl]ϕ

	It follows from Ex. E.30 and Ex. E.31 that
	[ , r] g :	CoList g (Tree A) [¬nil] ∧ 2 fin [hd]∀2[lbl]ϕ
	Hence, by Ex. E.33 and Ex. E.34 we obtain
	next(append

g ) xs [ , r] g : CoList g (Tree A) [¬nil] ∧ 2 fin [hd]∀2[lbl]ϕ and the result follows.

Martin Hofmann's Algorithm

We follow the presentation of

[START_REF] Berger | Martin Hofmann's Case for Non-Strictly Positive Data Types[END_REF]

with some slight changes in terminology and notation. Consider the non-strictly positive type Rou g

  We have to show ev• x, y ∈ {|ϕ|}. But if y ∈ {|ψ 0 |} then we are done since x ∈ {|[ev(ψ 0 )]ϕ|}, and similarly if y ∈ {|ψ 1 |}.

	Case of

  . . , D k ) ⊆ {|ϕ|} (D 1 , . . . , D k ) ∪ {|ψ|} (D 1 , . . . , D k ) So let x ∈ Γ P + such that x ∈ {|ϕ ∨ ψ|} (S 1 , . . . , S k ) for every S 1 ∈ D 1 , . . . , S k ∈ D k . Assume toward a contradiction that there are S 1 ∈ D 1 , . . . , S k ∈ D k such that x / ∈ {|ϕ|} (S 1 , . . . , S k ) and that there are S 1 ∈ D 1 , . . . , S k ∈ D k such that x / ∈ {|ψ|} (S 1 , . . . , S k ). Since the D i 's are codirected for inclusion, there are S 1 ∈ D 1 , . . . , S k ∈ D k such that S i ⊆ S i ∩ S i for i = 1, . . . , k. By monotonicity w.r.t. inclusion, we have x / ∈ {|ϕ|} (S 1 , . . . , S k ) and x / ∈ {|ψ|} (S 1 , . . . , S k ). But this implies x / ∈ {|ϕ ∨ ψ|} (S 1 , . . . , S k ), a contradiction. Case of [π i ]ϕ. Let D 1 ⊆ P(Γ P + 1 ), . . . , D k ⊆ P(Γ P + k ) be codirected. Let x ∈ Γ P + and write P

  , . . . , S k )) n+1 ( ) := {|ϕ|} S 1 , . . . , S k , ({|ϕ|} (S 1 , . . . , S k )) n ( ) It remains to show the converse directionϕ ∨ ψ (D 1 , . . . , D k ) ⊆ ϕ (D 1 , . . . , D k ) ∨ ψ (D 1 , . . . , D k )Since meets and joins are computed pointwise in subobject lattices, we are done if for each n > 0 we showϕ∨ψ (D 1 , . . . , D k )(n) ⊆ ϕ (D 1 , . . . , D k )(n) ∪ ψ (D 1 , . . . , D k )(n)We can then conclude as in the case of {|-|}. Fix n > 0 and lett ∈ P + such that t ∈ ϕ ∨ ψ (A 1 , . . . , A k )(n) for every A 1 ∈ D 1 , . . . , A k ∈ D k .Assume toward a contradiction that there areA 1 ∈ D 1 , . . . , A k ∈ D k such that t / ∈ ϕ (A 1 , . . . , A k )(n) and that there are A 1 ∈ D 1 , . . . , A k ∈ D k such that t / ∈ ψ (A 1 , . . . , A k )(n).Since the D i 's are codirected for inclusion, there areA 1 ∈ D 1 , . . . , A k ∈ D k such that A i ≤ A i ∧ A 1 for i = 1, .. . , k. By monotonicity w.r.t. subobject lattice orders, we have t / ∈ ϕ (A 1 , . . . , A k )(n) and t / ∈ ψ (A 1 , . . . , A k

	An easy induction on m ∈ N then shows that each function
	({|ϕ|} (-, . . . , -)) m ( ) : P(Γ P + 1 ) × • • • × P(Γ P + k ) -→ P(Γ P + )
	is Scott-cocontinuous.
	Case of ν αϕ.
	By induction hypothesis, the function
	where ({|ϕ|} (S 1 , . . . , S k )) 0 ( ) := and
	({|ϕ|} (S 1

8, for S 1 ∈ P(Γ P + 1 ), . . . , S k ∈ P(Γ P + k ) we have {|ν m αϕ|} (S 1 , . . . , S k ) = ({|ϕ|} (S 1 , . . . , S k )) m ( ) where ({|ϕ|} (S 1 , . . . , S k )) m+1 ( ) := {|ϕ|} S 1 , . . . , S k , ({|ϕ|} (S 1 , . . . , S k )) m ( ) and where ({|ϕ|} (S 1 , . . . , S k )) 0 ( ) := and ({|ϕ|} (S 1 , . . . , S k )) 0 (⊥) := ⊥. {|ϕ|} : P(Γ P + 1 )ו • •×P(Γ P + k )×P(Γ P + ) -→ P(Γ P + ), v, S -→ {|ϕ|} v[S/α] is Scott-cocontinuous. Hence by Lem. F.8, for S 1 ∈ P(Γ P + 1 ), . . . , S k ∈ P(Γ P + k ) we have {|να.ϕ|} (S 1 , . . . , S k ) = n∈N ({|ϕ|} (S 1 , . . . , S k )) n ( )

  |} (Γ (S 1 ), . . . , Γ (S k ), ) = Γ ϕ m (S 1 , . . . , S k , ) and {|ϕ

.

. , α k : P + k , α : P + ϕ(α) : P + , and let S 1 ∈ Sub( P + 1 ), . . . , S k ∈ Sub( P + k ). Using the induction hypothesis on ϕ, an easy induction on m ∈ N shows that

{|ϕ m m |} (Γ (S 1 ), . . . , Γ (S k ), ⊥) = Γ ϕ m (S 1 , . . . , S k , ⊥)

Case of ν αϕ.

Assume α 1 : P + 1 , . . . , α k : P + k , α : P + ϕ(α) : P + , and let S 1 ∈ Sub( P + 1 ), . . . , S k ∈ Sub( P + k ). Similarly as above, for all m ∈ N we have {|ϕ m |} (Γ (S 1 ), . . . , Γ (S k ), ) = Γ ϕ m (S 1 , . . . , S k , )

  . . } and {α µ , β µ , . . . } of respectively gfp (or ν) and lfp (or µ) propositional variables. Write Σ ν (resp. Σ µ ) if the context Σ only declares gfp (resp. lfp) propositional variables.

where, as in Not. E.10 ( §E.3), we let : [START_REF] Hofmann | Abstract interpretation from büchi automata[END_REF].

Example E. [START_REF] Hofmann | A cartesian-closed category for higher-order model checking[END_REF]. Similarly as in §E.1 and §E.1, assuming ϕ : A we have

The Append Function on Colists

Example E.32 (The Append Function on Colists).

Example E.33 (Properties of Append). [START_REF] Jacobs | Introduction to Coalgebra: Towards Mathematics of States and Observation[END_REF]. Assuming ϕ : A,

We reason by cases on the refinement type of s, applying the (∨-E) rule (Fig. 8).

Proof. Let

We show λs.λt.M (g, s, t)

We apply the (∀-CI) rule on ∀k. This leads to two cases.

Case of ∀ • T (0, ).

We apply the (∀-I) rule on ∀ and assume

the result follows using the rule (ExF).

Case of ∀ • T (k+1, ).

We apply the (∀-I) rule on ∀ and assume s :

we apply the (∨-E) rule on the refinement type of s. This leads to two subcases.

(Sub)Case of [nil].

We have unfold(s) :

We have

Using the (Inj 1 -E) rule we are left with showing

We show λs.λt.M (g, s, t)

We apply the (∀-CI) rule on ∀k. This leads to two cases.

Case of ∀ • T (0, ).

We apply the (∀-I) rule on ∀ and assume s :

the result follows using the rule (ExF). Case of ∀ • T (k+1, ).

We apply the (∀-I) rule on ∀ and assume s :

We have to show

we apply the (∨-E) rule on the refinement type of s. This leads to two subcases.

(Sub)Case of [nil].

We have unfold(s) :

Since +1 ≤ k+1+ , the result then follows by applying the (Inj 0 -E) rule.

Here, Ret g (a) represents a computation which returns the value a : A, while Cont g f, k (with f, k : I → (O × Res g A)) represents a computation which on input i : I outputs f i : O and continues with the computation ki : Res g A. Provided with resumptions p, q : Res g A, the scheduler (sched g p q), adapted from [48], first evaluates p. If p returns, then the whole computation returns, with the same value. Otherwise, p evaluates to say Cont g f, k . Then (sched g p q) produces a computation which on input i : I outputs f i and continues with the computation (sched g q (ki)), thus switching arguments.

Example E.41 (Formulae on Res

: The formula ∃3ϕ holds on a resumption if there is a finite sequence of inputs which leads to a resumption satisfying ϕ, while ∀3ϕ holds on a resumption if ϕ holds at some point for any infinite sequence of inputs (this relies on Weak König Lemma). Moreover, ∃2ϕ expresses that there is an infinite sequence of inputs in which the resumption never returns and along which ϕ always holds, while ∀2ϕ expresses that for all infinite sequence of inputs, the resumption never returns and ϕ always holds. For instance, the composite formula ∃2∃3[Ret] says that there is an infinite sequence of inputs along which (1) the resumption does not return and (2), at any point, there is a finite sequence of inputs which leads to a return.

E.8 Breadth-First Tree Traversal

Infinite Binary Trees The guarded recursive type of binary trees is

The usual guarded constructors and destructors on Tree g A are represented as

Their coinductive (for A a constant type) variants are

Node := λv.λ .λr.

Example E. [START_REF] Koskinen | Local Temporal Reasoning[END_REF]. Assuming ϕ : A, we have

Breadth-First Traversal of Guarded Trees Using Forests

The following are two basic important functions on Rou g :

We then let

Example E.51 ((Non) Emptiness).

[ov] : [START_REF] Lane | Sheaves in geometry and logic: A first introduction to topos theory[END_REF]. Assuming ϕ : A, we let

we have

But by Ex. E. 53 we are done since [START_REF] Chellas | Modal Logic: An Introduction[END_REF] gives almost all the axioms and rules of Table 2 and Fig. 6, but for the [ev(-)] modality that we treat separately. We first treat the axioms of Table 2.

Proof. Most of the axioms follow from Lem. D. [START_REF] Chellas | Modal Logic: An Introduction[END_REF]. Following Def. 4.4, we include the axioms marked (C) in Table 2. The cases of [box] are trivial and omitted.

Case of (C). Since in each case, the map {|[ ]|} preserves ∧.

The case of [ev(-)] is treated directly: We can now turn to the proof of Lemma F. [START_REF] Ahmed | Step-Indexed Syntactic Logical Relations for Recursive and Quantified Types[END_REF].

Proof (Proof of Lemma F.2). By induction on A ϕ. The rules of intuitionistic propositional logic (Fig. 16) as well as of (CL) are trivial and omitted.

Case of

Case of (C ⇒ ). Since [π i ] , [fold] and [box] are maps of Heyting algebras.

In order to handle fixpoints, we have the usual monotonicity property w.r.t. subobject posets.

Lemma F. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF]. Consider, for a formula α 1 : A 1 , . . . , α k : A k ϕ, the map

For i ∈ {1, . . . , k}, if α i Pos ϕ (resp. α i Neg ϕ), then w.r.t. subobjects posets, ϕ is monotone (resp. anti-monotone) in its ith argument.

We can now turn to the proof of Lemma F.5.

Proof (Proof of Lemma F.5). By induction on A ϕ. The rules of Fig. 16 follow from the fact that in a topos, the subobjects of a given object form a Heyting algebra.

Case of

The result holds for [π i ], [fold] and [box] since [π i ] , [fold] and [box] are maps of Heyting algebras. As for [in i ], [next] and [ev(-)], this follows from the fact that the maps [in i ] ,

[next] and [ev(-)] preserve implications since they preserve ∧.

Case of

Let furthermore ≤ k and u ∈ B ( ) such that u B ψ 0 ∨ ψ 1 . We have to show ev • t↑ , u A ϕ. If u B ψ 0 , then we are done since t k [ev(ψ 0 )]ϕ, and similarly if u B ψ 1 .

Case of

Write A = A 0 + A 1 and consider t ∈ A 0 + A 1 (n). Hence t = in i (u) for some u ∈ A i (n) and we have t n [in i ] . Moreover, since the injections in 0 and in 1 have disjoint images, we have

, so that we have t↑k = in i (u) for some (unique) u ∈ A i (k). We show

For the former, let ≤ k such that t↑ = (t↑k)↑ ¬[in i ]ϕ, that is such that t↑m m [in i ]ϕ for all m ≤ . We show t↑ [in i ]¬ϕ. Hence we are done if u↑m m ϕ for all m ≤ . But if u↑m m ϕ, then we would have t↑m = in i (u↑m) m [in i ]ϕ, a contradiction. For the latter, let ≤ k such that t↑ [in i ]¬ϕ. We have to show t↑ ¬[in i ]ϕ, that is t↑m m [in i ]ϕ for all m ≤ . So assume t↑ m m [in i ]ϕ for some m ≤ . Hence, there is u ∈ A i ( m) such that t↑ m = in i (u ) and u m ϕ. But we have u = u↑ m. On the other hand, since t↑ [in i ]¬ϕ, there is some u ∈ A i ( ) such that t↑ = in i (u ) and u ↑m m ϕ for all m ≤ . But we also have u ↑ m = u↑ m, thus contradicting u↑ m m ϕ.

Cases of

By definition of θ t αϕ .

Cases of t ≥ u

These cases follows from Lem. F.7 (in θ t αϕ we assume that α is positive in ϕ) and the definition of θ t αϕ .

Cases of

By Lem. F.7 and the Knaster-Tarski Theorem, since subobject lattices of S are complete ([52, Prop. I. [START_REF] Bahr | Diamonds are not Forever: Liveness in Reactive Programming with Guarded Recursion[END_REF].5]).

Cases of

Similar to the same case in the proof of Lem. F.2.

F.2 The Safe Fragment

Lemma F.8 (Lem. D.21). The greatest fixpoint of a Scott cocontinuous function f : L → L is given by

Proof. That ν(f ) is a fixpoint of f follows from the continuity of f and the fact that the set {f n ( ) | ∈ N} is codirected, which in turn follows from the fact that f is monotone. In order to show that ν(f ) is the greatest fixpoint of f , recall that the greatest fixpoint of f is in any case given by

We trivially have ν(f ) ≤ b as ν(f ) is a fixpoint of f . For the revere inequality, for all a such that a ≤ f (a), it follows by induction on n ∈ N and from the monotony of f that we have a ≤ f n ( ) for all n ∈ N. Hence a ≤ ν(f ) for all a such that a ≤ f (a), which in turn gives b ≤ ν(f ).

Lemma F.9 (Lem. D.22). Consider a safe formula α 1 : P + 1 , . . . , α k : P + k ϕ : P + . The following two functions are Scott-cocontinuous:

In both cases, monotony w.r.t. lattice order follows by an easy induction from the positivity of safe formulae. We now turn to preservation of codirected meets. We first consider the case of {|ϕ|}. We reason by induction on ϕ.

Cases of α, , ⊥.

Trivial.

Case of ϕ ∧ ψ.

Let This case cannot occur since µαϕ is not safe.

We now turn to the case of ϕ . Most of cases are similar to those for {|ϕ|}. Also, note that

being Scott-continuous means that for D 1 ⊆ Sub( P + 1 ), . . . , D k ⊆ Sub( P + k ) codirected w.r.t. subobject lattice orders, we have

But since meets in subobject lattices of S are pointwise, the above is equivalent to have, for all n > 0 that

Cases of α, , ⊥.

Trivial.

Case of ϕ ∧ ψ.

Let D 1 ⊆ Sub( P + 1 ), . . . , D k ⊆ Sub( P + k ) be codirected. By induction hypothesis we obtain

and the result is trivial. Case of ϕ ∨ ψ.

Let D 1 ⊆ Sub( P + 1 ), . . . , D k ⊆ Sub( P + k ) be codirected. By induction hypothesis we obtain

By monotonicity w.r.t. subobject lattice orders, we trivially get

Note that ψ is assumed to be closed since [ev(ψ)]ϕ is safe. Let D 1 ⊆ Sub( P + 1 ), . . . , D k ⊆ Sub( P + k ) be codirected. Write P + = R + → Q + . We show that for all n > 0 we have

Let n > 0 and t ∈ P + (n). Then we are done since by induction hypothesis we have:

Cases of θ t αϕ and ν αϕ.

These cases are handled exactly as for {|-|}.

Case of µαϕ.

This case cannot occur since µαϕ is not safe.

Proposition F.10 (Prop. [START_REF] Bahr | Simply RaTT: A Fitch-Style Modal Calculus for Reactive Programming without Space Leaks[END_REF].3). Let α 1 : P + 1 , . . . , α k : P + k ϕ : P + be a safe formula. Given S 1 ∈ Sub( P + 1 ), . . . , S k ∈ Sub(

Proof. We reason by induction on the derivation of α 1 : P + 1 , . . . , α k : P + k ϕ : P + . In all cases but θ t αϕ and ν αϕ, the parameters are irrelevant and we omit them.

Cases of α,

and ⊥.

Trivial.

Case of ϕ ∧ ψ.

Let x ∈ Γ P + . Then we are done since by induction hypothesis we have

Assume toward a contradiction that there are k, > 0 with (say

Hence, we have either x n (•) ∈ ϕ (n) for all n > 0 or x n (•) ∈ ψ (n) for all n > 0, and the result follows by induction hypothesis.

Case of a refinement type {A | ϕ}.

The result follows from monotony of forcing (i.e. that ϕ is a subobject of A ) .

Case of 1.

The result is trivial as x n 1 for all n > 0. Case of T 0 + T 1 .

Assume x n T 0 + T 1 and let k ≤ n. Then we have x = in i • y for some i = 0, 1 and some y ∈ Γ |T i | such that y n T i . By induction hypothesis we get y k T i , so that

Assume x n T 0 × T 1 and let k ≤ n. Then for each i = 0, 1 we have Trivial.

Lemma F.14 (Lem. D.26). For a pure type A and x ∈ Γ A , we have x n A for all n > 0.

Proof. The proof is by induction on pairs (n, A), using implicitly Lem. D.2 whenever required.

Case of 1.

Trivial.

Case of A

Then we are done since y n A i by induction hypothesis.

Case of A