Étienne Miquey
email: emiquey@inria.fr

Équipe Gallinette

A sequent calculus with dependent types for classical arithmetic

Keywords: Curry-Howard, dependent choice, classical arithmetic, side e ects, dependent types, classical realizability, sequent calculus Closures Commands p||e p, q :: Contexts Forcing contexts Delimited continuations

, Herbelin developed dPA ω , a calculus in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quanti cation as a stream of it components. However, the property of normalization (and therefore the one of soundness) was only conjectured. The di culty for the proof of normalization is due to the simultaneous presence of dependent types (for the constructive part of the choice), of control operators (for classical logic), of coinductive objects (to encode functions of type N → A into streams (a 0 , a 1 , . . .)) and of lazy evaluation with sharing (for these coinductive objects).

. By combining the techniques developed in these papers, we manage to de ne a realizability interpretation à la Krivine of our calculus that allows us to prove normalization and soundness.

Introduction

1.1 Realizing AC N and DC in presence of classical logic Dependent types are one of the key features of Martin-Löf's type theory [START_REF] Martin-Löf | An intuitionistic theory of types. In twenty-ve years of constructive type theory[END_REF], allowing formulas to refer to terms. Notably, the existential quanti cation rule is de ned so that a proof term of type ∃x A .B is a pair (t, p) where t-the witness-is of type A, while p-the proof -is of type B[t/x]. Dually, the theory enjoys two elimination rules: one with a destructor wit to extract the witness, the second one with a destructor prf to extract the proof. This allows for a simple and constructive proof of the full axiom of choice [START_REF] Martin-Löf | An intuitionistic theory of types. In twenty-ve years of constructive type theory[END_REF]: AC A := λH .(λx. wit (Hx), λx. prf (Hx)) : (∀x A .∃ B .P(x, )) → ∃f A→B .∀x A .P(x, f (x))

This term is nothing more that an implementation of Brouwer-Heyting-Kolomogoro interpretation of the axiom of choice [START_REF] Kolmogoro | Zur deutung der intuitionistischen logik[END_REF]:

given a proof H of ∀x A .∃ B .P(x, ), it constructs a choice function which simply maps any x to the witness of Hx, while the proof that this function is sound w.r.t. P returns the corresponding certi cate. Yet, this approach deeply relies on the constructivity of the theory. We present here a continuation of Herbelin's works [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF], who proposed a way of scaling up Martin-Löf's proof to classical logic. This is an extended version of LICS 2018 paper.. The rst idea is to restrict the dependent types to the fragment of negative-elimination-free proofs ( ) which, intuitively, only contains constructive proofs behaving as values. The second idea is to represent a countable universal quanti cation as an in nite conjunction. This allows us to internalize into a formal system (called dPA ω ) the realizability approach [2,[START_REF] Escardó | Bar recursion and products of selection functions[END_REF] as a direct proofsas-programs interpretation.

Informally, let us imagine that given a proof H : ∀x N .∃ B .P(x, ), we could create the in nite sequence H ∞ = (H 0, H 1, . . .) and select its n th -element with some function nth. Then, one might wish that: λH .(λn. wit (nth n H ∞ ), λn. prf (nth n H ∞ )) could stand for a proof for AC N . One problem is that even if we were e ectively able to build such a term, H ∞ might still contain some classical proofs. Therefore, two copies of Hn might end up behaving di erently according to the contexts in which they are executed, and thus returning two di erent witnesses (which is known to lead to logical inconsistencies [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF]). This problem can be xed by using a shared version of H ∞ , that is to say: λH . let a = H ∞ in (λn. wit (nth n a), λn. prf (nth n a) .

In words, the term H ∞ is now shared between all the places which may require some of its components.

It only remains to formalize the intuition of H ∞ , which is done by means of a stream cofix 0 f n [(Hn, f (S(n)))] iterated on f with parameter n, starting with 0:

AC N := λH .let a = cofix 0 f n [(Hn, f (S(n))] in (λn. wit (nth n a), λn. prf (nth n a) .

The stream is, at the level of formulas, an inhabitant of a coinductively de ned in nite conjunction ν 0 X n (∃ .P(n, ))∧X (n +1). Since we cannot a ord to pre-evaluate each of its components, and we thus have to use a lazy call-by-value evaluation discipline. However, it still might be responsible for some non-terminating reductions, all the more as classical proofs may contain backtrack.

Normalization of dPA ω

In [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF], the property of normalization (on which relies the one of consistency) was only conjectured, and the proof sketch that was given turned out to be hard to formalize properly. Our rst attempt to prove the normalization of dPA ω was to derive a continuationpassing style translation (CPS), but translations appeared to be hard to obtain for dPA ω as such. In addition to the di culties caused by control operators and co-xpoints, dPA ω reduction system is de ned in a natural deduction fashion, with contextual rules where the contexts involved can be of arbitrary depth. This kind of rules are indeed di cult to faithfully translate through a CPS.

Rather than directly proving the normalization of dPA ω , we choose to rst give an alternative presentation of the system under the form of a sequent calculus, which we call dLPA ω . Indeed, sequent calculus presentations of a calculus usually provides good intermediate steps for CPS translations [9,[START_REF] Munch-Maccagnoni | Syntax and Models of a non-Associative Composition of Programs and Proofs[END_REF][START_REF] Munch-Maccagnoni | Polarised Intermediate Representation of Lambda Calculus with Sums[END_REF] since they enforce a decomposition of the reduction system into ner-grain rules. To this aim, we rst handled separately the di culties peculiar to the de nition of such a calculus: on the one hand, we proved with Herbelin the normalization of a calculus with control operators and lazy evaluation [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF]; on the other hand, we de ned a classical sequent calculus with dependent types [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF]. By combining the techniques developed in these frameworks, we nally manage to de ne dLPA ω , which we present here and prove to be normalizing.

Realizability interpretation of classical call-by-need

In the call-by-need evaluation strategy, the substitution of a variable is delayed until knowing whether the argument is needed. To this end, Ariola et al. [START_REF] Ariola | Classical call-byneed sequent calculi: The unity of semantic artifacts[END_REF] proposed the λ [l τ ⋆] -calculus, a variant of Curien-Herbelin's λµ μ-calculus [7] in which substitutions are stored in an explicit environment. Thanks to Danvy's methodology of semantics artifacts [8], which consists in successively re ning the reduction system until getting context-free reduction rules 1 , they obtained an untyped CPS translation for the λ [l τ ⋆] -calculus. By pushing one step further this methodology, we showed with Herbelin how to obtain a realizability interpretation à la Krivine for this framework [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF]. The main idea, in contrast to usual models of Krivine realizability [START_REF] Krivine | Realizability in classical logic[END_REF], is that realizers are de ned as pairs of a term and a substitution. The adequacy of the interpretation directly provided us with a proof of normalization, and we shall follow here the same methodology to prove the normalization of dLPA ω .

A sequent calculus with dependent types

While sequent calculi are naturally tailored to smoothly support CPS interpretations, there was no such presentation of language with dependent types compatible with a CPS. In addition to the problem of safely combining control operators and dependent types [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF], the presentation of a dependently typed language under the form of a sequent calculus is a challenge in itself. In [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF], we introduced such a system, called dL t p , which is a call-by-value sequent calculus with classical control and dependent types. In comparison with usual type systems, we decorated typing derivations with a list of dependencies to ensure subject reduction. Besides, the soundness of the calculus was justi ed by means of a CPS translation taking the dependencies into account. The very de nition of the translation constrained us to use delimited continuations in the calculus when reducing dependently typed terms. At the same time, this unveiled the need for the syntactic restriction of dependencies to the negative-elimination-free fragment as in [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]. Additionally, we showed how to relate our calculus to a similar system by Lepigre [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF], whose consistency is proved by means of a realizability interpretation. In the present paper, we use the same techniques, namely a list of dependencies and delimited continuations, to ensure the soundness of dLPA ω , and we follow Lepigre's interpretation of dependent types for the de nition of our realizability model.

Contributions of the paper

The main contributions of this paper can be stated as follows. First, we de ne dLPA ω (Section 2), a sequent calculus with classical control, dependent types, inductive and coinductive xpoints and lazy evaluation made available thanks to the presence of stores. This calculus can be seen as a sound combination of dL t p [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF] and the λ [l τ ⋆] -calculus [START_REF] Ariola | Classical call-byneed sequent calculi: The unity of semantic artifacts[END_REF][START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF] extended with the expressive power of dPA ω [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]. Second, we prove the properties of normalization and soundness for dLPA ω thanks to a realizability interpretation à la Krivine, which we obtain by applying Danvy's methodology of semantic artifacts (Sections 3 and 4). Lastly, dLPA ω incidentally provides us with a direct proofs-as-programs interpretation of classical arithmetic with dependent choice, as sketched in [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF].

This paper is partially taken from the Chapter 8 of the author's PhD thesis [START_REF] Miquey | Classical realizability and side-e ects[END_REF]. For more detailed proofs, we refer the reader to the di erent appendices.

2 A sequent calculus with dependent types for classical arithmetic

Syntax

The language of dLPA ω is based on the syntax of dL t p [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF], extended with the expressive power of dPA ω [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF] and with explicit stores as in the λ [l τ ⋆] -calculus [START_REF] Ariola | Classical call-byneed sequent calculi: The unity of semantic artifacts[END_REF]. We stick to a strati ed presentation of dependent types, that is to say that we syntactically distinguish terms-that represent mathematical objects-from proof terms-that represent mathematical proofs. In particular, types and formulas are separated as well, matching the syntax of dPA ω 's formulas. Types are de ned as nite types with the set of natural numbers as the sole ground type, while formulas are inductively built on atomic equalities of terms, by means of conjunctions, disjunctions, rst-order quanti cations, dependent products and coinductive formulas:

Types T , U ::= N | T → U Formulas A, B ::= ⊤ | ⊥ | t = u | A ∧ B | A ∨ B | Πa : A.B | ∀x T .A | ∃x T .A | ν t x, f A
The syntax of terms is identical to the one in dPA ω , including functions λx.t and applications tu, as well as a recursion operator rec t

x [t 0 | t S ], so that terms represent objects in arithmetic of nite types. As for proof terms (and contexts, commands), they are now de ned with all the expressiveness of dPA ω . Each constructor in the syntax of formulas is re ected by a constructor in the syntax of proofs and by the dual co-proof (i.e. destructor) in the syntax of evaluation contexts. Amongst other things, the syntax includes pairs (t, p) where t is a term and p a proof, which inhabit the dependent sum type ∃x T .A; dual co-pairs μ(x, a).c which bind the (term and proof) variables x and a in the command c; functions λx.p inhabiting the type ∀x T .A together with their dual, stacks t • e where e is a context whose type might be dependent in t; functions λa.p which inhabit the dependent product type Πa : A.B, and, dually, stacks q•e, where e is a context whose type might be dependent in q; a proof term refl which is the proof of atomic equalities t = t and a destructor μ=.c which allows us to type the command c modulo an equality of terms; operators fix t ax [p 0 | p S ] and cofix t b x [p], as in dPA ω , for inductive and coinductive reasoning; delimited continuations through proofs µ t p.c tp and the context t p; a distinguished context [] of type ⊥, which allows us to reason ex-falso. As in dL t p , the syntax of proofs, contexts and commands is de ned as a restriction of the previous syntax. Technically, they are de ned (modulo α-conversion) with only one distinguished context variable ⋆ (and consequently only one binder µ ⋆.c), and without stacks of the shape t • e or q • e (to avoid applications). Intuitively, one can understand proofs as the proofs that cannot drop their continuation2 . The commands c t p within delimited continuations are de ned as commands of the shape p|| t p or formed by a proof and a context of the shape μa.

c t p τ , μ[a 1 .c t p |a 2 .c ′ t p
], μ(a 1 , a 2 ).c t p or μ(x, a).c t p .

We adopt a call-by-value evaluation strategy except for xpoint operators 3 , which are evaluated in a lazy way. To this purpose, we use stores4 in the spirit of the λ [l τ ⋆] -calculus, which are de ned as lists of bindings of the shape [a := p] where p is a value or a (co-) xpoint, and of bindings of the shape [α := e] where e is any context. We assume that each variable occurs at most once in a store τ , we thus reason up to α-reduction and we assume the capability of generating fresh names. Apart from evaluation contexts of the shape μa.c and co-variables α, all the contexts are forcing contexts which eagerly require a value to be reduced and trigger the evaluation of lazily stored terms. The resulting language is given in Figure 1.

Reduction rules

The reduction system of dLPA ω is given in Figure 2. The basic rules are those of the call-by-value λµ μ-calculus and of dL t p . The rules for delimited continuations are exactly the same as in dL t p , except that we have to prevent t p from being caught and stored by a proof µα .c. We thus distinguish two rules for commands of the shape µα .c ||e , depending on whether e is of the shape e t p or not. In the former case, we perform the substitution [e t p /α], which is linear since µα .c is necessarily . We should also mention in passing that we abuse the syntax in every other rules, since e should actually refer to e or e tp (or the reduction of delimited continuations would be stuck). Elimination rules correspond to commands where the proof is a constructor (say of pairs) applied to values, and where the context is the matching destructor. Call-by-value rules correspond to (ς) rule of Wadler's sequent calculus [START_REF] Wadler | Call-by-value is dual to call-by-name[END_REF]. The next rules express the fact that (co-) xpoints are lazily stored, and reduced only if their value is eagerly demanded by a forcing context. Lastly, terms are reduced according to the usual β-reduction, with the operator rec computing with the usual recursion rules. It is worth noting that the strati ed presentation allows to de ne the reduction of terms as external: within proofs and contexts, terms are reduced in place. Consequently, as in dL t p the very same happen for proofs embedded within terms. Computationally speaking, this corresponds indeed to the intuition that terms are reduced on an external device.

Typing rules

As often in Martin-Löf's intensional type theory, formulas are considered up to equational theory on terms. We denote by A ≡ B the re exive-transitive-symmetric closure of the relation ⊲ induced by the reduction of terms and proofs as follows:

A[t] ⊲ A[t ′ ] whenever t → β t ′ A[p] ⊲ A[q]
whenever ∀α ( p||α → q||α ) in addition to the reduction rules for equality and for coinductive formulas:

0 = S(t) ⊲ ⊥ S(t) = 0 ⊲ ⊥ S(t) = S(u) ⊲ t = u ν t f x A ⊲ A[t/x][ν f x A/f ( ) = 0]
We work with one-sided sequents where typing contexts are de ned by:

Γ, Γ ′ ::= ε | Γ, x : T | Γ, a : A | Γ, α : A ⊥ ⊥ | Γ, t p : A ⊥ ⊥ .
using the notation α : A ⊥ ⊥ for an assumption of the refutation of A. This allows us to mix hypotheses over terms, proofs and contexts while keeping track of the order in which they are added (which is necessary because of the dependencies). We assume that a variable occurs at most once in a typing context.

We de ne nine syntactic kinds of typing judgments: six5 in regular mode, that we write Γ ⊢ σ , and three6 more for the dependent mode, that we write Γ ⊢ d ; σ . In each case, σ is a list of dependencies-we explain the presence of a list of dependencies in

= e] V || μa.cτ ′ τ → cτ [a := V ]τ ′ Elimination rules ι i (V )|| μ[a 1 .c 1 | a 2 .c 2 ] τ → c i τ [a i := V ] (V 1 ,V 2 )|| μ(a 1 , a 2 ).c τ → cτ [a 1 := V 1 ][a 2 := V 2 ] (V t ,V )|| μ(x, a).c τ → (c[t/x])τ [a := V ] refl|| μ=.c τ → cτ Delimited continuations (if cτ → cτ ′ ) µ t p.c
Laziness (a fresh) cofix V t b x [p]||e τ → a||e τ [a := cofix V t b x [p]] (a fresh) fix V t b x [p 0 | p S ]||e τ → a||e τ [a := fix V t b x [p 0 | p S ]] Lookup V ||α τ [α := e]τ ′ → V ||e τ [α := e]τ ′ a|| f τ [a := V ]τ ′ → V ||a τ [a := V ]τ ′ (b ′ fresh) a|| f τ [a := cofix V t b x [p]]τ ′ → p[V t /x][b ′ /b]|| μa. a|| f τ ′ τ [b ′ := λ .cofix b x [p]] a|| f τ [a := fix 0 b x [p 0 | p S ]]τ ′ → p 0 || μa. a|| f τ ′ τ (b ′ fresh) a|| f τ [a := fix S (t ) b x [p 0 | p S ]]τ ′ → p S [t/x][b ′ /b]|| μa. a||f τ ′ τ [b ′ := fix t b x [p 0 | p S ]] Terms (if t -→ β t ′ ) T [t]τ → T [t ′ ]τ (∀α, p||α τ → (t, p ′ )||α τ ) T [wit p]τ -→ β T [t] (λx.t)V t -→ β t[V t /x] rec 0 x [t 0 | t S ] -→ β t 0 rec S (u) x [t 0 | t S ] -→ β t S [u/x][rec u x [t 0 | t S ]/ ]
where:

C t [ ] ::= ([ ], p)||e | fix [ ] ax [p 0 | p S ]||e | cofix [ ] b x [p]||e | λx.p||[ ] • e T [ ] ::= C t [ ] | T [[ ]u] | T [rec [ ] x [t 0 | t S ]]
σ ::= ε | σ {p|q}
The substitution on formulas according to a list of dependencies σ is de ned by:

ε(A) {A} σ {p|q}(A) σ (A[q/p]) if q ∈ σ (A) otherwise
Because the language of proof terms include constructors for pairs, injections, etc, the notation A[q/p] does not refer to usual substitutions properly speaking: p can be a pattern (for instance (a 1 , a 2 )) and not only a variable. We shall attract the reader's attention to the fact that all typing judgments include a list of dependencies. Indeed, as in the λ [l τ ⋆]calculus, when a proof or a context is caught by a binder, say V and μa, the substitution [V /a] is not performed but rather put in the store: τ [a := V ]. Now, consider for instance the reduction of a dependent function λa.p (of type Πa : A.B) applied to a stack V •e 7 : 7 We refer the reader to [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF] for detailed explanations on this rule.

λa.p||V • e τ → µ t p. V || μa. p|| t p ||e τ → µ t p. p|| t p ||e τ [a := V ] → p||e τ [a := V ]
Since p still contains the variable a, whence his type is still B[a], whereas the type of e is B[V ]. We thus need to compensate the missing substitution 8 .

We are mostly left with two choices. Either we mimic the substitution in the type system, which would amount to the following typing rule:

Γ, Γ ′ ⊢ τ (c) Γ ⊢ τ : Γ ′ Γ ⊢ cτ where: τ [α := e](c) τ (c) τ [a := p N ](c) τ (c[p N /a]) (p ∈ ) τ [a := p](c) τ (c) (p )
Or we type stores in the spirit of the λ [l τ ⋆] -calculus, and we carry along the derivations all the bindings liable to be used in types, which constitutes again a list of dependencies.

The former solution has the advantage of solving the problem before typing the command, but it has the aw of performing computations which would not occur in the reduction system. For instance, the substitution τ (c) could duplicate co-xpoints (and their typing derivations), which would never happen in the calculus. That is the reason why we favor the other solution, which is closer to the calculus in our opinion. Yet, it has the drawback that it forces us to carry a list of dependencies even in regular mode. Since this list is xed (it does not evolve in the derivation except

Regular types Γ ⊢ σ p : A Γ ⊢ σ e : B ⊥ ⊥ σ (A) = σ (B) Γ ⊢ σ p||e (C ) Γ, Γ ′ ⊢ σ σ ′ c Γ ⊢ σ τ : (Γ ′ ; σ ′ ) Γ ⊢ cτ (l ) Γ ⊢ σ τ : (Γ ′ ; σ ′ ) Γ, Γ ′ ⊢ σ σ ′ p : A Γ ⊢ σ τ [a := p] : (Γ ′ , a : A; σ ′ {a|p}) (τ p ) (a : A) ∈ Γ Γ ⊢ σ a : A Dependent mode Γ, Γ ′ ⊢ d c t p ; σσ ′ Γ ⊢ σ τ : (Γ ′ ; σ ′ ) Γ ⊢ d c t p τ ; σ (l d ) Γ, Γ ′ ⊢ σ p : A Γ, t p : B ⊥ ⊥ , Γ ′ ⊢ d e : A ⊥ ⊥ ; σ {•|p} Γ, t p : B ⊥ ⊥ , Γ ′ ⊢ d p||e ; σ (C d ) Γ, t p : A ⊥ ⊥ ⊢ d c t p ; σ Γ ⊢ σ µ t p.c t p : A (µ t p) σ (A) = σ (B) Γ, t p : A ⊥ ⊥ , Γ ′ ⊢ d t p : B ⊥ ⊥ ; σ {•|p} ( t p) Γ, a i : A i ⊢ d c i t p ; σ {ι i (a i )|p N }) ∀i ∈ {1, 2} Γ ⊢ d μ[a 1 .c 1 t p | a 2 .c 2 t p ] : (A 1 ∨ A 2 ) ⊥ ⊥ ; σ {•|p N } (∨ d l ) Γ, a : A ⊢ d c t p τ ′ ; σ {a|p N } Γ ⊢ d μa.c t p τ ′ : A ⊥ ⊥ ; σ {•|p N } Γ ⊢ σ p : ∃x T .A p Γ ⊢ σ wit p : T (wit ) Figure 3.
Type system for dLPA ω when stores occur), we di erentiate the denotation of regular typing judgments, written Γ ⊢ σ , from the one of judgments in dependent mode, which we write Γ ⊢ d ; σ to highlight that σ grows along derivations. The type system we obtain is given in Figure 3.

Subject reduction

We shall now prove that typing is preserved along reduction. As for the λ [l τ ⋆] -calculus, the proof is simpli ed by the fact that substitutions are not performed (except for terms), which keeps us from proving the safety of the corresponding substitutions. Yet, we rst need to prove some technical lemmas about dependencies. To this aim, we de ne a relation σ ⇛ σ ′ between lists of dependencies, which expresses the fact that any typing derivation obtained with σ could be obtained as well as with σ ′ :

Γ ⊢ p : ∃x T .A Γ, x : T , a : A ⊢ q : B[(x, a)/•] p ⇒ • B Γ ⊢ dest p as (x, a) in q : B[p/•] (dest) Γ ⊢ p : ⊥ Γ ⊢ exfalso p : B (⊥) Γ, a : A ⊢ q : B[a/•] p ⇒ • B Γ ⊢ let a = p in q : B[p/•] (let) Γ ⊢ p : A 1 ∧ A 2 Γ, a 1 : A 1 , a 2 : A 2 ⊢ q : B[(a 1 , a 2 )/•] p ⇒ • B Γ ⊢ split p as (a 1 , a 2 ) in q : B[p/•] (split) Γ ⊢ p : A 1 ∧ A 2 Γ ⊢ π i (p) : A i (∧ i E ) Γ, α : A ⊥ ⊥ ⊢ p : A Γ, α : A ⊥ ⊥ ⊢ throw α p : B (throw) Γ ⊢ p : A 1 ∨ A 2 Γ, a i : A i ⊢ q : B[ι i (a) i /•] for i = 1, 2 p ⇒ • B Γ ⊢ case p of [a 1 .p 1 | a 2 .p 2 ] : B[p/•] (case) Γ, α : A ⊥ ⊥ ⊢ p : A Γ ⊢ catch α p : A (catch) Γ ⊢ p : ∃x T .A(x) Γ ⊢ prf p : A(wit p) (prf )

Natural deduction as macros

We can recover the usual proof terms for elimination rules in natural deduction systems, and in particular the ones from dPA ω , by de ning them as macros in our language. The de nitions are straightforward, using delimited continuations for let . . . in and the constructors over proofs which might be dependently typed: 4, are admissible.

let a = p in q µα p . p|| μa. q||α p split p as (a 1 , a 2 ) in q µα p . p|| μ(
One can even check that the reduction rules in dLPA ω for these proofs almost mimic the ones of dPA ω . To be more precise, the rules of dLPA ω do not allow to simulate each rule of dPA ω , due to the head-reduction strategy amongst other things. Nonetheless, up to a few details the reduction of a command in dLPA ω follows one particular reduction path of the corresponding proof in dPA ω , or in other words, one reduction strategy.

The main result is that using the macros, the same proof terms are suitable for countable and dependent choice [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]. We do not state it here, but following the approach of [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF], we could also extend dLPA ω to obtain a proof for the axiom of bar induction.

Theorem 2.4 (Countable choice [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]). We have:

AC N := λH .let a = cofix 0 bn [(Hn,b(S(n))] in (λn. wit (nth n a), λn. prf (nth n a) : ∀x N ∃ T P(x, ) → ∃f N→T ∀x N P(x, f (x))
where nth n a := π 1 (fix n

x,c [a | π 2 (c)]). Theorem 2.5 (Dependent choice [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]). We have:

DC := λH .λx 0 . let a = (x 0 , cofix 0 bn [d n ])f six in (λn. wit (nth n a), (refl, λn.π 1 (prf (prf (nth n a))))) : ∀x T .∃ T .P(x, ) → ∀x T 0 .∃f ∈ T N .(f (0) = x 0 ∧ ∀n N .P(f (n), f (s(n)))) where d n := dest Hn as ( , c) in ( , (c, b ))) and nth n a := fix n x,d [a | (wit (prf d), π 2 (prf (prf (d))))].
3 Small-step calculus

As for the λ [l τ ⋆] -calculus [START_REF] Ariola | Classical call-byneed sequent calculi: The unity of semantic artifacts[END_REF][START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF], we follow here Danvy's methodology of semantic artifacts [START_REF] Ariola | Classical call-byneed sequent calculi: The unity of semantic artifacts[END_REF]8] to obtain a realizability interpretation. We rst decompose the reduction system of dLPA ω into small-step reduction rules, that we denote by s . This requires a re nement and an extension of the syntax, that we shall now present. To keep us from boring the reader sti with new (huge) tables for the syntax, typing rules and so forth, we will introduce them step by step. We hope it will help the reader to convince herself of the necessity and of the somewhat naturality of these extensions.

Values

First of all, we need to re ne the syntax to distinguish between strong and weak values in the syntax of proof terms. As in the λ [l τ ⋆] -calculus, this re nement is induced by the computational behavior of the calculus: weak values are the ones which are stored by μ binders, but which are not values enough to be eliminated in front of a forcing context, that is to say variables. Indeed, if we observe the reduction system, we see that in front of a forcing context f , a variable leads a search through the store for a "stronger" value, which could incidentally provoke the evaluation of some xpoints. On the other hand, strong values are the ones which can be reduced in front of the matching forcing context, that is to say functions, refl, pairs of values, injections or dependent pairs:

Weak values V ::= a | Strong values ::= ι i (V ) | (V ,V ) | (V t , V ) | λx.p | λa.p | refl
This allows us to distinguish commands of the shape || f τ , where the forcing context (and next the strong value) are examined to determine whether the command reduces or not; from commands of the shape a|| f τ where the focus is put on the variable a, which leads to a lookup for the associated proof in the store.

Terms

Next, we need to explicit the reduction of terms. To this purpose, we include a machinery to evaluate terms in a way which resemble the evaluation of proofs. In particular, we de ne new commands which we write t ||π where t is a term and π is a context for terms (or co-term). Co-terms are either of the shape μx.c or stacks of the shape u • π . These constructions are the usual ones of the λµ μcalculus (which are also the ones for proofs). We also extend the de nitions of commands with delimited continuations to include the corresponding commands for terms:

Commands Co-terms c ::= p||e | t ||π π ::= t • π | μx.c c t p ::= • • • | t ||π t p π t p ::= t • π t p | μx.c t p
We give typing rules for these new constructions, which are the usual rules for typing contexts in the λµ μ-calculus:

Γ ⊢ t : T Γ ⊢ π : U ⊥ ⊥ Γ ⊢ t • π : (T → U ) ⊥ ⊥ (→ l ) c : (Γ, x : T ) Γ ⊢ μx.c : T ⊥ ⊥ ( μx ) Γ ⊢ σ t : T Γ ⊢ σ π : T ⊥ ⊥ Γ ⊢ σ t ||π ( t )
It is worth noting that the syntax as well as the typing and reduction rules for terms now match exactly the ones for proofs 9 . In other words, with these de nitions, we could abandon the strati ed presentation without any trouble, since reduction rules for terms will naturally collapse to the ones for proofs.

Co-delimited continuations

Finally, in order to maintain typability when reducing dependent pairs of the strong existential type, we need to add what we call codelimited continuations. As observed in [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF], the CPS translation of pairs (t, p) in dL t p is not the expected one, re ecting the need for a special reduction rule. Indeed, consider such a pair of type ∃x T .A, the standard way of reducing it would be a rule like: We thus equip the language with new contexts μ ť p.c ť p , which we call co-shifts and where c ť p is a command whose last cut is of the shape ť p||e . This corresponds formally to the following syntactic sets, which are dual to the ones introduced for delimited continuations:

(t,

Contexts

Co-delimited continuations

e ::= • • • | μ ť p.c ť p c ť p ::= p N ||e ť p | t ||π ť p | ť p||e e ť p ::= μa.c ť p | μ[a 1 .c ť p | a 2 .c ′ ť p ] | μ(a 1 , a 2 ).c ť p | μ(x, a).c ť p π ť p ::= t • π ť p | μx.c ť p e N ::= • • • | μ ť p.c ť p
This might seem to be a heavy addition to the language, but we insist on the fact that these artifacts are merely the dual constructions of delimited continuations introduced in dL t p , with a very similar intuition. In particular, it might be helpful for the reader to think of the fact that we introduced delimited continuations for type safety of the evaluation of dependent products in Πa : A.B (which naturally extends to the case ∀x T .A). Therefore, to maintain type safety of dependent sums in ∃x T .A, we need to introduce the dual constructions of co-delimited continuations. We also give 9 Except for substitutions of terms, which we could store as well.

typing rules to these constructions, which are dual to the typing rules for delimited-continuations:

Γ, ť p : A ⊢ d c ť p ; σ Γ ⊢ σ μ ť p.c ť p : A ⊥ ⊥ ( μ ť p) Γ, Γ ′ ⊢ σ e : A ⊥ ⊥ σ (A) = σ (B) Γ, ť p : B, Γ ′ ⊢ d ť p||e ; σ ( ť p)
Note that we also need to extend the de nition of list of dependencies to include bindings of the shape {x |t } for terms, and that we have to give the corresponding typing rules to type commands of terms in dependent mode:

c : (Γ, x : T ; σ {x |t }) Γ ⊢ d μx.c : T ⊥ ⊥ ; σ {•|t } ( μd x ) Π t Γ, ť p : B, Γ ′ ⊢ d π : A ⊥ ⊥ ; σ {•|t } Γ, ť p : B, Γ ′ ⊢ d t ||π ; σ (C d t )
where Π t Γ, Γ ′ ⊢ σ t : T . The small-step reduction system is given in Appendix C. The rules are written c ι τ s c ′ o τ ′ where the annotation ι, p on commands are indices (i.e. c, p, e,V , f , t, π, V t ) indicating which part of the command is in control. As in the λ [l τ ⋆] -calculus, we observe an alternation of steps descending from p to f for proofs and from t to V t for terms. The descent for proofs can be divided in two main phases. During the rst phase, from p to e we observe the call-by-value process, which extracts values from proofs, opening recursively the constructors and computing values. In the second phase, the core computation takes place from V to f , with the destruction of constructors and the application of function to their arguments. The laziness corresponds precisely to a skip of the rst phase, waiting to possibly reach the second phase before actually going through the rst one.

Here again, reduction is safe with respect to the type system: Proposition 3.1 (Subject reduction). The small-step reduction rules satisfy subject reduction.

Proof. The proof is again an induction on s , see Appendix C.

It is also direct to check that the small-step reduction system simulates the big-step one, and in particular that it preserves the normalization : Proposition 3.2. If a closure cτ normalizes for the reduction s , then it normalizes for →.

Proof. By contraposition, see Appendix C.

A realizability interpretation of dLPA ω

We shall now present the realizability interpretation of dLPA ω , which will nally give us a proof of its normalization. Here again, the interpretation combines ideas of the interpretations for the λ [l τ ⋆] -calculus [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF] and for dL t p through the embedding in Lepigre's calculus [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF][START_REF] Miquey | A classical sequent calculus with dependent types[END_REF]. Namely, as for the λ [l τ ⋆] -calculus, formulas will be interpreted by sets of proofs-in-store of the shape (p|τ ), and the orthogonality will be de ned between proofs-in-store (p|τ ) and contexts-in-store (e |τ ′ ) such that the stores τ and τ ′ are compatible.

We recall the main de nitions necessary to the realizability interpretation:

De nition 4.1 (Proofs-in-store). We call closed proof-in-store (resp. closed context-in-store, closed term-in-store, etc) the combination of a proof p (resp. context e, term t, etc) with a closed store τ such that FV (p) ⊆ dom(τ ). We use the notation (p|τ ) to denote such a pair. In addition, we denote by Λ p (resp. Λ e , etc.) the set of all proofs and by Λ τ p (resp. Λ τ e , etc.) the set of all proofs-in-store. We denote the sets of closed closures by C 0 , and we identify (c |τ ) with the closure cτ when c is closed in τ .

We now recall the notion of compatible stores [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF], which allows us to de ne an orthogonality relation between proofs-and contexts-in-store.

De nition 4.2 (Compatible stores and union). Let τ and τ ′ be stores, we say that:

• they are independent and note τ #τ ′ if dom(τ ) ∩ dom(τ ′ ) = ∅.

• they are compatible and note τ ⋄τ ′ if for all variables a (resp.

co-variables α) present in both stores: a ∈ dom(τ ) ∩ dom(τ ′ ); the corresponding proofs (resp. contexts) in τ and τ ′ coincide. • τ ′ is an extension of τ and we write τ ⊳ τ ′ whenever τ ⋄ τ ′ and dom(τ ) ⊆ dom(τ ′ ). • ττ ′ is the compatible union of compatible closed stores τ and τ ′ . It is de ned as ττ ′ join(τ , τ ′ ), which itself given by:

join(τ 0 [a := p]τ 1 , τ ′ 0 [a := p]τ ′ 1 ) τ 0 τ ′ 0 [a := p]join(τ 1 , τ ′ 1 ) join(τ 0 [α := e]τ 1 , τ ′ 0 [α := e]τ ′ 1 ) τ 0 τ ′ 0 [α := e]join(τ 1 , τ ′ 1 ) join(τ 0 , τ ′ 0 ) τ 0 τ ′ 0
where τ 0 #τ ′ 0 . The next lemma (which follows from the previous de nition) states the main property we will use about union of compatible stores.

Lemma 4.3. If τ and τ ′ are two compatible stores, then τ ⊳ ττ ′ and τ ′ ⊳ ττ ′ . Besides, if τ is of the form τ 0 [x := t]τ 1 , then ττ ′ is of the form τ 0 [x := t]τ 1 with τ 0 ⊳ τ 0 and τ 1 ⊳ τ 1 .

We can now de ne the notion of pole, which has to satisfy an extra condition due to the presence of delimited continuations De nition 4.4 (Pole). A subset ⊥ ⊥ ∈ C 0 is said to be saturated or closed by anti-reduction whenever for all (c |τ ), (c ′ |τ ′ ) ∈ C 0 , we have:

(c ′ τ ′ ∈ ⊥ ⊥) ∧ (cτ → c ′ τ ′ ) ⇒ (cτ ∈ ⊥ ⊥)
It is said to be closed by store extension if whenever cτ is in ⊥ ⊥, for any store τ ′ extending τ , cτ ′ is also in ⊥ ⊥:

(cτ ∈ ⊥ ⊥) ∧ (τ ⊳ τ ′ ) ⇒ (cτ ′ ∈ ⊥ ⊥) It is said to be closed under delimited continuations if whenever c[e/ t p]τ (resp. c[V / ť p]τ ) is in ⊥ ⊥, then µ t p.c ||e τ (resp . V || μ ť p.c τ ) belongs to ⊥ ⊥: (c[e/ t p]τ ∈ ⊥ ⊥) ⇒ ( µ t p.c ||e τ ∈ ⊥ ⊥) (c[V / ť p]τ ∈ ⊥ ⊥) ⇒ ( V || μ ť p.c τ ∈ ⊥ ⊥)
A pole is de ned as any subset of C 0 that is closed by anti-reduction, by store extension and under delimited continuations.

We verify that the set of normalizing command is indeed a pole:

Proposition 4.5. The set ⊥ ⊥ ⇓ = {cτ ∈ C 0 : cτ normalizes } is a pole.

We nally recall the de nition of the orthogonality relation w.r.t. a pole, which is identical to the one for the λ [l τ ⋆] -calculus: De nition 4.6 (Orthogonality). Given a pole ⊥ ⊥, we say that a proof-in-store (p|τ ) is orthogonal to a context-in-store (e |τ ′ ) and write (p|τ )⊥ ⊥(e |τ ′ ) if τ and τ ′ are compatible and p||e ττ ′ ∈ ⊥ ⊥. The orthogonality between terms and co-terms is de ned identically.

We are now equipped to de ne the realizability interpretation of dLPA ω . Firstly, in order to simplify the treatment of coinductive formulas, we extend the language of formulas with second-order variables X , Y , . . . and we replace ν t f x A by ν t X x A[X ( )/f ( ) = 0]. The typing rule for co-xpoint operators then becomes:

Γ ⊢ σ t : T Γ, x : T , b : ∀ T .X ( ) ⊢ σ p : A X FV (Γ) Γ ⊢ σ cofix t b x [p] : ν t X x A (cofix)
where X has to be positive in A.

Secondly, as in the interpretation of dL t p through Lepigre's calculus, we introduce two new predicates, p ∈ A for proofs and t ∈ T for terms. This allows us to decompose the dependent products and sums into:

∀x T .A ∀x.(x ∈ T → A) ∃x T .A ∃x.(x ∈ T → A) Πa : A.B A → B (a FV (B)) Πa : A.B ∀a.(a ∈ A → B) (otw.)
This corresponds to the language of formulas and types de ned by:

Types Formulas Γ ⊢ σ e : A ⊥ ⊥ Γ ⊢ σ e : (q ∈ A) ⊥ ⊥ (∈ p l ) Γ ⊢ σ t : T Γ ⊢ σ t : t ∈ T (∈ t r ) Γ ⊢ σ π : T ⊥ ⊥ Γ ⊢ σ π : (t ∈ T ) ⊥ ⊥ (∈ t l )
These rules are exactly the same as in Lepigre's calculus [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF] up to our strati ed presentation in a sequent calculus fashion, and modulo our syntactic restriction to proofs instead of his semantical restriction. It is a straightforward veri cation to check that the typability is maintained through the decomposition of dependent products and sums.

Another similarity with Lepigre's realizability model is that truth/falsity values will be closed under observational equivalence of proofs and terms. To this purpose, for each store τ we introduce the relation ≡ τ , which we de ne as the re exive-transitive-symmetric closure of the relation ⊲ τ :

t ⊲ τ t ′ whenever ∃τ ′ , ∀π, ( t ||π τ → t ′ ||π τ ′ p ⊲ τ q whenever ∃τ ′ , ∀f ( p|| f τ → q|| f τ ′ ) All this being settled, it only remains to determine how to interpret coinductive formulas. While it would be natural to try to interpret them by xpoints in the semantics, this poses di culties for the proof of adequacy. We discuss this matter in Appendix E,

⊥ f Λ τ f ⊤ f ∅ F (t) f F (t) ∃x.A f t ∈Λ t A[t/x] f ∀x.A f ( t ∈Λ t A[t/x] ⊥ ⊥ f ) ⊥ ⊥ f ∀a.A f ( t ∈Λ p A[p/a] ⊥ ⊥ f ) ⊥ ⊥ f ν t f x A f n ∈N F n A,t f |A| V A ⊥ ⊥ V f A e |A| ⊥ ⊥ e V |N| V t {(S n (0)|τ ), n ∈ N} |t ∈ T | V t {(V t |τ ) ∈ |T | V t : V t ≡ τ t } |T → U | V t {(λx.t |τ ) : ∀V t τ ′ , τ ⋄ τ ′ ∧ (V t |τ ′ ) ∈ |T | V t ⇒ (t[V t /x]|ττ ′ ) ∈ |U | t } t = u f {( μ=.c |τ ) : cτ ∈ ⊥ ⊥} if t ≡ τ u Λ τ f otherwise p ∈ A f {(V |τ ) ∈ |A| V : V ≡ τ p} ⊥ ⊥ f T → B f {(V t • e |τ ) : (V t |τ ) ∈ |t ∈ T | V t ∧ (e |τ ) ∈ B e } A → B f {(V • e |τ ) : (V |τ ) ∈ |A| V ∧ (e |τ ) ∈ B e } T ∧ A f {( μ(x, a).c |τ ) : ∀τ ′ ,V t ∈ |T | τ ′ V t ,V ∈ |A| τ ′ V , τ ⋄ τ ′ ⇒ c[V t /x]ττ ′ [a := V ] ∈ ⊥ ⊥} A 1 ∧ A 2 f {( μ(a 1 , a 2 ).c |τ ) : ∀τ ′ , V 1 ∈ |A 1 | τ ′ V ,V 2 ∈ |A 2 | τ ′ V , τ ⋄ τ ′ ⇒ cττ ′ [a 1 := V 1 ][a 2 := V 2 ] ∈ ⊥ ⊥} A 1 ∨ A 2 f {( μ[a 1 .c 1 |a 2 .c 2 ]|τ ) : ∀τ ′ ,V ∈ |A i | τ ′ V , τ ⋄ τ ′ ⇒ cττ ′ [a i := V ] ∈ ⊥ ⊥} |A| p A ⊥ ⊥ p e |T | π |A| ⊥ ⊥ π V t |T | t |A| ⊥ ⊥ t π
where:

• p ∈ S τ (resp. e,V ,etc.) denotes (p|τ ) ∈ S (resp. (e |τ ), (V |τ ), etc.), • F is a function from Λ t to P(Λ τ f ) /≡ τ .

Figure 5. Realizability interpretation for dLPA ω but as for now, we will give a simpler interpretation. We stick to the intuition that since cofix operators are lazily evaluated, they actually are realizers of every nite approximation of the (possibly in nite) coinductive formula. Consider for instance the case of a stream:

str 0 ∞ p cofix 0 b x [(px, b(S(x)))] of type ν 0 X x A(x) ∧ X (S(x))
. Such stream will produce on demand any tuple (p0, (p1, ...(pn, )...)) where denotes the fact that it could be any term, in particular str n+1 ∞ p. Therefore, str 0 ∞ p should be a successful defender of the formula

(A(0) ∧ (A(1) ∧ ...(A(n) ∧ ⊤)...)
Since cofix operators only reduce when they are bound to a variable in front of a forcing context, it suggests interpreting the coinductive formula ν 0 X x A(x) ∧ X (S(x)) at level f as the union of all the opponents to a nite approximation 10 .

To this end, given a coinductive formula ν 0 X x A where X is positive in A, we de ne its nite approximations by:

F 0 A,t ⊤ F n+1 A,t A[t/x][F n A, /X ( )]
Since X is positive in A, we have for any integer n and any term t that F n A,t f ⊆ F n+1 A,t f . We can nally de ne the interpretation of coinductive formulas by:

ν t X x A f n ∈N F n A,t f
The realizability interpretation of closed formulas and types is de ned in Figure 5 by induction on the structure of formulas at level f , and by orthogonality at levels V , e, p. When S is a subset of P(Λ τ p ) (resp. P(Λ τ e ), P(Λ τ t ), P(Λ τ π )), we use the notation S ⊥ ⊥ f (resp. S ⊥ ⊥ V , etc.) to denote its orthogonal set restricted to Λ τ f :

S ⊥ ⊥ f {(f |τ ) ∈ Λ τ f : ∀(p|τ ′ ) ∈ S, τ ⋄ τ ′ ⇒ p|| f ττ ′ ∈ ⊥ ⊥} At level f , closed
formulas are interpreted by sets of strong forcing contexts-in-store (f |τ ). As explained earlier, these sets are besides closed under the relation ≡ τ along their component τ , we thus denote them by P(Λ τ f ) /≡ τ . Second-order variables X , Y , . . . are then interpreted by functions from the set of terms Λ t to P(Λ τ f ) /≡ τ 10 See Appendix E for a discussion on this point.

and as is usual in Krivine realizability [START_REF] Krivine | Realizability in classical logic[END_REF], for each such function F we add a predicate symbol F in the language.

We shall now prove the adequacy of the interpretation with respect to the type system. To this end, we need to recall a few de nitions and lemmas. Since stores only contain proof terms, we need to de ne valuations for term variables in order to close formulas 11 . These valuations are de ned by the usual grammar:

ρ ::= ε | ρ[x → V t ] | ρ[X → F ]
We denote by (p|τ ) ρ (resp. p ρ , A ρ ) the proof-in-store (p|τ ) where all the variables x ∈ dom(ρ) (resp. X ∈ dom(ρ)) have been substituted by the corresponding term ρ(x) (resp. falsity value ρ(x)).

De nition 4.7. Given a closed store τ , a valuation ρ and a xed pole ⊥ ⊥, we say that the pair (τ , ρ) realizes Γ, which we write 12(τ , ρ) Γ, if:

1. for any (a : A) ∈ Γ, (a|τ

) ρ ∈ |A ρ | V , 2. for any (α : A ⊥ ⊥ ρ ) ∈ Γ, (α |τ ) ρ ∈ A ρ e , 3. for any {a|p} ∈ σ , a ≡ τ p, 4. for any (x : T ) ∈ Γ, x ∈ dom(ρ) and (ρ(x)|τ ) ∈ |T ρ | V t .
We can check that the interpretation is indeed de ned up to the relations ≡ τ : Proposition 4.8. For any store τ and any valuation ρ, the component along τ of the truth and falsity values de ned in Figure 5 are closed under the relation

≡ τ : 1. if (f |τ ) ρ ∈ A ρ f and A ρ ≡ τ B ρ , then (f |τ ) ρ ∈ B ρ f , 2. if (V t |τ ) ρ ∈ |A ρ | V t and A ρ ≡ τ B ρ , then (V t |τ ) ρ ∈ |B ρ | . The same applies with |A ρ | p , A ρ e , etc.
We can now prove the main property of our interpretation: Proposition 4.9 (Adequacy). The typing rules are adequate with respect to the realizability interpretation, i.e. typed proofs (resp. values, terms, contexts, etc.) belong to the corresponding truth values.

Proof. By induction on typing derivations such as given in the system extended for the small-step reduction. See Appendix D.

We can nally deduce that dLPA ω is normalizing and sound. Assume there is such a proof p, by adequacy (p|ε) is in |⊥| p for any pole. Yet, the set ⊥ ⊥ ∅ is a valid pole, and with this pole, |⊥| p = ∅, which is absurd.

Conclusion and perspectives

Conclusion At the end of the day, we met our main objective, namely proving the soundness and the normalization of a language which includes proof terms for dependent and countable choice in a classical setting. This language, which we called dLPA ω , provides us with the same computational features as dPA ω but in a sequent calculus fashion. These computational features allow dLPA ω to internalize the realizability approach of [2,[START_REF] Escardó | Bar recursion and products of selection functions[END_REF] as a direct proofs-asprograms interpretation: both proof terms for countable and dependent choices furnish a lazy witness for the ideal choice function which is evaluated on demand. This interpretation is in line with the slogan that with new programing principles-here the lazy evaluation and the co-inductive objects-come new reasoning principles-here the axioms AC N and DC.

Interestingly, in our search for a proof of normalization for dLPA ω , we developed novel tools to study these side e ects and dependent types in presence of classical logic. On the one hand, we set out in [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF] the di culties related to the de nition of a sequent calculus with dependent types. On the other hand, building on [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF], we developed a variant of Krivine realizability adapted to a lazy calculus where delayed substitutions are stored in an explicit environment. The sound combination of both frameworks led us to the de nition of dLPA ω together with its realizability interpretation.

Krivine's interpretations of dependent choice

The computational content we give to the axiom of dependent choice is pretty di erent of Krivine's usual realizer of the same [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF]. Indeed, our proof uses dependent types to get witnesses of existential formulas, and we represent choice functions through the lazily evaluated stream of their values 13 . In turn, Krivine realizes a statement which is logically equivalent to the axiom of dependent choice thanks to the instruction quote, which injectively associates a natural number to each closed λ c -term. In a more recent work [START_REF] Krivine | Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis[END_REF], Krivine proposes a realizability model which has a bar-recursor and where the axiom of dependent choice is realized using the bar-recursion. This realizability model satis es the continuum hypothesis and many more properties, in particular the real numbers have the same properties as in the ground model. However, the very structure of this model, where Λ is of cardinal ℵ 1 (in particular in nite streams of integer are terms), makes it incompatible with quote.

It is clear that the three approaches are di erent in terms of programming languages. Nonetheless, it could be interesting to compare them from the point of view of the realizability models they give rise to. In particular, our analysis of the interpretation of 13 A similar idea can be found in NuPrl BITT type theory, where choice sequences are used in place of functions [5].

co-inductive formulas14 may suggest that the interest of lazy coxpoints is precisely to approximate the limit situation where Λ has in nite objects.

Reduction of the consistency of classical arithmetic in nite types with dependent choice to the consistency of second-order arithmetic The standard approach to the computational content of classical dependent choice in the classical arithmetic in nite types is via realizability as initiated by Spector [START_REF] Spector | Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics[END_REF] in the context of Gödel's functional interpretation, and later adapted to the context of modi ed realizability by Berardi et al [2]. The aforementioned works of Krivine [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF][START_REF] Krivine | Bar Recursion in Classical Realisability: Dependent Choice and Continuum Hypothesis[END_REF] in the di erent settings of PA2 and ZF ε also give realizers of dependent choice. In all these approaches, the correctness of the realizer, which implies consistency of the system, is itself justi ed by a use at the meta-level of a principle classically equivalent to dependent choice (dependent choice itself in [START_REF] Krivine | Dependent choice, 'quote' and the clock[END_REF], bar induction or update induction [3] in the case of [2,[START_REF] Spector | Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics[END_REF].).

Our approach is here di erent, since we directly interpret proofs of dependent choice in classical arithmetic computationally. Besides, the structure of our realizability interpretation for dLPA ω suggests the de nition of a typed CPS to an extension of system F15 , but it is not clear whether its consistency is itself conservative or not over system F . Ultimately, we would be interested in a computational reduction of the consistency of dPA ω or dLPA ω to the one of PA2, that is to the consistency of second-order arithmetic. While it is well-known that DC is conservative over second-order arithmetic with full comprehension (see [START_REF] Simpson | Subsystems of Second Order Arithmetic[END_REF]Theorem VII.6.20]), it would nevertheless be very interesting to have such a direct computational reduction. The converse direction has been recently studied by Valentin Blot, who presented in [4] a translation of System F into a simply-typed total language with a variant of bar recursion.

A typing derivation in regular mode for the command on the left-hand side is of the shape:

Π V Γ, Γ 0 ⊢ σ σ 0 V : A Π c Γ, Γ 0 , a : A, Γ 1 ⊢ σ σ 0 σ 1 c Π τ 1 Γ, Γ 0 , a : A ⊢ σ σ 0 τ 1 : (Γ 1 ; σ 1 ) Γ, Γ 0 , a : A ⊢ σ σ 0 cτ 1 (l ) Γ, Γ 0 ⊢ σ σ 0 μa.cτ 1 : A ⊥ ⊥ ( μ) Γ, Γ 0 ⊢ σ σ 0 V || μa.cτ 1 (C ) Π τ 0 Γ ⊢ σ τ 0 : (Γ 0 ; σ 0 ) Γ ⊢ σ V || μa.cτ 1 τ 0 (l )
Thus we can type the command on the right-hand side:

Π c Γ, Γ 0 , a : A, Γ 1 ⊢ σ σ 0 {a |V }σ 1 c Γ, Γ 0 , a : A, Γ 1 ⊢ σ σ 0 {a |V }σ 1 c (w ) Π τ 0 Γ ⊢ σ τ 0 : (Γ 0 ; σ 0 ) Π V Γ, Γ 0 ⊢ σ σ 0 V : A Γ ⊢ σ τ 0 [a := V ] : (Γ 0 , a : A; σ 0 , {a |V }) (τp ) Π τ 1 Γ, Γ 0 , a : A ⊢ σ σ 0 τ 1 : (Γ 1 ; σ 1 ) Γ ⊢ σ τ 0 [a := V ]τ 1 : (Γ 0 , a : A, Γ 1 ; σ 0 {a |V }σ 1 ) (τ τ ′ ) Γ ⊢ σ cτ 0 [a := V ]τ 1 (l )
As for the dependent mode, the binding {a|p} within the list of dependencies is compensated when typing the store as shown in the last derivation.

• Similarly, elimination rules for contexts μ[a 1 .c 1 |a 2 .c 2 ], μ(a 1 , a 2 ).c, μ(x, a).c or μ=.c are easy to check, using Lemma A.1 and the rule (τ p ) in dependent mode to prove the safety with respect to dependencies.

• The cases for delimited continuations are identical to the corresponding cases for dL t p .

• The cases for the so-called "call-by-value" rules opening constructors are straightforward, using again Lemma A.1 in dependent mode to prove the consistency with respect to the list of dependencies.

• The cases for the lazy rules are trivial.

• The rst case in the "lookup" section is trivial. The three lefts correspond to the usual unfolding of inductive and co-inductive xpoints. We only sketch the latter in regular mode. The reduction rule is:

a|| f τ 0 [a := cofix t b x [p]]τ 1 → p[t/x][b ′ /b]|| μa. a|| f τ 1 τ 0 [b ′ := λ .cofix b x [p]]
The crucial part of the derivation for the left-hand side command is the derivation for the co x in the store:

Π τ 0 Γ ⊢ σ τ 0 : (Γ 0 ; σ 0 ) Π t Γ ⊢ σ σ 0 t : T Π p Γ, Γ 0 , f : T → N, x : T , b : ∀ T .f ( ) = 0 ⊢ σ σ 0 p : A Γ, Γ 0 ⊢ σ σ 0 cofix t b x [p] : ν t f x A (cofix) Γ ⊢ σ τ 0 [a := cofix t b x [p]] : (Γ 0 , a : ν t f x A; σ 0 ) (τ p )
Then, using this derivation, we can type the store of the right-hand side command:

Π τ 0 Γ ⊢ σ τ 0 : (Γ 0 ; σ 0 ) Γ, Γ 0 , : T ⊢ σ σ 0 : T Π p Γ, Γ 0 , f : T → N, x : T , b : ∀ T .f ( ) = 0 ⊢ σ σ 0 p : A Γ, Γ 0 , : T ⊢ σ σ 0 cofix b x [p] : ν f x A (cofix) Γ, Γ 0 ⊢ σ σ 0 λ .cofix b x [p] : ∀ .ν t f x A (∀ r ) Γ ⊢ σ τ 0 [b ′ := λ .cofix b x [p]] : Γ 0 , b ′ : -∀ .ν f x A (τ p )
It only remains to type (we avoid the rest of the derivation, which is less interesting) the proof p[t/x] with this new store to ensure us that the reduction is safe (since the variable a will still be of type ν t f x A when typing the rest of the command):

Π p Γ, Γ 0 , b : ∀ .ν f x A ⊢ σ p[t/x] : A[t/x][ν f x A/f ( ) = 0] ν t f x A ≡ A[t/x][ν f x A/f ( ) = 0] Γ, Γ 0 , b : ∀ .ν f x A ⊢ σ p[t/x] : ν t f x A (≡ r )
• The cases for reductions of terms are easy. Since terms are reduced in place within proofs, the only things to check is that the reduction of wit preserves types (which is trivial) and that the β-reduction veri es the subject reduction (which is a well-known fact). • Case (∃ r ). We recall the typing rule through the decomposition of dependent sums:

Commands

= e]τ ′ V || μa.cτ ′ e τ s c c τ [a := V ]τ ′ V || f e τ s V || f V τ Values a|| f V τ [a := V ]τ ′ s V || f V τ [a := V ]τ ′ || f V τ s || f f τ (b ′ fresh) a|| f V τ [a = cofix t b x [p]]τ ′ s p[t/x][b ′ /b]|| μa. a||f τ ′ p τ [b ′ := λ .cofix b x [p]] a|| f V τ [a = fix 0 b x [p 0 | p S ]]τ ′ s p 0 || μa. a|| f τ ′ p τ (b ′ fresh) a|| f τ [a = fix S (t ) b x [p 0 | p S ]]τ ′ s p S [t/x][b ′ /b]|| μa. a||f τ ′ p τ [b ′ := fix t b x [p 0 | p S ]
i (V )|| μ[a 1 .c 1 | a 2 .c 2 ] f τ s c i c τ [a i := V ] (V 1 , V 2 )|| μ(a 1 , a 2 ).c f τ s c c τ [a 1 := V 1 ][a 2 := V 2 ] (V t ,V )|| μ(x, a).c f τ s (c[V t /x]) c τ [a := V ] refl|| μ=.c f τ s c c τ Terms tu||π t τ s t ||u • π t τ (x fresh) S(t)||π t τ s t || μx. S(x)||π t (x, a fresh) wit p||π t τ s p|| μ(x, a). x ||π p τ (t V t ) rec t x [t 0 | t S ]||π t τ s t || μz. rec z x [t 0 | t S ]||π t τ rec 0 x [t 0 | t S ]||π t τ s t 0 ||π t τ rec S (V t ) x [t 0 | t S ]||π t τ s t S [V t /x][rec V t x [t 0 | t S ]/ ]||π t τ V t ||π t τ s V t ||π π τ λx.t ||u • π π τ s u || μx. t ||π t τ V t || μx.c t π τ s (c t τ )[V t /x] V t || μx.c π τ s (c p τ )[V t /x]
Γ ⊢ σ t : u ∈ T Γ ⊢ σ p : A[u/x] Γ ⊢ σ (t, p) : (u ∈ T ∧ A[u])
V t || μx. V || μa. (x, a)||e τ 2 s V || μa. (V t , a)||e τ 2 s (V t , a)||e τ 2 [a := V ] It is now easy to check that ((V t , a)|τ 2 [a := V ]) ∈ |u ∈ T ∧ A[u]| V and to conclude, using Lemma D.1 to get (e |τ 2 [a := V ]) ∈ u ∈ T ∧ A[u] e ,
= u f = Λ τ f . • Case (∀ x r
). This case is standard in a call-by-value language with value restriction. We recall the typing rule:

Γ ⊢ σ : A x FV (Γ) Γ ⊢ σ : ∀x.A (∀ x r )
The induction hypothesis gives us that

( |τ ) ρ is in |A ρ | V for any valuation ρ[x → t]. Then for any t, we have ( |τ ) ρ ∈ A ρ [t/x] ⊥ ⊥ f so that ( |τ ) ρ ∈ ( t ∈Λ t A[t/x] ⊥ ⊥ f ). Therefore if (f |τ ′ ) ρ belongs to ∀x.A ρ f = ( t ∈Λ t A[t/x] ⊥ ⊥ f ) ⊥ ⊥ f , we have by de nition that ( |τ ) ρ ⊥ ⊥(f |τ ′ ) ρ .
• Case (fix). We recall the typing rule:

Γ ⊢ σ t : N Γ ⊢ σ p 0 : A[0/x] Γ, x : T , a : A ⊢ σ p S : A[S(x)/x] Γ ⊢ σ fix t ax [p 0 | p S ] : A[t/x] (fix)
We want to show that (fix

= fix b x [p 0 | p S ]]|τ 0 ) is in |t ∈ N| π . Let us then consider (V t |τ ′ 0 ) ∈ |t ∈ N| V t such
that τ 0 and τ ′ 0 are compatible, and let us denote by τ 1 the union τ 0 τ ′ 0 . By de nition, V t = S n (0) for some n ∈ N and t ≡ τ 1 S n (0), and we have:

S n (0)|| μ . a||e [a := fix b x [p 0 | p S ]] τ 1 s a||e τ 1 [a := fix S n (0) b x [p 0 | p S ]]
We conclude by showing by induction on the natural numbers that for any n ∈ N , the value-in-store (a|τ 1 [a := fix

S n (0) b x [p 0 | p S ]]) is in |A[S n (0)]| V . Let us consider (f |τ ′ 1 ) ∈ A[S n (0)] f such that the store τ 1 [a := fix S n (0) b x [p 0 | p S ]
] and τ ′ 1 are compatible, and let us denote by τ 2 [a := fix

S n (0) b x [p 0 | p S ]]τ ′ 2 their union. • If n = 0, we have: a|| f τ 2 [a := fix 0 b x [p 0 | p S ]]τ ′ 2 s p 0 || μa. a|| f τ ′ 2 τ 2
We conclude by anti-reduction and the induction hypothesis for p 0 , since it is easy to show that ( μa. a||f τ

′ 2 |τ 2 ) ∈ A[0] e . • If n = S(m), we have: a||f τ 2 [a := fix S (S m (0)) b x [p 0 | p S ]]τ ′ 2 s p S [S m (0)/x][b ′ /b]|| μa. a|| f τ ′ 2 p τ 2 [b ′ := fix S m (0) b x [p 0 | p S ]]
Since we have by induction that

(b ′ |τ 2 [b ′ := fix S m (0) b x [p 0 | p S ]]) is in |A[S m (0)]| V ,
we can conclude by anti-reduction, using the induction hypothesis for p S and the fact that ( μa. a|| f τ ′ 2 |τ 2 ) belongs to A[S(S m (0))] e .

• Case (cofix). We recall the typing rule:

Γ ⊢ σ t : T Γ, x : T , b : ∀ T .X ( ) ⊢ σ p : A X positive in A X FV (Γ) Γ ⊢ σ cofix t b x [p] : ν t X x A (cofix)
We want to show that (cofix

= cofix b x [p]]|τ 0 ) is in |t ∈ N| π . Let us then consider (V t |τ ′ 0 ) ∈ |t ∈ T | V t such
that τ 0 and τ ′ 0 are compatible, and let us denote by τ 2 the union τ 0 τ ′ 0 . We have:

V t || μ . a||e [a := cofix b x [p]] τ 1 s a||e τ 1 [a := cofix V t b x [p]] It su ces to show now that the value-in store (a|τ 1 [a := cofix V t b x [p]]) is in |ν V t X x A| V .
By de nition, we have:

|ν V t X x A| V = ( n ∈N F n A,V t f ) ⊥ ⊥ V = n ∈N F n A,V t ⊥ ⊥ V f = n ∈N |F n A,V t | V
We conclude by showing by induction on the natural numbers that for any n ∈ N and any V t , the value-in-store (a|τ A,V t e , which is trivial from the hypothesis for f . Theorem 4.11 (Consistency). dLPA ω p : ⊥ Proof. Assume there is such a proof p, by adequacy (p|ε) is in |⊥| p for any pole. Yet, the set ⊥ ⊥ ∅ is a valid pole, and with this pole, |⊥| p = ∅, which is absurd.

1 [a := cofix V t b x [p]]) is in |F n A,V t | V . The case n = 0 is trivial since |F 0 A,V t | V = |⊤| V = Λ τ V .

E About the interpretation of coinductive formulas

While our realizability interpretation give us a proof of normalization and soundness for dLPA ω , it has two aspects that we should discuss. First, regarding the small-step reduction system, one could have expected the lowest level of interpretation to be instead of f . Moreover, if we observe our de nition, we notice that most of the cases of • f are in fact de ned by orthogonality to a subset of strong values. Indeed, except for coinductive formulas, we could indeed have de ned instead an interpretation If this de nition is somewhat more natural, it poses a problem for the de nition of coinductive formulas. Indeed, there is a priori no strong value in the orthogonal of ν t f A f , which is:

: ∀V τ ′ , τ ⋄ τ ′ ∧ (V |τ ′ ) ∈ |A| V ⇒ (p|ττ ′ [a := V ]) ∈ |B| p } |T ∧ A| {((V t ,V )|τ ) : (V t |τ ) ∈ |T | V t ∧ (V |τ ) ∈ |A 2 | V } |A 1 ∧ A 2 | {((V 1 , V 2 )|τ ) : (V 1 |τ ) ∈ |A 1 | V ∧ (V 2 |τ ) ∈ |A 2 | V } |A 1 ∨ A 2 | {(ι i (V )
( ν t f A f ) ⊥ ⊥ = ( n ∈N F n A,t f ) ⊥ ⊥ = n ∈N ( F n A,t f ) ⊥ ⊥ )
For instance, consider again the case of a stream of type ν 0 f x A(x) ∧ f (S(x)) = 0, a strong value in the intersection should be in every |A(0) ∧ (A(1) ∧ . . . (A(n) ∧ ⊤) . . . )| , which is not possible due to the niteness of terms 17 . Thus, the de nition |ν t f A| n ∈N |F n A,t | would give |ν t f x A| = ∅ = |⊥| . Interestingly, and this is the second aspect that we shall discuss here, we could have de ned instead the truth value of coinductive formulas directly by :

|ν t f x A| |A[t/x][ν f x A/f ( ) = 0]|
Let us sketch the proof that such a de nition is well-founded. We consider the language of formulas without coinductive formulas and extended with formulas of the shape X (t) where X , Y , ... are parameters. At level , closed formulas are interpreted by sets of strong valuesin-store ( |τ ), and as we already observed, these sets are besides closed under the relation ≡ τ along their component τ . If A(x) is a formula whose only free variable is x, the function which associates to each term t the set |A(t)| is thus a function from Λ t to P(Λ τ ) ≡ τ , let us denote the set of these functions by L .

Proposition E.1. The set L is a complete lattice with respect to the order ≤ L de ned by: F ≤ L G ∀t ∈ Λ t .F (t) ⊆ G(t)

Proof. Trivial since the order on functions is de ned pointwise and the co-domain P(Λ τ ) is itself a complete lattice.

We de ne valuations, which we write ρ, as functions mapping each parameter X to a function ρ(X ) ∈ L . We then de ne the interpretations |A| ρ , A ρ f , ... of formulas with parameters exactly as above with the additional rule 18 :

|X (t)| ρ {( |τ ) ∈ ρ(X )(t)}
Let us x a formula A which has one free variable x and a parameter X such that sub-formulas of the shape X t only occur in positive positions in A.

Lemma E.2. Let B(x) is a formula without parameters whose only free variable is x, and let ρ be a valuation which maps X to the function t → |B(t)| . Then |A| ρ = |A[B(t)/X (t)]| 17 Yet, it might possible to consider interpretation with in nite proof terms, the proof of adequacy for proofs and contexts (which are nite) will still work exactly the same. However, another problem will arise for the adequacy of the cofix operator. Indeed, with the interpretation above, we would obtain the inclusion:

n∈N ( F n A, t f ) ⊂ ( n∈N |F n A, t | t ) ⊥ ⊥ f = ν t f x
A f which is strict in general. By orthogonality, this gives us that |ν t f x A | V ⊆ n∈N ( F n A, t f )) ⊥ ⊥ V , while the proof of adequacy only proves that (a |τ [a := cofix t b [x ]p]) belongs to the latter set. 18 Observe that this rule is exactly the same as in the previous section (see Figure 5).

Figure 1 .

 1 Figure 1. The language of dLPA ω

Figure 2 .

 2 Figure 2. Reduction rules of dLPA ω

Figure 4 .

 4 Figure 4. Typing rules of dPA ω

Theorem 4 . 10 (

 410 Normalization). If Γ ⊢ σ c, then c is normalizable.Proof. Direct consequence of Propositions 4.5 and 4.9. Theorem 4.11 (Consistency). dLPA ω p : ⊥ Proof.

Figure 7 .

 7 Figure 7. Small-step reduction rules

2 s

 2 p[V t /x][b ′ /b]|| μa. a|| f τ ′ 2 τ 2 [b ′ := λ .cofix b x [p]] It is straightforward to check, using the induction hypothesis for n, that (b ′ |τ 2 [b ′ := λ .cofix b x [p]]) is in |∀ . ∈ T → F n A, | V .Thus we deduce by induction hypothesis for p, denoting by S the function t → F n A,t f , that:(p[V t /x][b ′ /b]|τ 2 [b ′ := λ .cofix b x [p]]) ∈ |A[V t /x][ S/X ]| p = |A[V t /x][F n A, /X ( )]| p = |F n+1 A,V t | p It only remains to show that ( μa. a|| f τ ′ 2 |τ 2 ) ∈ F n+1

  ||e τ → µ t p.c ||e τ ′ µα .c ||e t p τ → c[e t p /α]τ µ t p. p|| t p ||e τ → p||e τ

	Call-by-value
	(a fresh)	ι i (p)||e τ → p|| μa. ι i (a)||e τ
	(a 1 , a 2 fresh)	(p 1 , p 2 )||e τ → p 1 || μa 1 . p 2 || μa 2 . (a 1 , a 2 )||e τ
	(a fresh)	(V t , p)||e τ → p|| μa. (V t , a)||e τ

  a 1 , a 2 ). q||α p case p of [a 1 .p 1 | a 2 .p 2 ] µα p . p|| μ[a 1 . p 1 ||α p |a 2 . p 2 ||α p ] dest p as (a, x) in q µα

p . p|| μ(x, a). q||α p prf p µ t p. p|| μ(x, a). a|| t p subst p q µα . p|| μ=. q||α exfalso p µα . p||[] catch α p µα . p||α throw α p µ_. p||α where α p = t p if p is and α p = α otherwise. It is then straightforward to check that the macros match the expected typing rules: Proposition 2.3 (Natural deduction). The typing rules from dPA ω , given in Figure

  p||e c τ s p||e p t ||π c τ s t ||π t Delimited continuations (for any ι, o) µ t p.cτ ′′ ||e p τ s µ t p.c ′ τ ′′ ||e p τ ′ (if c ι τ s c ′ o τ ′ ) µ t p. p|| t p ||e p τ s p||e p τ (for any ι, o)V || μ ť p.c e τ s V || μ ť p.c ′ e τ ′ (if c ι τ s c ′ o τ ′ ) V || μ ť p. ť p||e e τ s V||e e τ Proofs (e e t p ) µα .c ||e p τ s c c τ [α := e] µα .c ||e t p p τ s c c [e t p /α] τ (a fresh) (p 1 , p 2 )||e p τ s p 1 || μa 1 . p 2 || μa 2 . (a 1 , a 2 )||e p τ (a fresh) ι i (p)||e p τ s p|| μa. ι i (a)||e p τ (a fresh) (t, p)||e p τ s p|| μ ť p. t || μx. ť p|| μa. (x, a)||e p τ ( , a fresh) fix t b x [p | q]||e p τ s µ t p. t || μ . a|| t p [a := fix b x [p | q]] ||e p τ ( , a fresh) cofix t b x [p]||e p τ s µ t p. t || μ . a|| t p [a := cofix b x [p]]||e p τ V ||e p τ s V ||e e Contexts V ||α e τ [α := e]τ ′ s V ||e e τ [α :

  ]] Forcing contexts λx.p||t • e f τ s µ t p. t || μx. p|| t p ||e p τ (q ∈ ) λa.p||q • e f τ s µ t p. q|| μa. p|| t p ||e p τ (q ) λa.p||q • e f τ s q|| μa. p||e p τ ι

  By induction hypothesis, we obtain that (t |τ ) ∈ |u ∈ T | t and (p|τ ) ∈ |A[u]| p . Consider thus any context-in-store (e |τ ′ ) ∈ u ∈ T ∧ A[u] e such that τ and τ ′ are compatible, and let us denote by τ 0 the union ττ ′ . We have: (t, p)||e p τ 0 s p|| μ ť p. t || μx. ť p|| μa. (x, a)||e p τ 0 so that by anti-reduction, we need to show that μ ť p. t || μx. ť p|| μa. (x, a)||e ∈ A[u] e . Let us then consider a value-in-store (V |τ ′ 0 ) ∈ |A[u]| V such that τ 0 and τ ′ 0 are compatible, and let us denote by τ 1 the union τ 0 τ ′ 0 . By closure under delimited continuations, to show that V || μ ť p. t || μx. ť p|| μa. (x, a)||e p τ 1 is in the pole it is enough to show that the closure t || μx. V || μa. (x, a)||e τ 1 is in ⊥ ⊥,. Thus it su ces to show that the coterm-in-store ( μx. V || μa. (x, a)||e |τ 1 ) is in |u ∈ T | π .Consider a term value-in-store (V t |τ ′ 1 ) ∈ |u ∈ T | V t , such that τ 1 and τ ′ 1 are compatible, and let us denote by τ 2 the union τ 1 τ ′ 1 . We have:

  that this closure is nally in the pole.• Case (≡ r ),(≡ l ). These cases are direct consequences of Proposition 4.8 since if A, B are two formulas such that A ≡ B, in particular A ≡ τ B and thus |A| = |B| .• Case (refl),(= l ). The case for refl is trivial, while it is trivial to show that( μ=. p||e |τ ) is in t = u f if (p|τ ) ∈|A[t]| p and (e |τ ) ∈ A[u] e . Indeed, either t ≡ τ u and thus A[t] ≡ τ A[u] (Proposition 4.8, or t τ u and t

  ′ are compatible, and let us denote by τ 0 the union ττ ′ . By induction hypothesis, we have 16 t ∈ |t ∈ N| t and we have: S ]] ||e p τ 0 so that by anti-reduction and closure under delimited continuations, it is enough to show that the coterm-in-store ( μ . a||e [a :

	fix t b x [p 0 | p

t ax [p 0 | p S ]|τ ) ∈ |A[t]| p , let us then consider (e |τ ′ ) ∈ A[t] e such that τ and τ S ]||e p τ 0 s µ t p. t || μ . a|| t p [a := fix b x [p 0 | p

  t b x [p]|τ ) ∈ |ν t X x A| p , let us then consider (e |τ ′ ) ∈ ν t X x A e such that τ and τ ′ are compatible, and let us denote by τ 0 the union ττ ′ . By induction hypothesis, we have t ∈ |t ∈ T | t and we have: cofix t b x [p]||e p τ 0 s µ t p. t || μ . a|| t p [a := cofix b x [p]] ||e p τ 0 so that by anti-reduction and closure under delimited continuations, it is enough to show that the coterm-in-store ( μ . a||e [a :

  Let then n be an integer and any V t be a term value. Let us consider(f |τ ′ 1 ) ∈ F n+1 A,V t A f such that τ 1 [a := cofix V t b x [p]] andτ ′ 1 are compatible, and let us denote by τ 2 [a := cofix V t b x [p]]τ ′ 2 their union. By de nition, we have: a|| f τ 2 [a := cofix V t b x [p]]τ ′

  | • | of formulas at level and then the interpretation • f by orthogonality: A| {( |τ ) ∈ |A| : ≡ τ p} |T → B| {(λx.p|τ ): ∀V t τ ′ , τ ⋄ τ ′ ∧ (V t |τ ′ ) ∈ |T | V ⇒ (p[V t /x]|ττ ′ ) ∈ |B| p } |A → B| {(λa.p|τ )

	|⊥|	∅
	|t = u |	refl if t ≡ u ∅ otherwise
	|p ∈

  |τ ) : (V |τ ) ∈ |A i | V } |∃x.A| t ∈Λ t |A[t/x]| |∀x.A| t ∈Λ t |A[t/x]| |∀a.A| p ∈Λ p |A[p/x]| A f {(f |τ ) : ∀ τ ′ , τ ⋄ τ ′ ∧ ( |τ ′ ) ∈ |A| ⇒ ( |τ ′ )⊥ ⊥(F |τ )}

That is to say reduction rules in an abstract machine for which only the term or the context needs to be analyzed in order to decide whether the rule can be applied.

See[START_REF] Miquey | A classical sequent calculus with dependent types[END_REF] for further details.

To highlight the duality between inductive and coinductive xpoints, we evaluate both in a lazy way. Even though this is not indispensable for inductive xpoints, we nd this approach more natural in that we can treat both in a similar way in the small-step reduction system and thus through the realizability interpretation.

Our so-called stores somewhat behave like lazy explicit substitutions or mutable environments. See[START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF] for a discussion on this point.

For terms, proofs, contexts, commands, closures and stores.

For contexts, commands and closures.

On the contrary, the reduced command in dL t p would have been p[V /a]||e , which is typable with the (C ) rule over the formula B[V /a].

(A r ) (α : A ⊥ ⊥ ) ∈ Γ Γ ⊢ σ α : A ⊥ ⊥ (A l ) Γ, α : A ⊥ ⊥ ⊢ σ c Γ ⊢ σ µα .c : A (µ ) Γ ⊢ σ τ : (Γ ′ ; σ ′ ) Γ, Γ ′ ⊢ σ σ ′ α : A ⊥ ⊥ Γ ⊢ σ τ [α := e] : (Γ ′ , α : A ⊥ ⊥ ; σ ′ ) (τ e ) Γ, a : A ⊢ σ cτ Γ ⊢ σ μa.cτ : A ⊥ ⊥ ( μ) Γ ⊢ σ p 1 : A Γ ⊢ σ p 2 : B Γ ⊢ σ (p 1 , p 2 ) : A ∧ B (∧ r ) Γ, a 1 : A 1 , a 2 : A 2 ⊢ σ c Γ ⊢ σ μ(a 1 , a 2 ).c : (A 1 ∧ A 2 ) ⊥ ⊥ (∧ l ) Γ ⊢ σ p : A i Γ ⊢ σ ι i (p) : A 1 ∨ A 2 (∨ r ) Γ, a 1 : A 1 ⊢ σ c 1 Γ, a 2 : A 2 ⊢ σ c 2 Γ ⊢ σ μ[a 1 .c 1 | a 2 .c 2 ] : (A 1 ∨ A 2 ) ⊥ ⊥ (∨ l ) Γ ⊢ σ p : A[t/x] Γ ⊢ σ t : T Γ ⊢ σ (t, p) : ∃x T .A (∃ r ) Γ, x : T , a : A ⊢ σ c Γ ⊢ σ μ(x, a).c : (∃x T .A) ⊥ ⊥ (∃ l ) Γ, x : T ⊢ σ p : A Γ ⊢ σ λx.p : ∀x T .A (∀ r ) Γ ⊢ σ t : T Γ ⊢ σ e : A[t/x] ⊥ ⊥ Γ ⊢ σ t • e : (∀x T .A) ⊥ ⊥ (∀ l ) Γ ⊢ σ t : N Γ ⊢ σ refl : t = t refl Γ ⊢ σ p : A Γ ⊢ σ e : A[u/t] Γ ⊢ σ μ=. p||e : (t = u) ⊥ ⊥ (= l ) Γ, a : A ⊢ σ p : B Γ ⊢ σ λa.p : Πa : A.B (→ r ) Γ ⊢ σ q : A Γ ⊢ σ e : B[q/a] ⊥ ⊥ if q then a A Γ ⊢ σ q • e : (Πa : A.B) ⊥ ⊥ (→ l ) Γ ⊢ σ p : A A ≡ B Γ ⊢ σ p : B (≡ r ) Γ ⊢ σ e : A ⊥ ⊥ A ≡ B Γ ⊢ σ e : B ⊥ ⊥ (≡ l ) Γ ⊢ σ t : N Γ ⊢ σ p 0 : A[0/x] Γ, x : T , a : A ⊢ σ p S : A[S(x)/x] Γ ⊢ σ fix t ax [p 0 | p S ] : A[t/x] (fix) Γ ⊢ σ [] : ⊥ ⊥ ⊥ ⊥ Γ ⊢ σ t : T Γ, f : T → N, x : T , b : ∀ T .f ( ) = 0 ⊢ σ p : A f positive in A Γ ⊢ σ cofix t b x [p] : ν t f x A (cofix)

( μd ) Γ, x : T , a : A ⊢ d c t p ; σ {(x, a)|p N } Γ ⊢ d μ(x, a).c t p : (∃x T A) ⊥ ⊥ ; σ {•|p N } (∃ d l ) Γ, a 1 : A 1 , a 2 : A 2 ⊢ d c t p ; σ {(a 1 , a 2 )|p N } Γ ⊢ d μ(a 1 , a 2 ).c t p : (A 1 ∧ A 2 ) ⊥ ⊥ ; σ {•|p N } (∧ d l )Terms Γ ⊢ σ 0 :N (0) Γ ⊢ σ t : N Γ ⊢ σ S(t) : N (S ) (x : T ) ∈ Γ Γ ⊢ σ x : T (A t ) Γ, x : U ⊢ σ t : T Γ ⊢ σ λx.t : U → T (λ) Γ ⊢ σ t : U → T Γ ⊢ σ u : U Γ ⊢ σ t u : T (@) Γ ⊢ σ t : N Γ ⊢ σ t 0 : U Γ, x : N, : U ⊢ σ t S : U Γ ⊢ σ rec t x [t 0 | t S ] : U (rec)

σ ⇛ σ ′ σ (A) = σ (B) ⇒ σ ′ (A) = σ ′ (B) (for any A, B)Proposition 2.1 (Dependencies weakening). If σ, σ ′ are two lists of dependencies such that σ ⇛ σ ′ , then any derivation using σ can be done using σ ′ instead. In other words, the following rules are admissible:Γ ⊢ σ Γ ⊢ σ ′ (w ) Γ ⊢ d ; σ Γ ⊢ d ; σ ′ (w d )We can prove the safety of reduction with respect to typing:Theorem 2.2 (Subject reduction). For any context Γ and any closures cτ and c ′ τ ′ such that cτ → c ′ τ ′ , we have:1. If Γ ⊢ cτ then Γ ⊢ c ′ τ ′ . 2. If Γ ⊢ d cτ ; ε then Γ ⊢ d c ′ τ ′ ; ε.Proof. The proof follows the usual proof of subject reduction, by induction on the reduction cτ → c ′ τ ′ . See Appendix A.

T , U ::= N | T → U | t ∈ T A, B ::= ⊤ | ⊥ | X (t) | t = u | A ∧ B | A ∨ B | ∀x.A | ∃x.A | ∀a.A | ν t X x A | a ∈A and to the following inference rules:Γ ⊢ σ : A a FV (Γ) Γ ⊢ σ : ∀a.A (∀ a r ) Γ ⊢ σ e : A[q/a] q Γ ⊢ σ e : (∀a.A) ⊥ ⊥ (∀ a l ) Γ ⊢ σ : A x FV (Γ) Γ ⊢ σ : ∀x.A (∀ x r ) Γ ⊢ σ e : A[t/x] Γ ⊢ σ e : (∀x.A) ⊥ ⊥ (∀ x l ) Γ ⊢ σ : A[t/x] Γ ⊢ σ : ∃x.A (∃ x r ) Γ ⊢ σ e : A x FV (Γ) Γ ⊢ σ e : (∃x.A) ⊥ ⊥ (∃ x l ) Γ ⊢ σ p : A p Γ ⊢ σ p : p ∈ A (∈ p r )

Alternatively, we could have modi ed the small-step reduction rules to include substitutions of terms.

[START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF] Once again, we should formally write (τ , ρ ) ⊥ ⊥ Γ but we will omit the annotation by ⊥ ⊥ as often as possible.

See also Appendix E.

See[START_REF] Miquey | Classical realizability and side-e ects[END_REF] Chapitre 8] for further details.

Proof. The proof is done by induction on the typing derivation such as given in the system extended with the small-step reduction s . Most of the cases correspond to the proof of adequacy for the interpretation of the λ [l τ ⋆] -calculus, so that we only give the most interesting cases. To lighten the notations, we omit the annotation by the valuation ρ whenever it is possible.

Recall that any term t of type T can be given the type t ∈ T .

Acknowledgments

The author warmly thanks Hugo Herbelin for numerous discussions and attentive reading of this work during his PhD years.

Since most of the proofs contain typing derivations, we switch to a one column format to ease their display.

A Subject reduction (Proofs of Section 2.4)

We detail here the proof of subject reduction for dLPA ω . Recall that we de ne the relation σ ⇛ σ ′ between lists of dependencies by:

We rst show that the cases which we encounter in the proof of subject reduction satisfy this relation:

Lemma A.1 (Dependencies implication). The following holds for any σ, σ ′ , σ ′′ :

where the fourth item abuse the de nition of list of dependencies to include a substitution of terms.

Proof. All the properties are trivial from the de nition of the substitution σ (A).

We can now prove that the relation ⇛ indeed matches the expected intuition:

Proposition 2.1 (Dependencies weakening). If σ, σ ′ are two dependencies list such that σ ⇛ σ ′ , then any derivation using σ can be one using σ ′ instead. In other words, the following rules are admissible:

Proof. Simple induction on the typing derivations. The rules ( t p) and (C ) where the list of dependencies is used exactly match the de nition of ⇛. Every other case is direct using the rst item of Lemma A.1.

In addition to the previous proposition, we need the following extra lemma to simplify the proof of subject reduction, which we will use when concatenating two stores: Lemma A.2. The following rule is admissible:

Proof. By induction on the structure of τ 1 .

Finally, we need to prove that substitutions of terms are safe with respect to typing (recall that substitutions of proofs are handled through the typing rules for stores):

Lemma A.3. [Safe term substitution] If Γ ⊢ σ t : T then for any conclusion for typing proofs, contexts, terms, etc; the following holds:

Proof. By induction on typing rules.

We are now equipped to prove the expected property:

Theorem 2.2. For any context Γ and any closures cτ and c ′ τ ′ such that cτ → c ′ τ ′ , we have:

Proof. The proof follows the usual proof of subject reduction, by induction on the typing derivation and the reduction cτ → c ′ τ ′ . Since there is no substitution but for terms (proof terms and contexts being stored), there is no need for auxiliary lemmas about the safety of substitution. We sketch it by examining all the rules from Figure 3 from top to bottom.

• The cases for reductions of λ are identical to the cases proven in the previous chapter for dL t p .

• The rules for reducing µ and μ are almost the same except that elements are stored, which makes it even easier. For instance in the case of μ, the reduction rule is:

B Natural deduction as macros (Proofs of Section 2.5)

We give here two examples of typing rules for the macros subst p q and prf pq (in natural deduction) that are admissible in dLPA ω . Recall that we have the following typing rules in dLPA ω :

and that we de ned prf p and subst p q as syntactic sugar:

prf p µ t p. p|| μ(x, a). a|| t p subst p q µα . p|| μ=. q||α . Observe that prf p is now only de nable if p is a proof term. For any p ∈ and any variables a, α, we can prove the admissibility of the (prf )-rule:

Γ ⊢ σ µ t p. p|| μ(x, a). a|| t p : A(wit p) | ∆ Similarly, we can prove that the (subst)-rule is admissible:

. Theorem 2.4 (Countable choice [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]). We have:

where

Proof. The complete typing derivation of the proof term for AC N from Herbelin's paper [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF] is given in Figure 6.

Theorem 2.5 (Dependent choice [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]). We have:

Left to the reader.

Notations:

Typing derivation for nth (Π nth ):

Typing derivation for str 0 ∞ (Π str ∞ ):

Typing derivation for AC N :

a : A 0 ∞ , n : N ⊢ wit (nth n a) : where we omit the conversion P(x, (λn. wit (nth n a))x) ≡ P(x, wit (nth x a)) on the right-hand side derivation. We give in Figure 7 the full reduction system based on small-step reduction rules which are described in Section 3. We detail thereafter the proofs of the two main properties of the small-step reduction system.

Proposition 3.1 (Subject Reduction). The small-step reduction rules satisfy subject reduction.

Proof. The proof is again a tedious induction on the reduction s . There is almost nothing new in comparison with the cases for the big-step reduction rules: the cases for reduction of terms are straightforward, as well as the administrative reductions changing the focus on a command. We only give the case for the reduction of pairs (t, p). The reduction rule is:

(t, p)||e p τ s p|| μ ť p. t || μx. ť p|| μa. (x, a)||e p τ Consider a typing derivation for the command on the left-hand side, which is of the shape (we omit the rule (l) and the store for conciseness):

Then we can type the command on the right-hand side with the following derivation:

where Π (x, a) is as expected.

Proposition 3.2. If a closure cτ normalizes for the reduction s , then it normalizes for →.

Proof. By contraposition, one proves that if a command cτ produces an in nite number of steps for the reduction →, then it does not normalize for s either. This is proved by showing by induction on the reduction → that each step, except for the contextual reduction of terms, is re ected in at least on for the reduction s . The rules for term reductions require a separate treatment, which is really not interesting at this point. We claim that the reduction of terms, which are usual simply-typed λ-terms, is known to be normalizing anyway and does not deserve that we spend another page proving it in this particular setting.

D Realizability interpretation (Proofs of Section 4)

We give here the di erent proofs relative to the realizability interpretation of dLPA ω . First, we verify that the set of normalizing closures is indeed a pole:

Proposition 4.5. The set ⊥ ⊥ ⇓ = {cτ ∈ C 0 : cτ normalizes } is a pole.

Proof. The rst two conditions are already veri ed for the λ [l τ ⋆] -calculus [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF]. The third one is straightforward, since if a closure µ t p.c ||e τ is not normalizing, it is easy to verify that c[e/ t p] is not normalizing either. Roughly, there is only two possible reduction steps for a command µ t p.c ||e τ : either it reduces to µ t p.c ′ ||e τ ′ , in which case c[e/ t p]τ also reduces to a closure which is almost (c ′ τ ′ )[e/ t p]; or c is of the shape p|| t p and it reduces to c[e/ t p]τ . In both cases, if µ t p.c ||e τ can reduce, so can c[e/ t p]τ . The same reasoning allows us to show that if c[V / ť p]τ normalizes, then so does V || μ ť p.c τ for any value V .

We recall two key properties of the interpretation, whose proofs are similar to the proofs for the corresponding statements in the λ [l τ ⋆]calculus [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF]: Lemma D.1 (Store weakening). Let τ and τ ′ be two stores such that τ ⊳ τ ′ , let Γ be a typing context, let ⊥ ⊥ be a pole and ρ a valuation. The following statements hold:

Proposition D.2 (Monotonicity). For any closed formula A, any type T and any given pole ⊥ ⊥, we have the following inclusions:

Truth and falsity values are de ned up to observational equivalence: Proof. By induction on the structure of A, all cases are trivial, and this is true for the basic case A ≡ X (t):

Let us now de ne φ A as the following function:

Proposition E.3. The function φ A is monotone.

Proof. By induction on the structure of A, where X can only occur in positive positions. The case |X (t)| is trivial, and it is easy to check that truth values are monotonic with respect to the interpretation of formulas in positive positions, while falsity values are anti-monotonic.

We can thus apply Knaster-Tarski theorem to φ A , and we denote by gfp(φ A ) its greatest xpoint. We can now de ne:

This de nition satis es the expected equality: Proposition E.4. We have:

Observe rst that by de nition, the formula B(z) = |ν z X x A| satis es the hypotheses of Lemma E.2 and that gfp(φ A ) = t → B(t). Then we can deduce :

Back to the original language, it only remains to de ne |ν t f x A| as the set |ν t X x A[X ( )/f ( ) = 0]| that we just de ned. This concludes our proof that the interpretation of coinductive formulas through the equation in Proposition E.4 is well-founded.

We could also have done the same reasoning with the interpretation from the previous section, by de ning L as the set of functions from Λ t to P(Λ τ f ) ≡ τ . The function φ A , which is again monotonic, is then:

We recognize here the de nition of the formula F n A,t . De ning f 0 as the function t → ⊤ f and f n+1 φ A (f n ) we have:

However, in both cases (de ning primitively the interpretation at level or f ), this de nition does not allow us to prove 19 the adequacy of the (cofix) rule. In the case of an interpretation de ned at level f , the best that we can do is to show that for any n ∈ N, f n is a post-xpoint since for any term t, we have:

A f de ned as the greatest xpoint of φ A , for any term t and any n ∈ N we have the inclusion f n (t) ⊆ gfp(φ A )(t) = ν t f x A f and thus:

By orthogonality, we get:

and thus our proof of adequacy from the last section is not enough to conclude that cofix t b x [p] ∈ |ν t f x A| p . For this, we would need to prove that the inclusion is an equality. An alternative to this would be to show that the function t → n ∈N F n A,t f is a xpoint for φ A . In that case, we could stick to this de nition and happily conclude that it satis es the equation:

This would be the case if the function φ A was Scott-continuous on L (which is a dcpo), since we could then apply Kleene xed-point theorem 20 to prove that t → n ∈N F n A,t f is the stationary limit of φ n A (f 0 ). However, φ A is not Scott-continuous 21 (the de nition of falsity values involves double-orthogonal sets which do not preserve supremums), and this does not apply. 19 To be honest, we should rather say that we could not manage to nd a proof, and that we would welcome any suggestion from insightful readers. 20 In fact, Cousot and Cousot proved a constructive version of Kleene xed-point theorem which states that without any continuity requirement, the trans nite sequence (φ α A (f 0 )) α ∈On is stationary [6]. Yet, we doubt that the gain of the desired equality is worth a trans nite de nition of the realizability interpretation. 21 In fact, this is nonetheless a good news about our interpretation. Indeed, it is well-know that the more "regular" a model is, the less interesting it is. For instance, Streicher showed that the realizability model induced by Scott domains (using it as a realizability structure) was not only a forcing model by also equivalent to the ground model.