Étienne Miquey

A Classical Sequent Calculus with Dependent Types

Dependent types are a key feature of the proof assistants based on the Curry-Howard isomorphism. It is well-known that this correspondence can be extended to classical logic by enriching the language of proofs with control operators. However, they are known to misbehave in the presence of dependent types, unless dependencies are restricted to values. Moreover, while sequent calculi naturally support continuation-passing style interpretations, there is no such presentation of a language with dependent types. The main achievement of this paper is to give a sequent calculus presentation of a call-by-value language with a control operator and dependent types, and to justify its soundness through a continuation-passing style translation.

We start from the call-by-value version of the λµ μ-calculus. We design a minimal language with a value restriction and a type system that includes a list of explicit dependencies to maintains type safety. We then show how to relax the value restriction and introduce delimited continuations to directly prove the consistency by means of a continuation-passing-style translation. Finally, we relate our calculus to a similar system by Lepigre, and present a methodology to transfer properties from this system to our own.

INTRODUCTION

Control operators and dependent types

Originally created to deepen the connection between programming and logic, dependent types are now a key feature of numerous functional programming languages. From the point of view of programming, dependent types provide more precise types-and thus more precise specifications-to existing programs. From a logical perspective, they permit definitions of proof terms for statements like the full axiom of choice. Dependent types are provided by Coq or Agda, two of the most actively developed proof assistants. They both rely on constructive type theories: the calculus of inductive constructions for Coq [START_REF] Coquand | Inductively defined types[END_REF], and Martin-Löf's type theory for Agda [START_REF] Martin-Löf | Constructive mathematics and computer programming[END_REF]. Yet, both systems lack support for classical logic and more generally for side effects, which make them impractical as programming languages.

In practice, effectful languages give the programmer a more explicit access to low-level control (that is: to the way the program is executed on the available hardware), and make some algorithms easier to implement. Common effects, such as the explicit manipulation of the memory, the generation of random numbers and input/output facilities are available in most practical programming languages (e.g., OCaml, C++, Python, Java).

In 1990, Griffin discovered that the control operator call/cc (short for call with current continuation) could be typed by Peirce's law ((A→ B) →A) →A) [START_REF] Griffin | A formulae-as-type notion of control[END_REF], thus extending the formulas-as-types interpretation. Indeed, Peirce's law is known to imply, in an intuitionistic framework, all the other forms of classical reasoning (excluded middle, reductio ad absurdum, double negation elimination, etc.). This discovery opened the way for a direct computational interpretation of classical proofs, using control operators and their ability to backtrack. Several calculi were born from this idea, for example Parigot's λµ-calculus [START_REF] Parigot | Proofs of strong normalisation for second order classical natural deduction[END_REF], Barbanera and Berardi's symmetric λ-calculus [START_REF] Barbanera | A symmetric lambda calculus for classical program extraction[END_REF], Krivine's λ c -calculus [START_REF] Krivine | Realizability in classical logic. In interactive models of computation and program behaviour[END_REF], Curien and Herbelin's λµ μ-calculus [START_REF] Curien | The duality of computation[END_REF]. c b n a This work is licensed under a Creative Commons Attribution-ShareAlike 3.0 Unported License.

1:2 Étienne Miquey

Nevertheless, dependent types are known to misbehave in the presence of control operators, and lead to logical inconsistencies [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF]. Since the same problem arises with a wider class of effects, it seems that we are facing the following dilemma: either we choose an effectful language (allowing us to write more programs) while accepting the lack of dependent types, or we choose a dependently typed language (allowing us to write finer specifications) and give up effects.

Many works have tried to fill the gap between effectful programming languages and logic, by accommodating weaker forms of dependent types with computational effects (e.g., divergence, I/O, local references, exceptions). Amongst other works, we can cite the recent works by Ahman et al. [START_REF] Danel Ahman | Dependent Types and Fibred Computational Effects[END_REF], by Vákár [START_REF] Vákár | A framework for dependent types and effects[END_REF][START_REF] Vákár | In Search of Effectful Dependent Types[END_REF] or by Pédrot and Tabareau who proposed a systematical way to add effects to type theory [START_REF] Pédrot | An effectful way to eliminate addiction to dependence[END_REF]. Side effects-that are impure computations in functional programming-are often interpreted by means of monads. Interestingly, control operators can be interpreted similarly through the continuation monad, but the continuation monad generally lacks the properties necessary to fit these frameworks.

Although dependent types and classical logic have been deeply studied separately, the problem of accommodating both features 1 in one and the same system has not found a completely satisfying answer yet. Recent works from Herbelin [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF] and Lepigre [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF] proposed some restrictions on dependent types to make them compatible with a classical proof system, while Blot [START_REF] Blot | Hybrid realizability for intuitionistic and classical choice[END_REF] designed a hybrid realizability model where dependent types are restricted to an intuitionistic fragment.

Call-by-value and value restriction

In languages enjoying the Church-Rosser property (like the λ-calculus or Coq), the order of evaluation is irrelevant, and any reduction path will ultimately lead to the same value. In particular, the call-by-name and call-by-value evaluation strategies will always give the same result. However, this is no longer the case in presence of side effects. Indeed, consider the simple case of a function applied to a term producing some side effects (for instance increasing a reference). In call-by-name, the computation of the argument is delayed to the time of its effective use, while in call-by-value the argument is reduced to a value before performing the application. If, for instance, the function never uses its argument, the call-by-name evaluation will not generate any side effect, and if it uses it twice, the side effect will occur twice (and the reference will have its value increased by two). On the contrary, in both cases the call-by-value evaluation generates the side effect exactly once (and the reference has its value increased by one).

In this paper, we present a language following the call-by-value reduction strategy, which is as much a design choice as a goal in itself. Indeed, when considering a language with control operators (or other kinds of side effects), soundness often turns out to be subtle to preserve in call-by-value. The first issues in call-by-value in the presence of side effects were related to references [START_REF] Wright | Simple imperative polymorphism[END_REF] and polymorphism [START_REF] Harper | Polymorphic type assignment and CPS conversion[END_REF]. In both cases, a simple solution (but often unnecessarily restrictive in practice [START_REF] Garrigue | Relaxing the value restriction[END_REF][START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]) to solve the inconsistencies consists in the introduction of a value restriction for the problematic cases, restoring then a sound type system. Recently, Lepigre presented a proof system providing dependent types and a control operator [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF], whose consistency is preserved by means of a semantical value restriction defined for terms that behave as values up to observational equivalence. In the present work, we will rather use a syntactic restriction to a fragment of proofs that allows slightly more than values. As we will see, the restriction that arises naturally coincides with the negative-elimination-free fragment of Herbelin's dPAω system [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF].

A sequent calculus presentation

The main achievement of this paper is to give a sequent calculus presentation2 of a call-by-value language with classical control and dependent types, and to justify its soundness through a continuation-passing style translation. Our calculus is an extension of the λµ μ-calculus [START_REF] Curien | The duality of computation[END_REF] with dependent types. Amongst other motivations, such a calculus is close to an abstract machine, which makes it particularly suitable to define CPS translations or to be an intermediate language for compilation [START_REF] Downen | Sequent calculus as a compiler intermediate language[END_REF]. As a matter of fact, the original motivation for this work was the design of a program translation for Herbelin's dPAω system (that already encompasses control operators and dependent types) to justify its soundness. However, this calculus was presented in a natural deduction style, making such a translation hard to obtain. We thus developed the framework presented in this paper to have an intermediate language more suitable for a continuation-passing style translation at our disposal.

Additionally, while we consider in this paper the specific case of a calculus with classical logic, the sequent calculus presentation itself is responsible for another difficulty. As we will see, the usual call-by-value strategy of the λµ μ-calculus causes subject reduction to fail, which would already happen in an intuitionistic type theory. We claim that the solutions we give in this paper also works in the intuitionistic case. In particular, the system we develop might be a first step towards the adaption of the well-understood continuation-passing style translations for ML to design a (dependently) typed compilation of a system with dependent types such as Coq.

Delimited continuations and CPS translation

The main challenge in designing a sequent calculus with dependent types lies in the fact that the natural relation of reduction one would expect in such a framework is not safe with respect to types. As we will discuss in Section 2.6, the problem can be understood as a desynchronization of the type system with respect to the reduction. A simple solution, presented in Section 2, consists in the addition of an explicit list of dependencies in typing derivations. This has the advantage of leaving the computational part of the original calculus unchanged. However, it is not suitable for obtaining a continuation-passing style translation.

We thus present a second way to solve this issue by introducing delimited continuations [START_REF] Ariola | A type-theoretic foundation of delimited continuations[END_REF], which are used to force the purity needed for dependent types in an otherwise non purely functional language. It also justifies the relaxation of the value restriction and leads to the definition of the negative-elimination-free fragment (Section 3). In addition, it allows for the design, in Section 4, of a continuation-passing style translation that preserves dependent types and permits us to prove the soundness of our system. Finally, it also provides us with a way to embed our calculus into Lepigre's calculus [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF], as we shall see in Section 5. This embedding has in particular the benefit of furnishing us with a realizability interpretation for free.

Contributions of the paper

Our main contributions in this paper can be listed as follows:

• We soundly combine dependent types and control operators by means of a syntactic restriction to the negative-elimination-free fragment;

• We give a sequent calculus presentation and solve the type-soundness issues it raises in two different ways; • Our first solution simply relies on a list of dependencies that is added to the type system • Our second solution uses delimited continuations to ensure consistency with dependent types and provides us with a CPS translation (carrying dependent types) to a calculus without control operator; • We relate our system to Lepigre's calculus, which gives us a realizability interpretation for free and offers an additional way of proving the consistency of our system.

This paper is an extended and revised version of the article presented at ESOP 2017 [START_REF] Miquey | A classical sequent calculus with dependent types[END_REF].

A MINIMAL CLASSICAL LANGUAGE WITH DEPENDENT TYPES

2.1 A short primer to the λµ μ-calculus We recall here the spirit of the λµ μ-calculus, for further details and references please refer to the original article [START_REF] Curien | The duality of computation[END_REF]. The syntax and reduction rules (parameterized over a subset of proofs V and a subset of evaluation contexts E) are given in Figure 1, where μa.c can be read as a context let a = [ ] in c. A command ⟨p||e⟩ can be understood as a state of an abstract machine, representing the evaluation of a proof p (the program) against a co-proof e (the stack) that we call context. The µ operator comes from Parigot's λµ-calculus [START_REF] Parigot | Proofs of strong normalisation for second order classical natural deduction[END_REF], µα binds a context to a context variable α in the same way that μa binds a proof to some proof variable a.

The λµ μ-calculus can be seen as a proof-as-program correspondence between sequent calculus and abstract machines. Right introduction rules correspond to typing rules for proofs, while left introduction are seen as typing rules for evaluation contexts. In contrast with Gentzen's original presentation of sequent calculus, the type system of the λµ μ-calculus explicitly identifies at any time which formula is being worked on. In a nutshell, this presentation distinguishes between three kinds of sequents:

(1) sequents of the form Γ ⊢ p : A | ∆ for typing proofs, where the focus is put on the (right) formula A;

(2) sequents of the form Γ | e : A ⊢ ∆ for typing contexts, where the focus is put on the (left) formula A; (3) sequents of the form c : (Γ ⊢ ∆) for typing commands, where no focus is set.

In a right (resp. left) sequent Γ ⊢ p : A | ∆, the singled out formula3 A reads as the conclusion "where the proof shall continue" (resp. hypothesis "where it happened before").

For example, the left introduction rule of implication can be seen as a typing rule for pushing an element q on a stack e leading to the new stack q • e:

Γ ⊢ q : A | ∆ Γ | e : B ⊢ ∆ Γ | q • e : A → B ⊢ ∆ → l
As for the reduction rules, we can see that there is a critical pair if V and E are not restricted enough:

c[α := μx .c ′ ] ←-⟨µα .c || μx .c ′ ⟩ -→ c ′ [x := µα .c].
The difference between call-by-name and call-by-value can be characterized by how this critical pair 4is solved, by defining V and E such that the two rules do not overlap. Defining the subcategories Remark 2.1 (Application). The reader unfamiliar with the λµ μ-calculus might be puzzled by the absence of a syntactic construction for the application of proof terms. Intuitively, the usual application p q of the λ-calculus is replaced by the application of the proof p to a stack of the shape q • e as in an abstract machine 5 . The usual application can thus be recovered through the following shorthand:

Γ ⊢ t :A | ∆ Γ | e : A ⊢ ∆ ⟨t ||e⟩ : (Γ ⊢ ∆) (Cut) (a : A) ∈ Γ Γ ⊢ a : A | ∆ (Ax r ) Γ, a : A ⊢ p : B | ∆ Γ ⊢ λa.p : A → B | ∆ (→ r ) c : (Γ ⊢ ∆, α : A) Γ ⊢ µα .c : A | ∆ (µ) (α : A) ∈ ∆ Γ | α : A ⊢ ∆ (Ax l ) Γ ⊢ p : A | ∆ Γ | e : B ⊢ ∆ Γ | p • e : A → B ⊢ ∆ (→ l ) c : (Γ, a : A ⊢ ∆) Γ | μa.c : A ⊢ ∆ ( μ) (c) Typing rules
p q ≜ µα .⟨p||q • α⟩ Finally, it is worth noting that the µ binder is a control operator, since it allows for catching evaluation contexts and backtracking further in the execution. This is the key ingredient that makes the λµ μ-calculus a proof system for classical logic. To illustrate this, let us draw the analogy with the call/cc operator of Krivine's λ c -calculus [START_REF] Krivine | Realizability in classical logic. In interactive models of computation and program behaviour[END_REF]. Let us define the following proof terms:

call/cc ≜ λa.µα .⟨a||k α • α⟩ k e ≜ λa ′ .µβ .⟨a ′ ||e⟩
The proof k e can be understood as a proof term where the context e has been encapsulated. As expected, call/cc is a proof for Peirce's law (see Figure 2), which is known to imply other forms of classical reasoning (e.g., the law of excluded middle, the double negation elimination).

Let us observe the behavior of call/cc (in call-by-name evaluation strategy, as in Krivine λ c -calculus): in front of a context of the shape q • e with e of type A, it will catch the context e a :

(A → B) → A ⊢ a : (A → B) → A | • (Ax r ) •, a ′ : A ⊢ a ′ : A | • (Ax r ) • | α : A ⊢ α : A, • (Ax l ) ⟨a ′ ||α⟩ : (•, a ′ : A ⊢ α : A, β : B) (Cut) •, a ′ : A ⊢ µβ .⟨a ′ ||α⟩ : B | α : A (µ) • ⊢ λa ′ .µβ .⟨a ′ ||α⟩ : A → B | α : A (→ r ) | α : A ⊢ α : A (Ax l ) • | λa ′ .µβ .⟨a ′ ||α⟩ • α : (A → B) → A ⊢ α : A (→ l ) ⟨a||λa ′ .µβ .⟨a ′ ||α⟩ • α⟩ : (a : (A → B) → A ⊢ α : A) (Cut) a : (A → B) → A ⊢ µα .⟨a||λa ′ .µβ .⟨a ′ ||α⟩ • α⟩ : A | (µ) ⊢ λa.µα .⟨a||λa ′ .µβ .⟨a ′ ||α⟩ • α⟩ : ((A → B) → A) → A | (→ r )
(where • is used to shorten useless parts of typing contexts.) Fig. 2. Proof term for Peirce's law thanks to the µα binder and reduce as follows:

⟨λa.µα .⟨a||k α • α⟩||q • e⟩ → ⟨q|| μa.⟨µα .⟨a||k α • α⟩||e⟩⟩ → ⟨µα .⟨q||k α • α⟩||e⟩ → ⟨q||k e • e⟩
We notice that the proof term k e = λa ′ .µβ .⟨a ′ ||e⟩ on top of the stack (which, if e was of type A, is of type A → B, see Figure 2) contains a second binder µβ. In front of a stack q ′ • e ′ , this binder will now catch the context e ′ and replace it by the former context e:

⟨λa ′ .µβ .⟨a ′ ||e⟩||q ′ • e ′ ⟩ → ⟨q ′ || μa ′ .⟨µβ .⟨a ′ ||e⟩||e ′ ⟩⟩ → ⟨µβ .⟨q ′ ||e⟩||e ′ ⟩ → ⟨q ′ ||e⟩
This computational behavior corresponds exactly to the usual reduction rule for call/cc in the Krivine machine [START_REF] Krivine | Realizability in classical logic. In interactive models of computation and program behaviour[END_REF]:

call/cc ⋆ t • π ≻ t ⋆ k π • π k π ⋆ t • π ′ ≻ t ⋆ π

Inconsistency of classical logic with dependent types

The simultaneous presence of classical logic (i.e. of a control operator) and dependent types is known to cause a degeneracy of the domain of discourse. Let us shortly recap the argument of Herbelin highlighting this phenomenon [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF].

Let us adopt here a stratified presentation of dependent types, by syntactically distinguishing terms-that represent mathematical objects-from proof terms-that represent mathematical proofs. In other words, we syntactically separate the categories corresponding to witnesses and proofs in dependent sum types. Consider a minimal logic of strong existentials and equality, whose formulas, terms (only representing natural number) and proofs are defined as follows:

Formulas A, B ::= t = u | ∃x N .A Terms t, u ::= n | wit p Proofs p, q ::= refl | subst p q | (t, p) | prf p (n ∈ N)
Let us explain the different proof terms by presenting their typing rules. First of all, the pair (t, p) is a proof for an existential formula ∃x N .A where t is a witness for x and p is a certificate for A[t/x]. This implies that both formulas and proofs are dependent on terms, which is usual in mathematics.

What is less usual in mathematics is that, as in Martin-Löf's type theory, dependent types also allow for terms (and thus for formulas) to be dependent on proofs, by means of the constructors wit p and prf p. Typing rules are given with separate typing judgments for terms, which can only be of type N:

Γ ⊢ p : A(t) Γ ⊢ t : N Γ ⊢ (t, p) : ∃x N .A (∃ I ) Γ ⊢ (t, p) : ∃x N .A Γ ⊢ prf p : A[wit p/x] (prf ) Γ ⊢ t : ∃x N .A Γ ⊢ wit t : N (wit) n ∈ N Γ ⊢ n : N
Then, refl is a proof term for equality, and subst p q allows us to use a proof of an equality t = u to convert a formula A(t) into A(u):

t → u Γ ⊢ refl : t = u (refl) Γ ⊢ p : t = u Γ ⊢ q : B[t] Γ ⊢ subst p q : B[u] (subst)
The reduction rules for this language, which are safe with respect to typing, are then: wit (t, p) → t prf (t, p) → p subst refl p → p Starting from this (sound) minimal language, Herbelin showed that its classical extension with the control operators call/cc k and throw k (that are similar to those presented in the previous section) permits to derive a proof of 0 = 1 [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF]. The call/cc k operator, which is a binder for the variable k, is intended to catch its surrounding evaluation context. On the contrary, throw k discards the current context and restores the context captured by call/cc k . The addition to the type system of the typing rules for these operators:

Γ, k : ¬A ⊢ p : A Γ ⊢ call/cc k p : A Γ, k : ¬A ⊢ p : A Γ, k : ¬A ⊢ throw k p : B
allows the definition of the following proof:

p 0 ≜ call/cc k (0, throw k (1, refl)) : ∃x N .x = 1
Intuitively such a proof catches the context, gives 0 as witness (which is incorrect), and a certificate that will backtrack and give 1 as witness (which is correct) with a proof of the equality.

If, besides, the following reduction rules6 are added:

wit (call/cc k p) → call/cc k (wit (p[k(wit { })/k])) call/cc k t → t (k FV (t))
then we can formally derive a proof of 1 = 0. Indeed, the term wit p 0 will reduce to call/cc k 0, which itself reduces to 0. The proof term refl is thus a proof of wit p 0 = 0, and we obtain the following proof of 1 = 0:

⊢ p 0 : ∃x N .x = 1 ⊢ prf p 0 : wit p 0 = 1 (prf ) wit p 0 → 0 ⊢ refl : wit p 0 = 0 (refl) ⊢ subst (prf p 0 ) refl : 1 = 0 (subst)
The bottom line of this example is that the same proof p 0 is behaving differently in different contexts thanks to control operators, causing inconsistencies between the witness and its certificate. The easiest and usual approach (in natural deduction) to prevent this is to impose a restriction to values (which are already reduced) for proofs appearing inside dependent types and within the operators wit and prf , together with a call-by-value discipline. In the present example, this would prevent us from writing wit p 0 and prf p 0 .

1:8 Étienne Miquey

A minimal language with value restriction

In this section, we will focus on value restriction in a similar framework, and show that the obtained proof system is coherent. We will then see, in Section 3, how to relax this constraint. We follow here the stratified presentation7 from the previous section. We place ourselves in the framework of the λµ μ-calculus to which we add:

• a language of terms which contain an encoding 8 of the natural numbers, • proof terms (t, p) to inhabit the strong existential ∃x N .A together with the first and second projections, called respectively wit (for terms) and prf (for proofs), • a proof term refl for the equality of terms and a proof term subst for the convertibility of types over equal terms.

For simplicity reasons, we will only consider terms of type N throughout this paper. We address the question of extending the domain of terms in Section 6.2. The syntax of the corresponding system, that we call dL, is given by:

Terms t ::= x | n | wit V Proof terms p ::= V | µα .c | (t, p) | prf V | subst p q Proof values V ::= a | λa.p | λx .p | (t, V ) | refl Contexts e ::= α | p • e | t • e | μa.c Commands c ::= ⟨p||e⟩ (n ∈ N)
The formulas are defined by:

Formulas A, B ::= ⊤ | ⊥ | t = u | ∀x N .A | ∃x N .A | Π a:A B.
Note that we included a dependent product Π a:A B at the level of proof terms, but that in the case where a FV (B) this amounts to the usual implication A → B.

Reduction rules

As explained in Section 2.2, a backtracking proof might give place to different witnesses and proofs according to the context of reduction, leading to inconsistencies [START_REF] Herbelin | On the degeneracy of sigma-types in presence of computational classical logic[END_REF]. The substitution at different places of a proof which can backtrack, as the call-by-name evaluation strategy does, is thus an unsafe operation. On the contrary, the call-by-value evaluation strategy forces a proof to reduce first to a value (thus furnishing a witness) and to share this value amongst all the commands. In particular, this maintains the value restriction along reduction, since only values are substituted. The reduction rules, defined in Figure 3 (where t → t ′ denotes the reduction of terms and c ⇝ c ′ the reduction of commands), follow the call-by-value evaluation principle. In particular one can see that whenever a command is of the shape ⟨C[p]||e⟩ where C[p] is a proof built on top of p which is not a value, it reduces to ⟨p|| μa.⟨C[a]||e⟩⟩, opening the construction to evaluate p 9 .

Additionally, we denote by A ≡ B the transitive-symmetric closure of the relation A ▷ B, defined as a congruence over term reduction (i.e. if t → t ′ then A[t] ▷ A[t ′ ]) and by the rules:

0 = 0 ▷ ⊤ 0 = S(u) ▷ ⊥ S(t) = 0 ▷ ⊥ S(t) = S(u) ▷ t = u ⟨µα .c ||e⟩ ⇝ c[e/

Typing rules

As we explained before, in this section we limit ourselves to the simple case where dependent types are restricted to values, to make them compatible with classical logic. But even with this restriction, defining the type system in the most naive way leads to a system in which subject reduction will fail. Having a look at the β-reduction rule gives us an insight of what happens. Let us imagine that the type system of the λµ μ-calculus has been extended to allow dependent products instead of implications. and consider a proof λa.p : Π a:A B in front of a context q • e : Π a:A B. A typing derivation of the corresponding command would be of the form:

Π p Γ, a : A ⊢ p : B | ∆ Γ ⊢ λa.p : Π a:A B | ∆ (→ r ) Π q Γ ⊢ q : A | ∆ Π e Γ | e : B[q/a] ⊢ ∆ Γ | q • e : Π a:A B ⊢ ∆ (→ l ) ⟨λa.p||q • e⟩ : Γ ⊢ ∆ (Cut)
while this command would reduce as follows:

⟨λa.p||q • e⟩ ⇝ ⟨q|| μa.⟨p||e⟩⟩.

On the right-hand side, we see that p, whose type is B[a], is now cut with e whose type is B[q]. Consequently, we are not able to derive a typing judgment 10 for this command anymore:

Π q Γ ⊢ q : A | ∆ Γ, a : A ⊢ p : ¨B[a] | ∆ Γ, a : A | e : ¨B[q] ⊢ ∆ ⟨p||e⟩ : Γ, a : A ⊢ ∆ Mismatch Γ | μa.⟨p||e⟩ : A ⊢ ∆ ( μ) ⟨q|| μa.⟨p||e⟩⟩ : Γ ⊢ ∆ (Cut)
The intuition is that in the full command, a has been linked to q at a previous level of the typing judgment. However, the command is still safe, since the head-reduction imposes that the command ⟨p||e⟩ will not be executed before the substitution of a by q11 is performed, and by then the problem would be solved. This phenomenon can be seen as a desynchronization of the typing process with respect to computation. The synchronization can be re-established by making explicit a list of dependencies σ in the typing rules, which links μ variables (here a) to the associated proof term on the left-hand side of the command (here q). We can now obtain the following typing derivation:

Γ ⊢ p : A | ∆; σ Γ | e : B ⊢ ∆; σ {•|p} B ∈ A σ ⟨p||e⟩ : Γ ⊢ ∆; σ (Cut) (a : A) ∈ Γ Γ ⊢ a : A | ∆; σ (Ax r ) (α : A) ∈ ∆ Γ | α : A ⊢ ∆; σ {•|p} (Ax l ) c : (Γ ⊢ ∆, α : A; σ ) Γ ⊢ µα .c : A | ∆; σ
Π q Γ ⊢ q : A | ∆ Π p Γ, a : A ⊢ p : B[a] | ∆ Π e Γ, a : A | e : B[q] ⊢ ∆; σ {a|q}{•|p} ⟨p||e⟩ : Γ, a : A ⊢ ∆; σ {a|q} (Cut) Γ | μa.⟨p||e⟩ : A ⊢ ∆; σ {.|q} ( μ) ⟨q|| μa.⟨p||e⟩⟩ : Γ ⊢ ∆; σ (Cut)
Formally, we denote by D the set of proofs we authorize in dependent types, and define it for the moment as the set of values: D ≜ V . We define a list of dependencies σ as a list binding pairs of proof terms 12 :

σ ::= ε | σ {p|q},
and we define A σ as the set of types that can be obtained from A by replacing all (or none) occurrences of p by q for each binding {p|q} in σ such that q ∈ D:

A ε ≜ {A} A σ {p |q } ≜ A σ ∪ (A[q/p]) σ if q ∈ D A σ otherwise.
The list of dependencies is filled while going up in the typing tree, and it can be used when typing a command ⟨p||e⟩ to resolve a potential inconsistency between their types:

Γ ⊢ p : A | ∆; σ Γ | e : B ⊢ ∆; σ {•|p} B ∈ A σ ⟨p||e⟩ : Γ ⊢ ∆; σ (Cut)
Remark 2.2. The reader familiar with explicit substitutions [START_REF] Fridlender | Pure type systems with explicit substitutions[END_REF] can think of the list of dependencies as a fragment of the substitution that is available when a command c is reduced. Another remark is that the design choice for the (Cut) rule is arbitrary, in the sense that we chose to check whether B is in A σ . We could equivalently have checked whether the condition σ (A) = σ (B) holds, where σ (A) refers to the type A where for each binding {p|q} ∈ σ with q ∈ D, all the occurrences of p have been replaced by q.

Furthermore, when typing a stack with the (→ l ) and (∀ l ) rules, we need to drop the open binding in the list of dependencies 13 . We introduce the notation Γ | e : A ⊢ ∆; σ {•| †} to denote that the dependency to be produced is irrelevant and can be dropped. This trick spares us from defining a second type of sequents Γ | e : A ⊢ ∆; σ to type contexts when dropping the (open) binding {•|p}. Alternatively, one can think of † as any proof term not in D, which is the same with respect to the list of dependencies. The resulting set of typing rules is given in Figure 4, where we assume that every variable bound in the typing context is bound only once (proofs and contexts are considered up to α-conversion).

Note that we work with two-sided sequents here to stay as close as possible to the original presentation of the λµ μ-calculus [START_REF] Curien | The duality of computation[END_REF]. In particular this means that a type in ∆ might depend on a variable previously introduced in Γ and vice versa, so that the split into two contexts makes us lose track of the order of introduction of the hypotheses. In the sequel, to be able to properly define a typed CPS translation, we consider that we can unify both contexts into a single one that is coherent with respect to the order in which the hypotheses have been introduced.

Example 2.3. The proof p 1 ≜ subst (prf p 0 ) refl which was of type 1 = 0 in Section 2.2 is now incorrect since the backtracking proof p 0 , defined by µα .(0, µ_.⟨(1, refl)||α⟩) in our framework, is not a value in D. The proof p 1 should rather be defined by 14 µα .⟨p 0 || μa.⟨subst (prf a) refl||α⟩⟩ which can only be given the type 1 = 1.

Subject reduction

We start by giving a few technical lemmas that will be used for proving subject reduction. First, we will show that typing derivations allow weakening on the lists of dependencies. For this purpose, we introduce the notation σ ⇛ σ ′ to denote that whenever a judgment is derivable with σ as list of dependencies, then it is derivable using σ ′ :

σ ⇛ σ ′ ≜ ∀c ∀Γ ∀∆.(c : (Γ ⊢ ∆; σ ) ⇒ c : (Γ ⊢ ∆; σ ′ )).
This clearly implies that the same property holds when typing evaluation contexts, i.e. if σ ⇛ σ ′ then σ can be replaced by σ ′ in any typing derivation for any context e. Lemma 2.4 (Dependencies weakening). For any list of dependencies σ we have:

1. ∀V .(σ {V |V } ⇛ σ ) 2. ∀σ ′ .(σ ⇛ σσ ′ )
Proof. The first statement is obvious. The proof of the second one is straightforward from the fact that for any p and q, by definition A σ ⊂ A σ {p |q } . □

As a corollary, we get that † can indeed be replaced by any proof term when typing a context.

Corollary 2.5. If σ ⇛ σ ′ , then for any p, e, Γ, ∆:

Γ | e : A ⊢ ∆; σ {•| †} ⇒ Γ | e : A ⊢ ∆; σ ′ {•|p}.
Proof. Assume that e is of the form μa.c (other cases are trivial), then we have c : Γ ⊢ ∆; σ {a| †}. By definition of † and from the hypothesis, we get that σ {a| †} ⇛ σ ′ , i.e. that c : Γ ⊢ ∆; σ ′ is derivable. By applying the previous Lemma, we get that c : Γ ⊢ ∆; σ ′ {a|p} is derivable for any proof p, whence the result. □

We first state the usual lemmas that guarantee the safety of terms (resp. values, contexts) substitution.

Lemma 2.6 (Safe term substitution

). If Γ ⊢ t : N | ∆; ε then: (1) c : (Γ, x : N, Γ ′ ⊢ ∆; σ ) ⇒ c[t/x] : (Γ, Γ ′ [t/x] ⊢ ∆[t/x]; σ [t/x]), (2)
Γ, x : N, Γ ′ ⊢ q : B | ∆; σ ⇒ Γ, Γ ′ [t/x] ⊢ q[t/x] : B[t/x] | ∆[t/x]; σ [t/x], (3)
Γ, x : N, Γ ′ | e : B ⊢ ∆; σ ⇒ Γ, Γ ′ [t/x] | e[t/x] : B[t/x] ⊢ ∆[t/x]; σ [t/x], (4) Γ, x : N, Γ ′ ⊢ u : N | ∆; σ ⇒ Γ, Γ ′ [t/x] ⊢ u[t/x] : N | ∆[t/x]; σ [t/x].
Lemma 2.7 (Safe value substitution).

If Γ ⊢ V : A | ∆; ε then: (1) c : (Γ, a : A, Γ ′ ⊢ ∆; σ ) ⇒ c[V /a] : (Γ, Γ ′ [V /a] ⊢ ∆[V /a]; σ [V /a]), (2) Γ, a : A, Γ ′ ⊢ q : B | ∆; σ ⇒ Γ, Γ ′ [V /a] ⊢ q[V /a] : B[V /a] | ∆[V /a]; σ [t/x], (3)
Γ, a : A, Γ ′ | e : B ⊢ ∆; σ ⇒ Γ, Γ ′ [V /a] | e[V /a] : B[V /a] ⊢ ∆[V /a]; σ [V /a], (4)
Γ, a : A, Γ ′ ⊢ u : N | ∆; σ ⇒ Γ, Γ ′ [V /a] ⊢ u[V /a] : N | ∆[V /a]; σ [V /a]. Lemma 2.8 (Safe context substitution). If Γ | e : A ⊢ ∆; ε then: (1) c : (Γ ⊢ ∆, α : A, ∆ ′ ; σ ) ⇒ c[e/α] : (Γ ⊢ ∆, ∆ ′ ; σ ), ( 2
) Γ ⊢ q : B | ∆, α : A, ∆ ′ ; σ ⇒ Γ ⊢ q[e/α] : B | ∆, ∆ ′ ; σ , ( 3
) Γ | e : B ⊢ ∆, α : A, ∆ ′ ; σ ⇒ Γ | e[e/α] : B ⊢ ∆, ∆ ′ ; σ , ( 4
) Γ ⊢ u : N | ∆, α : A, ∆ ′ ; σ ⇒ Γ ⊢ u : N | ∆, ∆ ′ ; σ ].
Proof. The proofs are done by induction on typing derivations. □

We can now prove the preservation of typing through reduction, using the previous lemmas for rules which perform a substitution, and the list of dependencies to resolve local desynchronizations for dependent types. Theorem 2.9 (Subject reduction). If c, c ′ are two commands of dL such that c :

(Γ ⊢ ∆; ε) and c ⇝ c ′ , then c ′ : (Γ ⊢ ∆; ε).
Proof. The proof is done by induction on the typing derivation of c : (Γ ⊢ ∆; ε), assuming that for each typing proof, the conversion rules are always pushed down and right as much as possible.

To save some space, we sometimes omit the list of dependencies when empty, writing c : Γ ⊢ ∆ instead of c : Γ ⊢ ∆; ε, and we denote the composition of consecutive rules (≡ l ) as:

Γ | e : B ⊢ ∆; σ Γ | e : A ⊢ ∆; σ Π q Γ ⊢ q : A ′ | ∆ Γ ⊢ q : A | ∆ (≡ l ) Π p Γ, a : A ⊢ p : B | ∆ Γ, a : A ⊢ p : B ′ | ∆ (≡ r ) Π e Γ, a : A | e : B ′ q ⊢ ∆; {a|q}{•|p} B ′ q ∈ B ′ {a |q } ⟨p||e⟩ : Γ, a : A ⊢ ∆; {a|q} (Cut) Γ | μa.⟨p||e⟩ : A ⊢ ∆; {.|q} ( μ) ⟨q|| μa.⟨p||e⟩⟩ : Γ ⊢ ∆ (Cut)
using Corollary 2.5 to weaken the dependencies in Π e .

• Case ⟨µα .c ||e⟩ ⇝ c[e/α].

A typing proof for the command on the left-hand side is of the form:

Π c c : Γ ⊢ ∆, α : A Γ ⊢ µα .c : A | ∆ (µ) Π e Γ | e : A ⊢ ∆; {•|µα .c} ⟨µα .c ||e⟩ : Γ ⊢ ∆ (Cut)
We get a proof that c[e/α] : Γ ⊢ ∆ is valid by Lemma 2.8.

• Case ⟨V || μa.c⟩ ⇝ c[V /a].
A typing proof for the command on the left-hand side is of the form:

Π V Γ ⊢ V : A | ∆ Π c c : Γ, a : A ′ ⊢ ∆; {a|V } Γ | μa.c : A ′ ⊢ ∆; {•|V } ( μ) Γ | μa.c : A ⊢ ∆; {•|V } (≡ l ) ⟨V || μa.c⟩ : Γ ⊢ ∆ (Cut)
We first observe that we can derive the following proof:

Π V Γ ⊢ V : A | ∆ Γ ⊢ V : A ′ | ∆ (≡ l )
and we get a proof for c[V /a] : Γ ⊢ ∆; {V |V } by Lemma 2.7. We finally get a proof for c[V /a] : Γ ⊢ ∆ by Lemma 2.4.

• Case ⟨(t, p)||e⟩ ⇝ ⟨p|| μa.⟨(t, a)||e⟩⟩, with p V .

A proof of the command on the left-hand side is of the form:

Π t Γ ⊢ t : N | ∆ Π p Γ ⊢ p : A[t/x] | ∆ Γ ⊢ (t, p) : ∃x N .A | ∆ (∃ r ) Π e Γ | e : ∃x N .A ⊢ ∆; {•|(t, p)} ⟨(t, p)||e⟩ : Γ ⊢ ∆ (Cut)
We can build the following derivation:

Π p Γ ⊢ p : A[t/x] | ∆ Π (t,a) Γ, a : A[t/x] ⊢ (t, a) : ∃x N .A | ∆ (∃ I ) Π e Γ | e : ∃x N .A ⊢ ∆; {a|p}{•|(t, a)} ⟨(t, a)||e⟩ : Γ, a : A[t/x] ⊢ ∆; {a|p} (Cut) Γ | μa.⟨(t, a)||e⟩ : A[t/x] ⊢ ∆; {•|p} ( μ) ⟨p|| μa.⟨(t, a)||e⟩⟩ : Γ ⊢ ∆ (Cut)
where Π (t,a) is as expected, observing that since p D, the binding {•|(t, p)} is the same as {•| †}, and we can apply Corollary 2.5 to weaken dependencies in Π e .

• Case ⟨prf (t, V )||e⟩ ⇝ ⟨V ||e⟩. This case is easy, observing that a derivation of the command on the left-hand side is of the form:

Π t Π V Γ ⊢ V : A(t) | ∆ Γ ⊢ (t, V ) : ∃x N .A(x) | ∆ (∃ r ) Γ ⊢ prf (t, V ) : A(wit (t, V )) | ∆ (prf ) Π e Γ | e : A(wit (t, V )) ⊢ ∆; {•| †} ⟨prf (t, V )||e⟩ : Γ ⊢ ∆ (Cut)
Since by definition we have A(wit (t, V )) ≡ A(t), we can derive:

Π V Γ ⊢ V : A(t) | ∆ Π e Γ | e : A(wit (t, V )) ⊢ ∆; {•|V } Γ | e : A(t) ⊢ ∆; {•|V } (≡ l ) ⟨prf (t, V )||e⟩ : Γ ⊢ ∆ (Cut)
• Case ⟨subst refl q||e⟩ ⇝ ⟨q||e⟩. This case is straightforward, observing that for any terms t, u, if we have refl :

t = u, then A[t] ≡ A[u] for any A.
• Case ⟨subst p q||e⟩ ⇝ ⟨p|| μa.⟨subst a q||e⟩⟩. This case is similar to the case ⟨(t, p)||e⟩.

• Case c[t] ⇝ c[t ′ ] with t → t ′ .
Immediate by observing that by definition of the relation ≡, we have A[t] ≡ A[t ′ ] for any A. □

Soundness

We here give a proof of the soundness of dL with a value restriction. The proof is based on an embedding into the λµ μ-calculus extended with pairs, whose syntax and rules are given in Figure 5.

A more interesting proof through a continuation-passing translation is presented in Section 4. We first show that typed commands of dL normalize by translation to the simply-typed λµ μcalculus with pairs (i.e. extended with proofs of the form (p 1 , p 2 ) and contexts of the form μ(a 1 , a 2 ).c). We do not consider here a particular reduction strategy, and take ↣ to be the contextual closure of the rules given in Figure 5.

The translation essentially consists in erasing the dependencies in types 15 , turning the dependent products into arrows and the dependent sum into a pair. The erasure procedure is defined by:

(∀x N .A) * ≜ N → A * ⊤ * ≜ N → N (∃x N .A) * ≜ N ∧ A * ⊥ * ≜ N → N (Π a:A B) * ≜ A * → B * (t = u) * ≜ N → N
and the corresponding translation for terms, proofs, contexts and commands is given by:

1:16 Étienne Miquey Proofs p ::= V | µα .c | (p 1 , p 2 ) Values V ::= a | λa.p | (V 1 , V 2 ) Contexts e ::= α | p • e | μa.c | μ(a 1 , a 2 ).c Commands c ::= ⟨p||e⟩ Γ ⊢ p 1 : A 1 | ∆ Γ ⊢ p 2 : A 2 | ∆ Γ ⊢ (p 1 , p 2 ) : A 1 ∧ A 2 | ∆ (∧ r ) c : Γ, a 1 : A 1 , a 2 : A 2 ⊢ ∆ Γ | μ(a 1 , a 2 ).c : A 1 ∧ A 2 ⊢ ∆ (∧ l ) (a) Syntax (b) Typing rules ⟨µα .c ||e⟩ ↣ c[e/α] ⟨λa.p||q • e⟩ ↣ ⟨q|| μa.⟨p||e⟩⟩ ⟨p|| μa.c⟩ ↣ c[p/a] ⟨(p 1 , p 2 )|| μ(a 1 , a 2 ).c⟩ ↣ c[p 1 /a 1 ][p 2 /a 2 ] µα .⟨p||α⟩ ↣ p μa.⟨a||e⟩ ↣ e (c) Reduction rules
⟨p||e⟩ * ≜ ⟨p * ||e * ⟩ α * ≜ α (t • e) * ≜ t * • e * (q • e) * ≜ q * • e * ( μa.c) * ≜ μa.c * x * ≜ x n * ≜ n (wit p) * ≜ π 1 (p * ) a * ≜ a refl * ≜ λx .x (λa.p) * ≜ λa.p * (λx .p) * ≜ λx .p * (µα .c) * ≜ µα .c * (prf p) * ≜ π 2 (p * ) (t, p) * ≜ µα .⟨p * || μa.⟨(t * , a)||α⟩⟩ (subst V q) * ≜ µα .⟨q * ||α⟩ (subst p q) * ≜ µα .⟨p * || μ_ .⟨µα .⟨q * ||α⟩||α⟩⟩ (p V )
where π i (p) ≜ µα .⟨p|| μ(a 1 , a 2 ).⟨a 1 ||α⟩⟩. The term n is defined as any encoding of the natural number n with its type N * , the encoding being irrelevant here as long as n ∈ V . Note that we translate differently subst V q and subst p q to simplify the proof of Proposition 2.12. We first show that the erasure procedure is adequate with respect to the previous translation.

Lemma 2.10. The following holds for any types A and B:

(1) For any terms t and u, (A[t/u]) * = A * .

(2) For any proofs p and q, (A[p/q]) * = A * .

(

) If A ≡ B then A * = B * . (4) For any list of dependencies σ , if A ∈ B σ , then A * = B * . 3
Proof. Straightforward: (1) and ( 2) are direct consequences of the erasure of terms (and thus proofs) from types. (3) follows from (1),( 2) and the fact that (t = u) * = ⊤ * = ⊥ * . (4) follows from [START_REF] Ariola | A type-theoretic foundation of delimited continuations[END_REF]. □

We can extend the erasure procedure to typing contexts, and show that it is adequate with respect to the translation of proofs.

Proposition 2.11. The following holds for any contexts Γ, ∆ and any type A:

(1) For any command c, if c :

Γ ⊢ ∆; σ , then c * : Γ * ⊢ ∆ * . (2) For any proof p, if Γ ⊢ p : A | ∆; σ , then Γ * ⊢ p * : A * | ∆ * . (3) For any context e, if Γ | e : A ⊢ ∆; σ , then Γ * | e * : A * ⊢ ∆ * .
Proof. By induction on typing derivations. The fourth item of the previous lemma shows that the list of dependencies becomes useless: since

A ∈ B σ implies A * = B * , it is no longer needed Γ * | μa.⟨(t * , a)||α⟩ : A * ⊢ ∆ * , α : N∧A * ( μ) ⟨p * || μa.⟨(t * , a)||α⟩⟩ : Γ * ⊢ ∆ * , α : N∧A * (Cut) Γ * ⊢ µα .⟨p * || μa.⟨(t * , a)||α⟩⟩ : N ∧ A * | ∆ * (µ) □
We can then deduce the normalization of dL from the normalization of the λµ μ-calculus [START_REF] Polonovski | Strong normalization of lambda-bar-mu-mu-tilde-calculus with explicit substitutions[END_REF], by showing that the translation preserves the normalization in the sense that if c does not normalize, then neither does c * . Proposition 2.12. If c is a command such that c * normalizes, then c normalizes.

Proof. We prove this by contraposition, by showing that if c does not normalize (i.e. if it admits an infinite reduction path), then c * does not normalize either. We will actually prove a slightly more precise statement, namely that each step of reduction is reflected into at least one step through the translation:

∀c 1 , c 2 , (c 1 1 ⇝ c 2 ⇒ ∃n ≥ 1, (c 1 ) * n ↣ (c 2 ) * ).
Assuming this holds, we get from any infinite reduction path (for ⇝) starting from c another infinite reduction path (for ↣) from c * . Thus, the normalization of c * implies the one of c.

We shall now prove the previous statement by case analysis of the reduction c 1 ⇝ c 2 .

• Case wit (t, V ) → t: Proof. Proof by contradiction: if c does not normalize, then by Proposition 2.12 neither does c * . However, by Proposition 2.11 we have that c * : Γ * ⊢ ∆ * . This is absurd since any well-typed command of the λµ μ-calculus normalizes [START_REF] Polonovski | Strong normalization of lambda-bar-mu-mu-tilde-calculus with explicit substitutions[END_REF].

(wit (t, V )) * = π 1 (µα .⟨V * || μa.⟨(t * , a)||α⟩⟩) ↣ π 1 (µα .⟨(t * , V * )||α⟩) ↣ π 1 (t * , V * ) = µα .⟨(t * , t * )|| μ(a 1 , a 2 ).⟨a 1 ||α⟩⟩ ↣ µα .⟨t * ||α⟩ ↣ t * • Case ⟨µα .c ||e⟩ ⇝ c[e/α]: (⟨µα .c ||e⟩) * = ⟨µα .c * ||e * ⟩ ↣ c * [e * /α] = c[e/α] * • Case ⟨V || μa.c⟩ ⇝ c[V /a]: (⟨V || μa.c⟩) * = ⟨V * || μa.c * ⟩ ↣ c * [V * /a] = c[V /a]
(⟨prf (t, V )||e⟩) * = ⟨π 2 (µα .⟨V * || μa.⟨(t * , a)||α⟩⟩)||e * ⟩ ↣ ⟨π 2 (µα .⟨(t * , V * )||α⟩)||e * ⟩ ↣ ⟨π 2 (t * , V * )||e * ⟩ = ⟨µα .⟨(t * , V * )|| μ(a 1 , a 2 ).⟨a 2 ||α⟩⟩||e * ⟩ = ⟨(t * , V * )|| μ(a 1 , a 2 ).
□

Using the normalization, we can finally prove the soundness of the system.

Theorem 2.14 (Soundness). For any p ∈ dL, we have ⊬ p : ⊥ .

Proof. We actually start by proving by contradiction that a command c ∈ dL cannot be welltyped with empty contexts. Indeed, let us assume that there exists such a command c : (⊢). By normalization, we can reduce it to c ′ = ⟨p ′ ||e ′ ⟩ in normal form and for which we have c ′ : (⊢) by subject reduction. Since c ′ cannot reduce and is well-typed, p ′ is necessarily a value and cannot be a free variable. Thus, e ′ cannot be of the shape μa.c ′′ and every other possibility is either ill-typed or admits a reduction, which are both absurd.

We can now prove the soundness by contradiction. Assuming that there is a proof p such that ⊢ p : ⊥, we can form the well-typed command ⟨p||⋆⟩ : (⊢ ⋆ : ⊥) where ⋆ is any fresh α-variable. The previous result shows that p cannot drop the context ⋆ when reducing, since it would give rise to the command c : (⊢). We can still reduce ⟨p||⋆⟩ to a command c in normal form, and see that c has to be of the shape ⟨V ||⋆⟩ (by the same kind of reasoning, using the fact that c cannot reduce and that c : (⊢ ⋆ : ⊥) by subject reduction). Therefore, V is a value of type ⊥. Since there is no typing rule that can give the type ⊥ to a value, this is absurd. □

Toward a continuation-passing style translation

The difficulties we encountered while defining our system mostly came from the interaction between classical control and dependent types. Removing one of these two ingredients leaves us with a sound system in both cases. Without dependent types, our calculus amounts to the usual λµ μ-calculus. And without classical control, we would obtain an intuitionistic dependent type theory that we could easily prove sound.

To prove the correctness of our system, we might be tempted to define a translation to a subsystem without dependent types, or without classical control. We will discuss later in Section 5 a solution to handle the dependencies. We will focus here on the possibility of removing the classical part from dL, that is to define a translation that gets rid of the classical control. The use of continuationpassing style translations to address this issue is very common, and it was already studied for the simply-typed λµ μ-calculus [START_REF] Curien | The duality of computation[END_REF]. However, as it is defined to this point, dL is not suitable for the design of a CPS translation.

Indeed, in order to fix the problem of desynchronization of typing with respect to the execution, we have added an explicit list of dependencies to the type system of dL. Interestingly, if this solved the problem inside the type system, the very same phenomenon happens when trying to define a CPS translation carrying the type dependencies. Let us consider, as discussed in Section 2.5, the case of a command ⟨q|| μa.⟨p||e⟩⟩ with p : B[a] and e : B[q]. Its translation is very likely to look like:

q μa.⟨p||e⟩ = q (λa.( p e )),
where p has type (B[a] → ⊥) → ⊥ and e type B[q] → ⊥, hence the sub-term p e will be ill-typed. Therefore, the fix at the level of typing rules is not satisfactory, and we need to tackle the problem already within the reduction rules.

We follow the idea that the correctness is guaranteed by the head-reduction strategy, preventing ⟨p||e⟩ from reducing before the substitution of a was made. We would like to ensure that the same thing happens in the target language (that will also be equipped with a head-reduction strategy), namely that p cannot be applied to e before q has furnished a value to substitute for a. This would correspond informally to the term 16 :

( q (λa. p )) e .

Assuming that q eventually produces a value V , the previous term would indeed reduce as follows:

( q (λa. p )) e → ((λa. p ) V ) e → p [ V /a] e
Since p [ V /a] now has a type convertible to (B[q] → ⊥) → ⊥, the term that is produced in the end is well-typed.

The first observation is that if q, instead of producing a value, was a classical proof throwing the current continuation away (for instance µα .c where α FV (c)), this would lead to the unsafe reduction:

(λα . c (λa. p )) e → c e . Indeed, through such a translation, µα would only be able to catch the local continuation, and the term would end in c e instead of c . We thus need to restrict ourselves at least to proof terms that could not throw the current continuation.

The second observation is that such a term suggests the use of delimited continuations 17 to temporarily encapsulate the evaluation of q when reducing such a command: ⟨λa.p||q • e⟩ ⇝ ⟨µ t p.⟨q|| μa.⟨p|| t p⟩⟩||e⟩.

Under the guarantee that q will not throw away the continuation 18 μa.⟨p|| t p⟩, this command is safe and will mimic the aforedescribed reduction:

⟨µ t p.⟨q|| μa.⟨p|| t p⟩⟩||e⟩ ⇝ ⟨µ t p.⟨V || μa.⟨p|| t p⟩⟩||e⟩ ⇝ ⟨µ t p.⟨p[V /a]|| t p⟩||e⟩ ⇝ ⟨p[V /a]||e⟩.
This will also allow us to restrict the use of the list of dependencies to the derivation of judgments involving a delimited continuation, and to fully absorb the potential inconsistency in the type of t p. In Section 3, we will extend the language according to this intuition, and see how to design a continuation-passing style translation in Section 4.

EXTENSION OF THE SYSTEM

Limits of the value restriction

In the previous section, we strictly restricted the use of dependent types to proof terms that are values. In particular, even though a proof term might be computationally equivalent to some value (say µα .⟨V ||α⟩ and V for instance), we cannot use it to eliminate a dependent product, which is unsatisfactory. We will thus relax this restriction to allow more proof terms within dependent types. 16 We will see in Section 4.4 that such a term could be typed by turning the type A → ⊥ of the continuation that q is waiting for into a (dependent) type Π a:A R[a] parameterized by R. This way we could have q : ∀R .(Π a:A R[a] → R[q]) instead of q : ((A → ⊥) → ⊥). For R[a] := (B(a) → ⊥) → ⊥, the whole term is well-typed. Readers familiar with realizability will also note that such a term is realizable, since it eventually terminates on a correct term p[q/a] e . 17 We stick here to the presentations of delimited continuations in [START_REF] Ariola | A type-theoretic foundation of delimited continuations[END_REF][START_REF] Herbelin | An approach to call-by-name delimited continuations[END_REF], where t p is used to denote the top-level delimiter. 18 Otherwise, this could lead to an ill-formed command ⟨µ t p.c ||e ⟩ where c does not contain t p.

Proofs

p ::=

::= V | (t, p N ) | µ⋆.c N fragment | prf p N | subst p N q N c N ::= ⟨p N ||e N ⟩ e N ::= ⋆ | μa.c N (a) Language ⟨µα .c ||e⟩ ⇝ c[e/α] ⟨λa.p||q • e⟩ q ∈nef ⇝ ⟨µ t p.⟨q|| μa.⟨p|| t p⟩⟩||e⟩ ⟨λa.p||q • e⟩ ⇝ ⟨q|| μa.⟨p||e⟩⟩ ⟨λx .p||V t • e⟩ ⇝ ⟨p[V t /x]||e⟩ ⟨V p || μa.c⟩ ⇝ c[V p /a] ⟨(V t , p)||e⟩ p V ⇝ ⟨p|| μa.⟨(V t , a)||e⟩⟩ ⟨prf (V t , V p )||e⟩ ⇝ ⟨V p ||e⟩ ⟨prf p||e⟩ ⇝ ⟨µ t p.⟨p|| μa.⟨prf a|| t p⟩⟩||e⟩ ⟨subst p q||e⟩ p V ⇝ ⟨p|| μa.⟨subst a q||e⟩⟩ ⟨subst refl q||e⟩ ⇝ ⟨q||e⟩ ⟨µ t p.⟨p|| t p⟩||e⟩ ⇝ ⟨p||e⟩ c → c ′ ⇒ ⟨µ t p.c ||e⟩ ⇝ ⟨µ t p.c ′ ||e⟩ wit p → t ⇐ ∀α, ⟨p||α⟩ ⇝ ⟨(t, p ′ )||α⟩ t → t ′ ⇒ c[t] ⇝ c[t ′ ]
where: We can follow several intuitions. First, we saw at the end of the previous section that we could actually allow any proof term as long as its CPS translation uses its continuation and uses it only once. We do not have such a translation yet, but syntactically, these are the proof terms that can be expressed (up to α-conversion) in the λµ μ-calculus with only one continuation variable (that we write ⋆ in Figure 6), and which do not contain application 19 . We insist on the fact that this defines a syntactic subset of proofs. Indeed, ⋆ is only a notation and any proof defined with only one continuation variable is α-convertible to denote this continuation variable with ⋆. For instance, µα .⟨µβ ⟨V ||β⟩||α⟩ belongs to this category since: µα .⟨µβ .⟨V ||β⟩||α⟩ = α µ⋆.⟨µ⋆.⟨V ||⋆⟩||⋆⟩ Interestingly, this corresponds exactly to the so-called negative-elimination-free (nef) proofs of Herbelin [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF]. To interpret the axiom of dependent choice, he designed a classical proof system with dependent types in natural deduction, in which the dependent types allow the use of nef proofs.

V t ::= x | n V p ::= a | λa.p | λx .p | (V t , V p ) | refl c[t] ::= ⟨(t, p)||e⟩ | ⟨λx .p||t • e⟩ (b) Reduction rules
Second, Lepigre defined in recent work [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF] a classical proof system with dependent types, where the dependencies are restricted to values. However, the type system allows derivations of judgments up to an observational equivalence, and thus any proof computationally equivalent to a value can be used. In particular, any proof in the nef fragment is observationally equivalent to a value, and hence is compatible with the dependencies of Lepigre's calculus.

From now on, we consider the system dL of Section 2 extended with delimited continuations, which we call dL t p , and we define the fragment of negative-elimination-free proof terms (nef). The syntax of both categories is given by Figure 6, the proofs in the nef fragment are considered up 19 Indeed, λa .p is a value for any p, hence proofs like µα . ⟨λa .p ||q • α ⟩ can drop the continuation in the end once p becomes the proof in active position.

to α-conversion for the context variables 20 . The reduction rules, given in Figure 6, are slightly different from the rules in Section 2. In the case ⟨λa.p||q • e⟩ with q ∈ nef (resp. ⟨prf p||e⟩), a delimited continuation is now produced during the reduction of the proof term q (resp. p) that is involved in the list of dependencies. As terms can now contain proofs which are not values, we enforce the call-by-value reduction by requiring that proof values only contain term values. We elude the problem of reducing terms, by defining meta-rules for them 21 . We add standard rules for delimited continuations [START_REF] Ariola | A type-theoretic foundation of delimited continuations[END_REF][START_REF] Herbelin | An approach to call-by-name delimited continuations[END_REF], expressing the fact that when a proof µ t p.c is in active position, the current context is temporarily frozen until c is fully reduced.

Delimiting the scope of dependencies

Regarding the typing rules, which are given in Figure7, we extend the set D to be the nef fragment: D ≜ nef and we now distinguish two modes. The regular mode corresponds to a derivation without dependency issues whose typing rules are the same as in Figure 4 without the list of dependencies; plus the new rule ( t p I ) for the introduction of delimited continuations. The dependent mode is used to type commands and contexts involving t p, and we use the symbol ⊢ d to denote these sequents. There are three rules: one to type t p, which is the only one where we use the dependencies to unify dependencies; one to type context of the form μa.c (the rule is the same as the former rule for μa.c in Section 2); and a last one to type commands ⟨p||e⟩, where we observe that the premise for p is typed in regular mode.

Additionally, we need to extend the congruence to make it compatible with the reduction of nef proof terms (that can now appear in types), we thus add the rules:

A[p] ▷ A[q]
if ∀α (⟨p||α⟩ ⇝ ⟨q||α⟩) A[⟨q|| μa.⟨p||⋆⟩⟩] ▷ A[⟨p[q/a]||⋆⟩] with p, q ∈ nef Due to the presence of nef proof terms (which contain a delimited form of control) within types and lists of dependencies, we need the following technical lemma to prove subject reduction. Lemma 3.1. For any context Γ, ∆, any type A and any e, µ⋆.c:

⟨µ⋆.c ||e⟩ : Γ ⊢ d ∆, t p : B; ε ⇒ c[e/⋆] : Γ ⊢ d ∆, t p : B; ε.
Proof. By definition of the nef proof terms, µ⋆.c is of the general form µ⋆.c = µ⋆.⟨p 1 || μa 1 .⟨p 2 || μa 2 .⟨. . .|| μa n-1 .⟨p n ||⋆⟩⟩⟩⟩. For simplicity reasons, we will only give the proof for the case n = 2, so that a derivation for the hypothesis is of the form (we assume the Thus, we have to show that we can turn Π e into a derivation Π ′ e of Γ | e : A ⊢ d ∆ t p ; {a 1 |p 1 }{•|p 2 } with ∆ t p ≜ ∆, t p : B, since this would allow us to build the following derivation:

Π 1 Γ ⊢ p 1 : A 1 | ∆ Π 2 Γ, a 1 : A 1 ⊢ p 2 : A | ∆ Π ′ e • • • | e : A ⊢ d ∆ t p ; {a 1 |p 1 }{•|p 2 } ⟨p 2 ||⋆⟩ : Γ, a 1 : A 1 ⊢ ∆ t p ; {a 1 |p 1 } (Cut) Γ | μa 1 .⟨p 2 ||e⟩ : A 1 ⊢ d ∆ t p ; {•|p 1 } ( μ) ⟨p 1 || μa 1 .⟨p 2 ||e⟩⟩ : Γ ⊢ d ∆ t p ; ε (Cut)
It suffices to prove that if the list of dependencies is used in Π e to type t p, we can still give a derivation with the new one. In practice, it corresponds to showing that for any variable a and any list of dependencies σ :

{a|µ⋆.c}σ ⇛ {a 1 |p 1 }{a|p 2 }σ .
For any A ∈ B σ , by definition we have:

A[µ⋆.⟨p 1 || μa 1 .⟨p 2 ||⋆⟩⟩/b] ≡ A[µ⋆.⟨p 2 [p 1 /a 1 ]||⋆⟩/b] ≡ A[p 2 [p 1 /a 1 ]/b] = A[p 2 /b][p 1 /a 1 ].
Hence for any A ∈ B {a |µ⋆.c }σ , there exists A ′ ∈ B {a 1 |p 1 } {a |p 2 }σ such that A ≡ A ′ , and we can derive:

A ′ ∈ B {a 1 |p 1 } {a |p 2 }σ Γ | t p : A ′ ⊢ d ∆, t p : B; {a 1 |p 1 }{b|p 2 }σ A ≡ A ′ Γ | t p : A ⊢ d ∆, t p : B; {a 1 |p 1 }{b|p 2 }σ (≡ l )

□

We can now prove subject reduction for dL t p .

Theorem 3.2 (Subject reduction). If c, c ′ are two commands of dL t p such that c : (Γ ⊢ ∆) and c ⇝ c ′ , then c ′ : (Γ ⊢ ∆).

Proof. Actually, the proof is slightly easier than for Theorem 2.9, because most of the rules do not involve dependencies. We only give some key cases.

• Case ⟨λa.p||q • e⟩ ⇝ ⟨µ t p.⟨q|| μa.⟨p|| t p⟩⟩||e⟩ with q ∈ nef.

A typing derivation for the command on the left is of the form:

Π p Γ, a : A ⊢ p : B | ∆ Γ ⊢ λa.p : Π a:A B | ∆ (→ l ) Π q Γ ⊢ q : A | ∆ Π e Γ | e : B[q/a] ⊢ ∆ Γ | q • e : Π a:A B ⊢ ∆ (→ l ) ⟨λa.p||q • e⟩ : Γ ⊢ ∆ (Cut) • Case ⟨µ t p.c ||e⟩ ⇝ ⟨µ t p.c ′ ||e⟩ with c ⇝ c ′ .
This case corresponds exactly to Theorem 2.9, except for the rule ⟨µα .c ||e⟩ ⇝ c[e/α], since µα .c is a nef proof term (remember we are inside a delimited continuation), but this corresponds precisely to Lemma 3.1.

□

Remark 3.3. Interestingly, we could have already taken D ≜ nef in dL and still be able to prove the subject reduction property. The only difference would have been for the case ⟨µα .c ||e⟩ ⇝ c[e/α] when µα .c is nef. Indeed, we would have had to prove that such a reduction step is compatible with the list of dependencies, as in the proof for dL t p , which essentially amounts to Lemma 3.1. This shows that the relaxation to the nef fragment is valid even without delimited continuations.

To sum up, the restriction to nef is sufficient to obtain a sound type system, but is not enough to obtain a calculus suitable for a continuation-passing style translation. As we will now see, delimited continuations are crucial for the soundness of the CPS translation. Observe that they also provide us with a type system in which the scope of dependencies is more delimited.

A CONTINUATION-PASSING STYLE TRANSLATION

We shall now see how to define a continuation-passing style translation from dL t p to an intuitionistic type theory, and use this translation to prove the soundness of dL t p . Continuation-passing style translations are indeed very useful to embed languages with classical control into purely functional ones [START_REF] Curien | The duality of computation[END_REF][START_REF] Griffin | A formulae-as-type notion of control[END_REF]. From a logical point of view, they generally amount to negative translations that allow us to embed classical logic into intuitionistic logic [START_REF] Ferreira | On various negative translations[END_REF]. Yet, we know that removing classical control (i.e. classical logic) from our language leaves us with a sound intuitionistic type theory. We will now see how to design a CPS translation for our language which will allow us to prove its soundness.

Target language

We choose the target language to be an intuitionistic theory in natural deduction that has exactly the same elements as dL t p , except the classical control. The language distinguishes between terms (of type N) and proofs, it also includes dependent sums and products for types referring to terms, as well as a dependent product at the level of proofs. As is common for CPS translations, the evaluation follows a head-reduction strategy. The syntax of the language and its reduction rules are given by Figure 8.

The type system, also presented in Figure 8, is defined as expected, with the addition of a secondorder quantification that we will use in the sequel to refine the type of translations of terms and nef proofs. As in dL t p , the type system has a conversion rule, where the relation A ≡ B is the symmetric-transitive closure of A ▷ B, defined once again as the congruence over the reduction -→ and by the rules:

0 = 0 ▷ ⊤ 0 = S(u) ▷ ⊥ S(t) = 0 ▷ ⊥ S(t) = S(u) ▷ t = u.

Translation of proofs and terms

We can now define the continuation-passing style translation of terms, proofs, contexts and commands. The translation is given in Figure 9, in which we tag some lambdas with a bullet λ • for technical reasons. The translation of delimited continuations follows the intuition we presented in Section 2.8, and the definition for stacks t • e and q • e (with q nef) inlines the reduction producing a command with a delimited continuation. All the other rules are natural in the sense that they

Γ ⊢ q : t = u Γ ⊢ q : A[t] Γ ⊢ subst p q : A[u] (subst) Γ ⊢ p : A A ≡ B Γ ⊢ p : B (CONV)
(c) Type system reflect the reduction rule ⇝, except for the translation of pairs (t, p):

(t, p) p ≜ λk. p p ( t t (λxa.k (x, a)))
The natural definition would have been λk. t t (λu. p p λq.k (u, q)), however such a term would have been ill-typed (while the former definition is correct, as we will see in the proof of Lemma 4.9). Indeed, the type of p p depends on t, while the continuation (λq.k (u, q)) depends on u, but both become compatible once u is substituted by the value return by t t . This somewhat strange definition corresponds to the intuition that we reduce t t within a delimited continuation 22 , in order to guarantee that we will not reduce p p before t t has returned a value to substitute for u.

The complete translation is given in Figure 9. Before defining the translation of types, we first state a lemma expressing the fact that the translations of terms and nef proof terms use the continuations they are given once and only once. In particular, it makes them compatible with delimited continuations and a parametric return type. This will allow us to refine the type of their translation. Lemma 4.1. The translation satisfies the following properties:

(1) For any term t in dL t p , there exists a term t + such that for any k, we have t t k → * β k t + . (2) For any nef proof p N , there exists a proof p + N such that for any k, we have

p N p k → * β k p + N . wit p t ≜ λk. p p (λ • q.k (wit q)) V t V t ≜ λk.k V t a V ≜ a λa.p V ≜ λ • a. p p (V t , V p ) V ≜ ( V t V t , V V ) V p ≜ λk.k V V µα .c p ≜ λ • α . c c prf p p ≜ λ • k.( p p (λ • qλk ′ .k ′ (prf q))) k (t, p) p ≜ λ • k. p p ( t t (λxλ • a.k (x, a))) subst V q p ≜ λk. q p (λ • q ′ .k (subst V V q ′ ))) subst p q p ≜ λk. p p (λ • p ′ . q p (λ • q ′ .k (subst p ′ q ′ ))) (p V ) α e ≜ α t • e e ≜ λp.( t t (λ • v.p v)) e e q N • e e ≜ λp.( q N p (λ • v.p v)) e e (q N ∈ nef) q • e e ≜ λ • p. q p (λ • v.p v e e ) ( q
n V t ≜ n x V t ≜ x refl V ≜ refl λx .p V ≜ λ • x . p p µ t p.c p ≜ λk. c t p k μa.c e ≜ λ • a. c c ⟨p|| t p⟩ t p ≜ p p μa.c e t p ≜ λ • a. c t p

Fig. 9. Continuation-passing style translation

In particular, we have :

t t λx .x → * β t + and p N p λa.a → * β p + N
Proof. Straightforward mutual induction on the structure of terms and nef proofs, adding similar induction hypothesis for nef contexts and commands. The terms t + and proofs p + are given in Figure 10. We detail the case (t, p) with p ∈ nef to give an insight of the proof. Proof. Simple proof by induction on the reduction rules for ⇝, using Lemma 4.1 for cases involving a term t. □

(t, p) p k → β p p ( t t (λxa.k (x, a))) → β ( t t (λxa.k (x, a))) p + → β (λxa.k (x, a)) t + p + → β (λa.k (t + , a)) p + → β k (t + , p + ) ( by
x + ≜ x n + ≜ n (wit p) + ≜ wit p + a + ≜ a refl + ≜ refl (λa.p) + ≜ λa. p p (λx .p) + ≜ λx . p p (t, p) + ≜ (t + , p + ) (prf p) + ≜ prf p + (subst p q) + ≜ subst p + q + (µ⋆.c) + ≜ c + (µ t p.c) + ≜ c + (⟨p||⋆⟩) + ≜ p + (⟨p|| t p⟩) + ≜ p + (⟨p|| μa.c t p ⟩) + ≜ c + [p + /a]

Normalization of dL t p

We can in fact prove a finer result to show that normalization is preserved through the translation. Namely, we want to prove that any infinite reduction sequence in dL t p is responsible for an infinite reduction sequence through the translation. Using the preservation of typing (Proposition 4.10) together with the normalization of the target language, this will give us a proof of the normalization of dL t p for typed proof terms.

To this purpose, we roughly proceed as follows:

(1) we identify a set of reduction steps in dL t p which are directly reflected into a strictly positive number of reduction steps through the CPS;

(2) we show that the other steps alone can not form an infinite sequence of reductions;

(3) we deduce that every infinite sequence of reductions in dL t p gives rise to an infinite sequence through the translation. The first point corresponds thereafter to Proposition 4.5, the second one to the Proposition 4.6. As a matter of fact, the most difficult part is somehow anterior to these points. It consists in understanding how a reduction step can be reflected through the translation in a way that is sufficient to ensure the preservation of normalization (that is the third point). Instead of stating the result directly and giving a long and tedious proof of its correctness, we will rather sketch its main steps.

First of all, we split the reduction rule → β into two different kinds of reduction steps:

• administrative reductions, that we denote by -→ a , which correspond to continuationpassing and computationally irrelevant (w.r.t. to dL t p ) reduction steps. These are defined as the β-reduction steps of non-annotated λs. • distinguished reductions, that we denote by -→ • , which correspond to the image of a reduction step through the translation. These are defined as every other rules, that is to say the β-reduction steps of annotated λ • 's plus the rules corresponding to redexes formed with wit, prf and subst . In other words, we define two deterministic reductions -→ • and -→ a , such that the usual weakhead reduction → β is equal to the union -→ • ∪ -→ a . Our goal will be to prove that every infinite reduction sequence in dL t p will be reflected in the existence of an infinite reduction sequence for -→ • .

Second, let us assume for a while that we can show that for any reduction c ⇝ c ′ , through the translation we have:

c c t 0 t 1 t 2 c ′ c β * a * • 1 β * 1:30

Étienne Miquey

Then by induction, it implies that if a command c 0 produces an infinite reduction sequence c 0 ⇝ c 1 ⇝ c 2 ⇝ . . ., it is reflected through the translation by the following reduction scheme: Using the fact that all reductions are deterministic, and that the arrow from c 1 c to t 02 (and c 2 c to t 12 and so on) can only contain steps of the reduction -→ a , the previous scheme in fact ensures us that we have:

c
c 0 c t 00 t 01 t 02 t 10 t 11 t 12 t 20 t 21 c 1 c c 2 c β * a * a * • 1 β * β * • 1 β * β * • 1
This directly implies that c 0 c produces an infinite reduction sequence and thus is not normalizing. This would be the ideal situation, and if the aforementioned steps were provable as such, the proof would be over. Yet, our situation is more subtle, and we need to refine our analysis to tackle the problem. We shall briefly explain now why we can actually consider a slightly more general reduction scheme, while trying to remain concise on the justification. Keep in mind that our goal is to preserve the existence of an infinite sequence of distinguished steps. The first generalization consists in allowing distinguished reductions for redexes that are not in head positions. The safety of this generalization follows from this proposition: Proof. By induction on the structure of t, a very similar proof can be found in [START_REF] Joachimski | Short proofs of normalization for the simply-typed λ-calculus, permutative conversions and gödel's t[END_REF]. □

Following this idea, we define a new arrow ? -→ • by:

u -→ • u ′ ⇒ t[u] ? -→ • t[u ′ ]
where t[] ::

= [] | t ′ (t[]) | λx .t[],
expressing the fact that a distinguished step can be performed somewhere in the term. We denote by -→ β + the extended reduction relation defined as the union -→ β ∪ ? -→ • , which is not deterministic. Coming back to the thread scheme we described above, we can now generalize it with this arrow. Indeed, as we are only interested in getting an infinite reduction sequence from c 0 c , the previous proposition ensures us that if t 02 (t 12 , etc.) does not normalize, it is enough to have an arrow t 01 * -→ β + t 02 (t 11 * -→ β + t 12 , etc.) to deduce that t 01 does not normalize either. Hence, it is enough to prove that we have the following thread scheme, where we took advantage of this observation:

c 0 c t 00 t 01 t 02 t 10 t 11 t 12 t 20 t 21 c 1 c c 2 c β * β * β * a * a * • 1 β + * • 1 β + * • 1
In the same spirit, if we define = a to be the congruence over terms induced by administrative reductions -→ a , we can show that if a term has a redex for the distinguished relation in head position, then so does any (administratively) congruent term. -→ • u and t = a t ′ , then there exists u ′ such that t ′ 1 -→ • u ′ and u = a u ′ .

Proof. By induction on t, observing that an administrative reduction can neither delete nor create redexes for -→ • . □

In other words, as we are only interested in the distinguished reduction steps, we can take the liberty to reason modulo the congruence = a . Notably, we can generalize one last time our reduction scheme, replacing the left (administrative) arrow from c i c by this congruence:

c 0 c t 00 t 01 t 02 t 10 t 11 t 12 t 20 t 21 c 1 c c 2 c β * β * β * a a • 1 β + * • 1 β + * • 1
For all the reasons explained above, such a reduction scheme ensures that there is an infinite reduction sequence from c 0 c . Because of this guarantee, by induction, it is enough to show that for any reduction step c 0 ⇝ c 1 , we have:

c 0 c t 0 t 1 t 2 c 1 c β * • 1 β + * a (1)
In fact, as explained in the preamble of this section, not all reduction steps can be reflected this way through the translation. There are indeed 4 reduction rules, that we identify hereafter, that might only be reflected into administrative reductions, and produce a scheme of this shape (which subsumes the former):

c 0 c * -→ β + t = a c 1 c (2)
This allows us to give a more precise statement about the preservation of reduction through the CPS translation.

Proposition 4.5 (Preservation of reduction). Let c 0 , c 1 be two commands of dL t p . If c 0 ⇝ c 1 , then it is reflected through the translation into a reduction scheme (1), except for the rules:

⟨subst p q||e⟩ p V ⇝ ⟨p|| μa.⟨subst a q||e⟩⟩ ⟨subst refl q||e⟩ ⇝ ⟨q||e⟩ ⟨µ t p.⟨p|| t p⟩||e⟩ ⇝ ⟨p||e⟩ c[t] ⇝ c[t ′ ]
which are reflected into the reduction scheme (2).

Proof. The proof is done by induction on the reduction ⇝ (see Figure 6). To ease the notations, we will often write λ

• v.(λ • x . p p ) v -→ • λ • x . p p where we perform α-conversion to identify λ • v. p p [v/x]
and λ • x . p p . Additionally, to facilitate the comprehension of the steps corresponding to the congruence = a , we use an arrow ? -→ a to denote the possibility of performing an administrative reduction not in head position, defined by:

u -→ a u ′ ⇒ t[u] ? -→ a t[u ′ ]
We write -→ a + the union -→ a ∪ ? -→ a .

• Case ⟨µα .c ||e⟩ ⇝ c[e/α]:

We have:

⟨µα .c ||e⟩ c = (λ • α . c c ) e e -→ • c c [ e e /α] = c[e/α] c
• Case ⟨λa.p||q • e⟩ ⇝ ⟨q|| μa.⟨p||e⟩⟩:

We have:

⟨λa.p||q • e⟩ c = (λk.k (λ • a. p p )) λ • p. q p (λ • v.p v e e ) -→ a (λ • p. q p (λ • v.p v e e )) λ • a. p p -→ • q p (λ • v.(λ • a. p p ) v e e ) ? -→ • q p (λ • a. p p e e ) = ⟨q|| μa.⟨p||e⟩⟩ c • Case ⟨λa.p||q N • e⟩ q N ∈nef
⇝ ⟨µ t p.⟨q N || μa.⟨p|| t p⟩⟩||e⟩: We know by Lemma 4.1 that q N being nef, it will use, and use only once, the continuation it is applied to. Thus, we know that if k -→ • k ′ , we have that:

q N p k * -→ β k q + N -→ • k ′ q + N β ←-q N p k ′
and we can legitimately write q N p k -→ • q N p k ′ in the sense that it corresponds to performing now a reduction that would have been performed in the future. Using this remark, we have:

⟨λa.p||q N • e⟩ c = (λk.k (λ • a. p p )) λp.( q N p (λ • v.p v)) e e 2 -→ a ( q N p (λ • v.(λ • a. p p ) v)) e e -→ • ( q N p (λ • a. p p )) e e a ←-(λk.( q N p (λ • a. p p )) k) e e = ⟨µ t p.⟨q N || μa.⟨p|| t p⟩⟩||e⟩ c • Case ⟨λx .p||V t • e⟩ ⇝ ⟨p[V t /x]||e⟩: Since V t is a value (i.e. x or n), we have V t t = λk.k V t V t .
In particular, it is easy to deduce that p[V t /x] p = p p [ V t V t /x], and then we have:

⟨λx .p||V t • e⟩ c = (λk.k (λ • x . p p ))λp.( V t t (λ • v.p v)) e e 2 -→ a ( V t t (λ • v.(λ • x . p p ) v)) e e -→ a ((λ • v.(λ • x . p p ) v) V t V t ) e e -→ • ((λ • x . p p ) V t V t ) e e -→ • ( p p [ V t V t /x]) e e = p[V t /x] p e e = ⟨p[V t /x]||e⟩ • Case ⟨V || μa.c⟩ ⇝ c[V /a]:
Similarly to the previous case, we have

V p = λk.k V V and thus c[V /x] c = p p [ V V /a]. ⟨V p || μa.c⟩ c = (λk.k V V )λ • a. c c -→ a (λ • a. c c ) V V -→ • c c [ V V /a] = c[V /a] c • Case ⟨(V t , p)||e⟩ p V ⇝ ⟨p|| μa.⟨(V t , a)||e⟩⟩: We have : ⟨(V t , p)||e⟩ c = (λ • k. p p ( V t t (λxλ • a.k (x, a))) e e -→ • p p ( V t t (λxλ • a. e e (x, a))) -→ a + p p ((λxλ • a. e e (x, a)) V t V t ) -→ a + p p (λ • a. e e ( V t V t , a)) a +←-p p (λ • a. (V t , a) p e e ) a +←-(λk p p (λ • a. (V t , a) p k)) e e = ⟨p|| μa.⟨(V t , a)||e⟩⟩ c
• Case ⟨prf p||e⟩ ⇝ ⟨µ t p.⟨p|| μa.⟨prf a|| t p⟩⟩||e⟩:

We have:

⟨prf p)||e⟩ c = λ • k.( p p (λ • aλk ′ .k ′ (prf a))) k) e e -→ • ( p p (λ • a.λk ′ .k ′ (prf a))) e e a ←-(λk.( p p (λ • a.λk ′ .k ′ (prf a))) k) e e = ⟨µ t p.⟨p|| μa.⟨prf a|| t p⟩⟩||e⟩ c • Case ⟨prf (V t , V p )||e⟩ ⇝ ⟨V p ||e⟩:
We have:

⟨prf (V t , V p )||e⟩ c = λ • k.((λk.k ( V t V , V p V )) (λ • qλk ′ .k ′ (prf q))) k) e e -→ • ((λk.k ( V t V , V p V )) (λ • qλk ′ .k ′ (prf q))) e e -→ a ((λ • qλk ′ .k ′ (prf q))( V t V , V p V )) e e -→ • (λk ′ .k ′ (prf ( V t V , V p V ))) e e -→ a e e (prf ( V t V , V p V ))) ? -→ • e e V p V a ←-⟨V p ||e⟩ c • Case ⟨subst p q||e⟩ p V
⇝ ⟨p|| μa.⟨subst a q||e⟩⟩: We have:

⟨subst p q||e⟩ c = (λk. p p (λ • a. q p (λ • q ′ .k (subst a q ′ )))) e e -→ a p p (λ • a. q p (λ • q ′ . e e (subst a q ′ ))) ? a ←-p p (λ • a.(λk. q p (λ • q ′ .k (subst a q ′ ))) e e ) = ⟨p|| μa.⟨subst a q||e⟩⟩ c
• Case ⟨subst refl q||e⟩ ⇝ ⟨q||e⟩:

We have:

⟨subst refl q||e⟩ c = (λk. q p (λ • q ′ .k (subst refl q ′ ))) e e -→ a q p (λ • q ′ . e e (subst refl q ′ ))

?

-→ • q p (λ • q ′ . e e q ′ ) ? -→ • q p e e = ⟨q||e⟩ c

• Case ⟨µ t p.⟨p|| t p⟩||e⟩ ⇝ ⟨p||e⟩:

We have:

.c ′ ||e⟩ • Case t → t ′ ⇒ c[t] ⇝ c[t ′ ]:
As such, the translation does not allow an analysis of this case, mainly because we did not give an explicit small-step semantics for terms, and defined terms reduction through a big-step semantics:

∀α, ⟨p||α⟩ * ⇝ ⟨(t, q)||α⟩ ⇒ wit p → t However, we claim that we could have extended the language of dL t p with commands for terms:

c t ::= ⟨t
⟨V t || μx .c t ⟩ ⇝ c t [V t /x] ⟨wit (V t , V p )||e t ⟩ ⇝ ⟨V t ||e t ⟩ ⟨V p || μ ť p.⟨ ť p||e⟩⟩ ⇝ ⟨V p ||e⟩ c ⇝ c ′ ⇒ ⟨p|| μ ť p.c⟩ ⇝ ⟨p|| μ ť p.c ′ ⟩
It is worth noting that these rules simulate the big-step definitions we had before while preserving the global call-by-value strategy. Defining the translation for terms in the extended syntax:

wit V t t ≜ λk.k (wit V t V t ) wit p t ≜ λk. p p (λ • q.k (wit q)) μ ť p.c t t ≜ c t t μx .c t ≜ λ • x . c c ⟨t ||e t ⟩ t ≜ t t e t t ť p p ≜ λ • k.k
We can then prove that each reduction rule satisfies the expected scheme.

Case ⟨λx .p||t • e⟩ ⇝ ⟨µ t p.⟨t || μx .⟨p|| t p⟩⟩||e⟩:

We have: We have:

⟨λx .p||t • e⟩ = (λ • k.k λ • x . p p ) (
wit (V t , V p ) t e t t = (λk.k (wit ( V t V t , V p V ))) e t t -→ a e t t (wit ( V t V t , V p V )) -→ • e t t V t V t a ←-(λk.k V t V t ) e t t = V t t e t Case ⟨V t || μx .c t ⟩ ⇝ c t [V t /x]:
We have:

V t t μx .c t = (λk.k V t V t ) λ • x . c c -→ a (λ • x . c c ) V t V t -→ • c c [ V t V t /x] = c[V t /x] c
Case ⟨V || μ t p.⟨ t p||e⟩⟩ ⇝ ⟨V ||e⟩:

We have:

V p μ t p.⟨ t p||e⟩ e = (λk.k V V ) ((λk.k) e e ) -→ a ((λk.k) e e ) V V -→ a e e V V a ←-(λk.k V V ) e e = ⟨V ||e⟩ c Case c ⇝ c ′ ⇒ ⟨V || μ t p.c⟩ ⇝ ⟨V || μ t p.c ′ ⟩:
This case is similar to the case for delimited continuations proved before, we only need to use the induction hypothesis for c c to get:

V p μ t p.c e = (λk.k V V ) c c -→ a c c V V * -→ β + t V V = a c ′ c V V a +←-(λk.k V V ) c ′ c = V p μ t p.c ′ e □ Proposition 4.6.
There is no infinite sequence only made of reductions:

(1) ⟨subst p q||e⟩ p V ⇝ ⟨p|| μa.⟨subst a q||e⟩⟩ (2) ⟨subst refl q||e⟩ ⇝ ⟨q||e⟩

(3) ⟨µ t p.⟨p|| t p⟩||e⟩ ⇝ ⟨p||e⟩ (4)

c[t] ⇝ c[t ′ ]
Proof. It is sufficient to observe that if we define the following quantities:

(1) the quantity of subst p q with p not a value within a command, (2) the quantity of subst within a command, (3) the quantity of t p within a command, (4) the quantity of wit terms within a command. then the rule (1) makes quantity (1) decrease while preserving the others. Likewise, (2) decreases quantity (2) preserves the other, and so on. All in all, we have a bound on the maximal number of steps for the reduction restricted to these four rules. □ Proposition 4.7 (Preservation of normalization). If c c normalizes, then c is also normalizing.

Proof. Reasoning by contraposition, let us assume that c is not normalizing. Then in any infinite reduction sequence from c, according to the previous proposition, there are infinitely many steps that are reflected through the CPS into at least one distinguished step (Proposition 4.5). Thus, there is an infinite reduction sequence from c c too. □ Proof. Using the preservation of typing that we shall prove in the next section (Proposition 4.10), we know that if c is typed in dL t p , then its image c c is also typed. Using the fact that typed terms of the target language are normalizing, we can finally apply the previous proposition to deduce that c normalizes. □

Translation of types

We can now define the translation of types in order to show further that the translation p p of a proof p of type A is of type A * . The type A * is the double-negation of a type A + that depends on the structure of A. Thanks to the restriction of dependent types to nef proof terms, we can interpret a dependency in p (resp. t) in dL t p by a dependency in p + (resp. t + ) in the target language. Lemma 4.1 indeed guarantees that the translation of a nef proof p will eventually return p + to the continuation it is applied to. The translation is defined by:

A * ≜ ( A + → ⊥) → ⊥ t = u + ≜ t + = u + ∀x N .A + ≜ ∀x N . A * ⊤ + ≜ ⊤ ∃x N .A + ≜ ∃x N . A + ⊥ + ≜ ⊥ Π a:A B + ≜ Π a: A + B * N +
≜ N Observe that types depending on a term of type T are translated to types depending on a term of the same type T , because terms can only be of type N. As we shall discuss in Section 6.2, this will no longer be the case when extending the domain of terms.

To extend the translation for types to the translation of contexts, we consider that we can unify left and right contexts into a single one that is coherent with respect to the order in which the hypotheses have been introduced. We denote this context by Γ ∪ ∆, where the assumptions of Γ remain unchanged, while the former assumptions (α : A) in ∆ are denoted by (α : A ⊥ ⊥ ). The translation of unified contexts is given by:

Γ, a : A ≜ Γ + , a : A + Γ, x : N ≜ Γ + , x : N Γ, α : A ⊥ ⊥ ≜ Γ + , α : A + → ⊥.
As explained informally in Section 2.8 and stated by Lemma 4.1, the translation of a nef proof term p of type A uses its continuation linearly. In particular, this allows us to refine its type to make it parametric in the return type of the continuation. From a logical point of view, it amounts to replacing the double-negation (A → ⊥) → ⊥ by Friedman's translation [START_REF] Friedman | Classically and intuitionistically provably recursive functions[END_REF]: ∀R.(A → R) → R. It is worth noticing the correspondences with the continuation monad [START_REF] Filinski | Representing monads[END_REF]. Also, we make plain use here of the fact that the nef fragment is intuitionistic, so to speak. Indeed, it would be impossible to attribute this type 23 to the translation of a (really) classical proof.

Moreover, we can even make the return type of the continuation dependent on its argument (that is a type of the shape Π a:A R(a)), so that the type of p p will correspond to the elimination rule:

∀R.(Π a:A R(a) → R(p + )). This refinement will make the translation of nef proofs compatible with the translation of delimited continuations. Lemma 4.9 (Typing translation for nef proofs). The following holds:

(1) For any term t, if Γ ⊢ t : N | ∆ then Γ ∪ ∆ ⊢ t t : ∀X .(∀x N .X (x) → X (t + )).

(2) For any nef proof p, if Γ ⊢ p : A | ∆ then Γ ∪ ∆ ⊢ p p : ∀X .(Π a: A + X (a) → X (p + ))).

(3) For any nef command c, if c :

(Γ ⊢ ∆, ⋆ : B) then Γ ∪ ∆ , ⋆ : Π b:B + X (b) ⊢ c c : X (c + )).
Proof. The proof is done by induction on typing derivations. We only give the key cases of the proof.

• Case (µ). For this case, we could actually conclude directly using the induction hypothesis for c. Rather than that, we do the full proof for the particular case µ⋆.⟨p|| μa.⟨q||⋆⟩⟩, which condensates the proofs for µ⋆.c and the two possible cases ⟨p N ||e N ⟩ and ⟨p N ||⋆⟩ of nef commands. This case corresponds to the following typing derivation in dL t p :

Π p Γ ⊢ p : A | ∆ Π q Γ, a : A ⊢ q : B | ∆ • • • | ⋆ : B ⊢ ∆, ⋆ : B ⟨q||⋆⟩ : Γ, a : A ⊢ ∆, ⋆ : B
the reduction rules for the fragment of Lepigre's calculus we use, for the type system we refer the reader to [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]:

Values Terms Stacks Processes Formulas v, w ::= x | λx .t | {l 1 = v 1 , l 2 = v 2 } t, u ::= a | v | t u | µα .t | p | v.l i π , ρ ::= α | v • π | [t]π p, q ::= t * π A, B ::= X n (t 1 , . . . , t n ) | A → B | ∀a.A | ∃a.A | ∀X n .A | {l 1 : A 1 , l 2 : A 2 } | t ∈ A
The reduction ≻ is defined as the smallest relation satisfying:

t u * π ≻ u * [t]π v * [t]π ≻ t * v • π λx .t * v • π ≻ t[x := v] * π µα .t * π ≻ t[α := π ] * π p * π ≻ p (v 1 , v 2 ).l i ≻ v i
It is worth noting that the call-by-value strategy is obtained via the construction [t]π which allows to evaluate the argument of t to a value before pushing it onto the stack.

Even though records are only defined for values, we can define pairs and projections as syntactic sugar:

(

t 1 , t 2 ) ≜ (λv 1 v 2 .{l 1 = v 1 , l 2 = v 2 }) t 1 t 2 fst(t) ≜ (λx .(x .l 1 )) t snd(t) ≜ (λx .(x .l 2 )) t A 1 ∧ A 2 ≜ {l 1 : A 1 , l 2 : A 2 }
Similarly, only values can be pushed on stacks, but we can define processes 25 with stacks of the shape t • π as syntactic sugar:

t * u • π ≜ tu * π We first define the translation for types (extended for typing contexts) where the predicate Nat(x) is defined 26 as usual in second-order logic: Nat(x) ≜ ∀X .(X (0) → ∀y.(X (y) → X (S(y))) → X (x)) and t t is the translation of the term t given in Figure 11.

(∀x N .A) * ≜ ∀x .(Nat(x) → A * ) (∃x N .A) * ≜ ∃x .(Nat(x) ∧ A * ) (t = u) * ≜ ∀X .(X ( t t ) → X ( u t )) ⊤ * ≜ ∀X .(X → X ) ⊥ * ≜ ∀XY .(X → Y ) (Π a:A B) * ≜ ∀a.((a ∈ A * ) → B * ) (Γ, x : N) * ≜ Γ * , x : Nat(x) (Γ, a : A) * ≜ Γ * , a : A * (Γ, α : A ⊥ ⊥ ) * ≜ Γ * , α : ¬A *
Note that the equality is mapped to Leibniz equality, and that the definitions of ⊥ * and ⊤ * respectively correspond to (0 = 1) * and (0 = 0) * in order to make the conversion rule admissible through the translation.

The translation for terms, proofs, contexts and commands of dL t p , given in Figure 11 is almost straightforward. We only want to draw the reader's attention on a few points:

• the equality being translated as Leibniz equality, refl is translated as the identity λa.a, which also matches with ⊤ (α). By hypothesis, σ realizes Γ, α : A ⊥ ⊥ from which we obtain ασ = σ (α) ∈ A ⊥ σ .

( * ). We need to show that tσ * πσ ∈ B ⊥⊥ σ , so we take ρ ∈ B ⊥ σ and show that (tσ * πσ ) * ρ ∈ ⊥ ⊥. By anti-reduction, it is enough to show that (tσ * πσ ) ∈ ⊥ ⊥. This is true by induction hypothesis, since tσ ∈ A ⊥⊥ σ and πσ ∈ A ⊥ σ .

(µ). The proof is the very same as in [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]Theorem 6].

(∀ l ). By induction hypothesis, we have that πσ ∈ A[x := t] ⊥ σ . We need to show the inclusion

A[x := t] ⊥ σ ⊆ ∀x .A ⊥ σ , which follows from ∀x .A σ = t ∈Λ A[x := t] σ ⊆ A[x := t] σ .
(⇒ l ). If t is a value v, by induction hypothesis, we have that vσ ∈ A σ and πσ ∈ B ⊥ σ , and we need to show that vσ • πσ ∈ A ⇒ B ⊥ σ . The proof is already done in the case (⇒ e ) (see [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]Theorem 6]). Otherwise, by induction hypothesis, we have that tσ ∈ A ⊥⊥ σ and πσ ∈ B ⊥ σ , and we need to show that tσ • πσ ∈ A ⇒ B ⊥ σ . So we consider λx .u ∈ A ⇒ B σ , and show that λx .u * tσ • πσ ∈ ⊥ ⊥. We can take a reduction step, and prove instead that tσ * [λx .u]πσ ∈ ⊥ ⊥. This amounts to showing that [λx .u]π ∈ A ⊥ σ , which is already proven in the case (⇒ e ).

(let). We need to show that for all v ∈ A σ , v * [tσ ]πσ ∈ ⊥ ⊥. Taking a step of reduction, it is enough to have tσ * v •πσ ∈ ⊥ ⊥. This is true since by induction hypothesis, we have tσ ∈ A ⇒ B ⊥⊥ Proof. The proof is an easy induction on the typing derivation Γ ⊢ p : A | ∆. Note that in a way, the translation of a delimited continuation decompiles it to simulate in a natural deduction fashion the reduction of the applications of functions to stacks (that could have generated the same delimited continuations in dL t p ), while maintaining the frozen context (at top-level) outside of the active command (just like a delimited continuation would do). This trick allows us to avoid the problem of dependencies conflict in the typing derivation. For instance, assuming that q 1 p (resp.

q 2 p ) reduces to a value V 1 (resp. V 2 )
. p p [V 1 /a 1 ]] e e ≻ * p p [ V 1 p /a 1 ][ V 2 p /a 2 ] * e e * ≺ q 2 p * [λa 2 . p p [V 1 /a 1 ]] e e * ≺ q 1 p * [λa 1 a 2 . p p )] q 2 p • e e * ≺ (λa 1 a 2 . p p ) * q 1 p • q 2 p • e e = ⟨λa 1 λa 2 .p||q 1 • q 2 • e⟩ c
where we observe that e e is always kept outside of the computations, and where each command ⟨q i || μa i .c t p ⟩ is decompiled into (µα . q i p * [λa i . c t p t p ].α) * e e , simulating the (natural deduction style) reduction of λa i . c t p t p * q i p • e e . These terms correspond somehow to the translations of former commands typable without types dependencies. □

As a corollary we get a proof of the adequacy of dL t p typing rules with respect to Lepigre's realizability model. This immediately implies the soundness of dL t p : Theorem 5.4 (Soundness). For any proof p in dL t p , we have: ⊬ p : ⊥.

Proof. By contradiction, if we had a closed proof p of type ⊥, it would be translated as a realizer of ⊤ → ⊥. Therefore, p p λx .x would be a realizer of ⊥, which is impossible. □ Furthermore, the translation clearly preserves normalization (in the sense that for any c, if c does not normalize then neither does c c ), and thus the normalization of dL t p is a consequence of adequacy. It is worth noting that without delimited continuations, we would not have been able to define an adequate translation, since we would have encountered the same problem 27 than with a naive CPS translation (see Section 2.8).

FURTHER EXTENSIONS

As we explained in the preamble of Section 2, we defined dL and dL t p as small languages containing all the potential sources of inconsistency we wanted to mix: classical control, dependent types, and a sequent calculus presentation. It had the benefit to focus our attention on the difficulties inherent to the issue, but on the other hand, the language we obtain is far from being as expressive as other usual proof systems. We claimed our system to be extensible, thus we shall now discuss this matter.

Intuitionistic sequent calculus

There is not much to say on this topic, but it is worth mentioning that dL and dL t p could be easily restricted to obtain an intuitionistic framework. Indeed, just like for the passage from LK to LJ, it is enough to restrict the syntax of proofs to allow only one continuation variable (that is one conclusion on the right-hand side of sequent) to obtain an intuitionistic calculus. In particular, in such a setting, all proofs will be nef, and every result we obtained will still hold.

Extending the domain of terms

Throughout the paper, we only worked with terms of a unique type N, hence it is natural to wonder whether it is possible to extend the domain of terms in dL t p , for instance with terms in the simply-typed λ-calculus. A good way to understand the situation is to observe what happens through the CPS translation. We saw that a term t of type T = N is translated into a proof t * which is roughly of type T * = ¬¬T + = ¬¬N, from which we can extract a term t + of type N.

However, if T was for instance the function type N → N (resp. T → U ), we would only be able to extract a proof of type T + = N → ¬¬N (resp. T + → U * ). There is no hope in general to extract a function f : N → N from such a term, since such a proof could be of the form λx .p, where p might backtrack to a former position, for instance before it was extracted, and furnish another proof. Such a proof is no longer a witness in the usual sense, but rather a realizer of f ∈ N → N in the sense of Krivine classical realizability. This accounts for a well-know phenomenon in classical logic, where witness extraction is limited to formulas in the Σ 1 0 -fragment [START_REF] Miquel | Existential witness extraction in classical realizability and via a negative translation[END_REF]. It also corresponds to the type we obtain for the image of a dependent product Π a:A B, that is translated to a type ¬¬Π a:A + B * where the dependence is in a proof of type A + . This phenomenon is not surprising and was already observed for other CPS translations for type theories with dependent types [START_REF] Barthe | CPS translations and applications: The cube and beyond[END_REF].

Nevertheless, if the extraction is not possible in the general case, our situation is more specific. Indeed, we only need to consider proofs that are obtained as translation of terms, which can only contains nef proofs in dL t p . In particular, such proofs cannot drop continuations (remember that this was the whole point of the restriction to the nef fragment). Therefore, we could again refine the translation of types, similarly to what we did in Lemma 4.9. Once more, this refinement would also coincide with a computational property similar to Lemma 4.1, expressing the fact that the extraction can be done simply by passing the identity as a continuation 28 . This witnesses the fact that for any function t in the source language, there exists a term t + in the target language which represents the same function, even though the translation of t is a proof t .

To sum up, this means that we can extend the domain of terms in dL t p (in particular, it should affect neither the subject reduction property nor the soundness), but the stratification between terms and proofs is to be lost through a CPS translation. If the target language is a non-stratified type theory (most of the presentations of type theory correspond to this case), then it becomes possible to force the extraction of terms through the translation.

Another solution would consist in the definition of a separate translation for terms. Indeed, as it was reflected by Lemma 4.1, since neither terms nor nef proofs may contain continuations, they can be directly translated. The corresponding translation is actually an embedding which maps every pure term (without wit p) to itself, and which performs the reduction of nef proofs p to proofs p + so as to eliminate every µ binder. Such a translation would intuitively reflect an abstract machine where the reduction of terms (and the nef proofs inside) is performed in an external machine. If this solution is arguably a bit ad hoc, it is nonetheless correct and it is maybe a good way to take advantage of the stratified presentation.

Adding expressiveness

From the point of view of the proof language (that is of the tools we have to build proofs), dL t p only enjoys the presence of a dependent sum and a dependent product over terms, as well as a dependent product at the level of proofs (which subsumes the non-dependent implication). If this is obviously enough to encode the usual constructors for pairs (p 1 , p 2 ) (of type A 1 ∧ A 2 ), injections ι i (p) (of type A 1 ∨ A 2 ), etc..., it seems reasonable to wonder whether such constructors can be directly defined in the language of proofs. In fact, this is the case, and we claim that is possible to define the constructors for proofs (for instance (p 1 , p 2 )) together with their destructors in the contexts (in that case μ(a 1 , a 2 ).c), with the appropriate typing rules. In practice, it is enough to:

• extend the definitions of the nef fragment according to the chosen extension,

• extend the call-by-value reduction system, opening if needed the constructors to reduce them to a value, • in the dependent typing mode, make some pattern-matching within the list of dependencies for the destructors.

The soundness of such extensions can be justified either by extending the CPS translation, or by defining a translation to Lepigre's calculus (which already allows records and pattern-matching over general constructors) and proving the adequacy of the translation with respect to the realizability model.

For instance, for the case of the pairs, we can extend the syntax with: We then need to add the corresponding typing rules (plus a third rule to type μ(a 1 , a 2 ).c in regular mode):

Γ ⊢ p 1 : A 1 | ∆ Γ ⊢ p 2 : A 2 | ∆ Γ ⊢ (
)||e⟩⟩⟩ ⟨(V 1 , V 2 )|| μ(a 1 , a 2 ).c⟩ ⇝ c[V 1 /a 1 , V 2 /a 2 ]
We let the reader check that these rules preserve subject reduction, and suggest the following CPS translations:

(p 1 , p 2 ) p ≜ λ • k. p 1 p (λ • a 1 . p 2 p (λ • a 2 .k (a 1 , a 2 ))) (V 1 , V 2 ) V ≜ λ • k.k ( V 1 V , V 2 V ) μ(a 1 , a 2 )
.c e ≜ λp. split p as (a 1 , a 2 ) in c c which allow us to prove that the calculus remains correct with these extensions.

We claim that this methodology furnishes a good approach to handle the question "Can I extend the language with ... ?". In particular, it should be enough to get closer to a realistic programming language and extend the language with inductive fixed point operators 29 .

CONCLUSION

Several directions remain to be explored. We plan to investigate possible extensions of the syntactic restriction we defined, and its connections with notions such as Fürhmann's thunkability [START_REF] Führmann | Direct models for the computational lambda calculus[END_REF] or Munch-Maccagnoni's linearity [START_REF] Munch-Maccagnoni | Models of a Non-associative Composition[END_REF]. Moreover, it might be of interest to check whether this restriction could make dependent types compatible with other side effects, in presence of classical logic or not. More generally, we would like to better understand the possible connections between our calculus and the categorical models for dependently typed theory.

On a different perspective, the continuation-passing style translation we defined is at the best of our knowledge a novel contribution, even without considering the classical part. In particular, our translation allows us to use computations (as in the call-by-push value terminology) within dependent types with a call-by-value evaluation strategy, and without any thunking construction. It might be the case that this translation could be adapted to justify extensions of other dependently typed calculi, or provide typed translations between them.

Last but not least, we plan to present an application of dL t p to solve the problem that was our original motivation to design such a calculus. In [START_REF] Miquey | Classical realizability and side-effects[END_REF]Chapter 8], we present a sequent calculus equivalent to Herbelin's dPA ω [START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF], whose presentation is inspired from dL t p . This leads to the definition of a realizability model inspired from Lepigre's construction and from another technique developed with Herbelin [START_REF] Miquey | Realizability interpretation and normalization of typed call-by-need λ-calculus with control[END_REF] to give a realizability interpretation to calculi with laziness and memory sharing (two features of dPA ω ). As a consequence, we deduce the normalization and the soundness of our system.

  Proofs p ::= a | λa.p | µα .c ⟨p|| μa.c⟩ → c[a := p] p ∈ V Contexts e ::= α | p • e | μa.c ⟨µα .c ||e⟩ → c[α := e] e ∈ E Commands c ::= ⟨p||e⟩ ⟨λa.p||u • e⟩ → ⟨u || μa.⟨p||e⟩⟩ (a) Syntax (b) Reduction rules

Fig. 1 .

 1 Fig. 1. The λµ μ-calculus

Fig. 4 .

 4 Fig. 4. Typing rules of dL

Fig. 5 .

 5 Fig. 5. λµ μ-calculus with pairs

Theorem 2 . 13 .

 213 ⟨a 2 ||e * ⟩⟩ ↣ ⟨V * ||e * ⟩ = (⟨V ||e⟩) * • Case ⟨subst refl q||e⟩ ⇝ ⟨q||e⟩: (⟨subst refl q||e⟩) * = ⟨µα .⟨q * ||α⟩||e * ⟩ ↣ ⟨q * ||e * ⟩ = (⟨q||e⟩) * • Case ⟨subst p q||e⟩ ⇝ ⟨p|| μa.⟨subst a q||e⟩⟩ (with p V ): (⟨subst p q||e⟩) * = ⟨µα .⟨p * || μ_ .⟨µα .⟨q * ||α⟩||α⟩⟩||e * ⟩ ↣ ⟨p * || μ_ .⟨µα .⟨q * ||α⟩||e * ⟩⟩ ↣ ⟨µα .⟨q * ||α⟩||e * ⟩ = (⟨subst a q||e⟩) * □ If c : (Γ ⊢ ∆; ε), then c normalizes.

Fig. 6 .

 6 Fig. 6. dL t p : extension of dL with delimited continuations

Fig. 8 .

 8 Fig. 8. Target language

  definition) (by induction) (by induction) □ Moreover, we can verify that the translation preserves the reduction: Proposition 4.2. If c, c ′ are two commands of dL t p such that c ⇝ c ′ , then c c = β c ′ c

Fig. 10 .

 10 Fig. 10. Linearity of the translation for nef proofs

Proposition 4 . 3 .

 43 If u -→ • u ′ and t[u ′ ] does not normalize, then neither does t[u].

Proposition 4 . 4 .

 44 If t 1

•

  ⟨µ t p.⟨p|| t p⟩||e⟩ c = (λk. p p k) e e -→ a p p e e = ⟨p||e⟩ c Case c ⇝ c ′ ⇒ ⟨µ t p.c ||e⟩ ⇝ ⟨µ t p.c ′ ||e⟩: By induction hypothesis, we get that c c * -→ β + t = a c ′ c for some term t. Therefore, we have: ⟨µ t p.c ||e⟩ = (λk. c c k) e e -→ a c c e e * -→ β + t e e = a c ′ c e e a ←-(λk. c ′ c k) e e = ⟨µ t p

Theorem 4 . 8 (

 48 Normalization). If c : Γ ⊢ ∆, then c normalizes.

σ

  and πσ ∈ B ⊥ σ , thus v • πσ ∈ A ⇒ B ⊥ σ . □ It only remains to show that the translation we defined in Figure 11 preserves typing to conclude the proof of Proposition 5.3. Lemma 5.2. If Γ ⊢ p : A | ∆ (in dL t p ), then (Γ ∪ ∆) * ⊢ p p : A * (in Lepigre's extended system). The same holds for contexts, and if c : Γ ⊢ ∆ then (Γ ∪ ∆) * ⊢ c c : ⊥.

Proposition 5 . 3 (

 53 Adeqacy). If Γ ⊢ p : A | ∆ and σ is a substitution realizing (Γ ∪ ∆) * , then p p σ ∈ A * ⊥⊥ σ .

p

  ::= • • • | (p 1 , p 2 ) e ::= • • • | μ(a 1 , a 2 ).c

  • • • | µ t p.c t p Delimited c t p ::= ⟨p N ||e t p ⟩ | ⟨p|| t p⟩ continuations e t p ::= μa.c t p nef p N

  ||e t ⟩ e t ::= μx .c[t] c[] ::= ⟨([], p)||e⟩ | ⟨λx .p||[] • e⟩ and adding dual operators ť p/ μ ť p for (co-)delimited continuations to allow for a small-step definition of terms reduction: ⟨λx .p||t • e⟩ ⇝ ⟨µ t p.⟨t || μx .⟨p|| t p⟩⟩||e⟩ ⟨wit p||e t ⟩ ⇝ ⟨p|| μa.⟨wit a||e t ⟩⟩ ⟨(t, p)||e⟩ ⇝ ⟨p|| μ ť p.⟨t || μx .⟨ ť p|| μa.⟨(x, a)||e⟩⟩⟩⟩

  λp.( t t (λ • v.p v)) e e ) -→ • (λp.( t t (λ • v.p v)) e e ) λ • x . p p -→ a ( t t (λ • v.(λ • x . p p ) v))e e +←-λk.(( t t (λ • x . p )) k) e e = ⟨µ t p.⟨t || μx .⟨p|| t p⟩⟩||e⟩ c Case ⟨(t, p)||e⟩ ⇝ ⟨p|| μ ť p.⟨t || μx .⟨ ť p|| μa.⟨(x, a)||e⟩⟩⟩⟩: We have: ⟨(t, p)||e⟩ = (λ • k. p p ( t t (λx .λ • a.k (x, a)))) e e -→ • p p ( t t (λx .λ • a. e e (x, a))) a +←-p p ( t t (λx .(λk.k)λ • a. e e (x, a))) a +←-p p ( t t (λx .(λk.k)λ • a.(λk.k (x, a)) e e )) = ⟨p|| μ ť p.⟨t || μx .⟨ ť p|| μa.⟨(x, a)||e⟩⟩⟩⟩ c Case ⟨wit p||e t ⟩ ⇝ ⟨p|| μa.⟨wit a||e t ⟩⟩: We have: wit p t e t t = (λk. p p (λ • a.k (wit a))) e t t -→ a p p (λ • a. e t t (wit a))) a +←-p p (λ • a.(λk.k (wit a)) e t t ) = ⟨p|| μa.⟨wit a||e t ⟩⟩ c Case ⟨wit (V t , V p )||e t ⟩ ⇝ ⟨V t ||e t ⟩:

? -→ • ( t t (λ • x . p )) e e a

  • e e ≜ q p • e e t • e e ≜ t t • e e μa.c e ≜ [λa. c c ]• (•). By definition, we have ⊥ σ = ∀X .X σ = ∅, thus for any stack π , we have π ∈ ⊥ ⊥ σ = Π. In particular, • ∈ ⊥ ⊥ σ .

	x t	≜ x	(t, p) p	≜ ( t t , p p )	q
	n t	≜ λzs.s n (z)	µα .c p	≜ µα . c c
	wit p t ≜ π 1 ( p p )	prf p p	≜ π 2 ( p p )
	a p	≜ a	refl p	≜ λa.a
	λa.p p ≜ λa. p p	subst p q p ≜ p p q p
	λx .p p ≜ λx . p p	α e	≜ α

* ,

  we have: ⟨µ t p.⟨q 1 || μa 1 .⟨q 2 || μa 2 .⟨p|| t p⟩⟩⟩||e⟩ c = µα .(µα .( q 1 p * [λa 1 . ⟨q 2 || μa 2 .⟨p|| t p⟩⟩ t p ]α) * α) * e e ≻ µα .( q 1 p * [λa 1 . ⟨q 2 || μa 2 .⟨p|| t p⟩⟩ t p ]α) * e e ≻ q 1 p * [λa 1 . ⟨q 2 || μa 2 .⟨p|| t p⟩⟩ t p ] e e ≻ * q 2 p * [λa 2

  p 1 , p 2 ) : (A 1 ∧ A 2 ) | ∆ ∧ r c : Γ, a 1 : A 1 , a 2 : A 2 ⊢ d ∆, t p : B; σ {(a 1 , a 2 )|p} Γ | μ(a 1 , a 2 ).c : (A 1 ∧ A 2 ) ⊢ d ∆, t p : B; σ {•|p} ∧ land the reduction rules:⟨(p 1 , p 2 )||e⟩ ⇝ ⟨p 1 || μa 1 .⟨p 2 || μa 2 .⟨(a 1 , a 2

Aside from strictly logical considerations as in[START_REF] Herbelin | A constructive proof of dependent choice, compatible with classical logic[END_REF], there are motivating examples of programs that could only be written and specified in such a setting. Consider for instance the infinite tape lemma that states that from any infinite sequence of natural numbers, one can extract either an infinite sequence of odd numbers, or an infinite sequence of even numbers. Its proof deeply relies on classical logic, and the corresponding program (which, given as input a stream of integers, returns a stream that consists either only of odd integers or only of even ones) can only be written in a classical setting and requires dependent types to be specified. See[START_REF] Lepigre | Semantics and Implementation of an Extension of ML for Proving Programs[END_REF] Section 7.8] for more details.

In the sense of a formulas-as-types interpretation of a sequent calculus à la Hilbert (as Curien-Herbelin's λµ μ-calculus[START_REF] Curien | The duality of computation[END_REF] or Munch-Maccagnoni's system L[START_REF] Munch-Maccagnoni | Focalisation and Classical Realisability[END_REF]), as opposed to traditional type systems given in a natural deduction style.

This formula is often referred to as the formula in the stoup, a terminology due to Girard.

Observe that this critical pair can be also interpreted in terms of non-determinism. Indeed, we can define a fork instruction by ⋔≜ λab .µα . ⟨µ_⟨a ||α ⟩ || μ_. ⟨b ||α ⟩ ⟩, which verifies indeed that ⟨⋔||p 0 • p 1 • e ⟩ → ⟨p 0 ||e ⟩ and ⟨⋔||p 0 • p 1 • e ⟩ → ⟨p 1 ||e ⟩.

To pursue the analogy with the λ-calculus, the rest of the stack e can be viewed as a context C e [ ] surrounding the application p q, the command ⟨p ||q • e ⟩ thus being identified with the term C e [p q]. Similarly, the whole stack can be seen as the context C q•e [ ] = C e [[ ]q], whence the terminology.

Technically this requires to extend the language to authorize the construction of terms call/cc k t and of proofs throw t . The first rule expresses that call/cc k captures the context wit { } and replaces every occurrence of throw k t with throw k (wit t ). The second one just expresses the fact that call/cc k can be dropped when applied to a term t which does not contain the variable k .

This design choice is usually a matter of taste and might seem unusual for some readers. However, it has the advantage of exhibiting the different treatments for terms and proofs through the CPS in the next sections.

The nature of the representation is irrelevant here as we will not compute over it. We can for instance add one constant for each natural number.

The reader might recognize the rule (ς ) of Wadler's sequent calculus[START_REF] Wadler | Call-by-value is dual to call-by-name[END_REF].

Observe that the problem here arises independently of the value restriction (that is whether we consider that q is a value or not), and is peculiar to the sequent calculus presentation.

Note that even if we were not restricting ourselves to values, this would still hold: if at some point the command ⟨p ||e ⟩ is executed, it is necessarily the case that q has produced a value to substitute for a.

(µ) c : (Γ, a : A ⊢ ∆; σ {a|p}) Γ | μa.c : A ⊢ ∆; σ {•|p} ( μ) Γ, a : A ⊢ p : B | ∆; σ Γ ⊢ λa.p : Π a:A B | ∆; σ (→ r ) Γ ⊢ q : A | ∆; σ Γ | e : B[q/a] ⊢ ∆; σ {•| †} q D → a FV (B) Γ | q • e : Π a:A B ⊢ ∆; σ {•|p} (→ l ) Γ, x : N ⊢ p : A | ∆; σ Γ ⊢ λx .p : ∀x N .A | ∆; σ (∀ r ) Γ ⊢ t : N ⊢ ∆; σ Γ | e : A[t/x] ⊢ ∆; σ {•| †} Γ | t • e : ∀x N .A ⊢ ∆; σ {•|p} (∀ l ) Γ ⊢ t : N | ∆; σ Γ ⊢ p : A(t) | ∆; σ Γ ⊢ (t, p) : ∃x N .A(x) | ∆; σ (∃ r ) Γ ⊢ p : ∃x N .A(x) | ∆; σ p ∈ D Γ ⊢ prf p : A(wit p) | ∆; σ prf Γ ⊢ p : A | ∆; σ A ≡ B Γ ⊢ p : B | ∆; σ (≡ r ) Γ | e : A ⊢ ∆; σ A ≡ B Γ | e : B ⊢ ∆; σ (≡ l ) Γ ⊢ p : t = u | ∆; σ Γ ⊢ q : B[t/x] | ∆; σ Γ ⊢ subst p q : B[u/x] | ∆; σ (subst) Γ ⊢ t : N | ∆; σ Γ ⊢ refl : t = t | ∆; σ (refl) Γ, x : N ⊢ x : N | ∆; σ (Ax t ) n ∈ N Γ ⊢ n : N | ∆; σ(Ax n ) Γ ⊢ p : ∃x .A(x) | ∆; σ p ∈ D Γ ⊢ wit p : N | ∆; σ (wit)

In practice we will only bind a variable with a proof term, but it is convenient for proofs to consider this slightly more general definition.

It is easy to convince ourselves that when typing a command ⟨p ||q • μa .c ⟩ with {• |p }, the "correct" dependency within c should be {a |µα ⟨p ||q • α ⟩ }, where the right proof is not a value. Furthermore, this dependency is irrelevant since there is no way to produce such a command where a type adjustment with respect to a needs to be made in c.

That is to say let a = p 0 in subst (prf a) refl in natural deduction.

(≡ l )where the hypothesis A ≡ B is implicit.• Case ⟨λx .p||t • e⟩ ⇝ ⟨p[t/x]||e⟩.A typing proof for the command on the left-hand side is of the form:Π p Γ, x : N ⊢ p : A | ∆ Γ ⊢ λx .p : ∀x N .A | ∆ (∀ r ) Π t Γ ⊢ t : N | ∆ Π e Γ | e : B[t/x] ⊢ ∆; {•| †} Γ | t • e : ∀x N .B ⊢ ∆; {•|λx .p} (∀ l ) Γ | t • e : ∀x N .A ⊢ ∆; {•|λx .p} (≡ l ) ⟨λx .p||t • e⟩ : Γ ⊢ ∆ (Cut)We first deduce A[t/x] ≡ B[t/x] from the hypothesis ∀x N .A ≡ ∀x N .B. Then, using the fact that Γ, x : N ⊢ p : A | ∆ and Γ ⊢ t : N | ∆, by Lemma 2.6 and the fact that∆[t/x] = ∆, we get a proof Π ′ p of Γ ⊢ p[t/x] : A[t/x] | ∆.We can thus build the following derivation:Π ′ p Γ ⊢ p[t/x] : A[t/x] | ∆ Π e Γ | e : B[t/x] ⊢ ∆; {•|p[t/x]} Γ | e : A[t/x] ⊢ ∆; {•|p[t/x]} (≡ l ) ⟨p[t/x]||e⟩ : Γ ⊢ ∆ (Cut)using Corollary 2.5 to weaken the binding to p[t/x] in Π e .• Case ⟨λa.p||q • e⟩ ⇝ ⟨q|| μa.⟨p||e⟩⟩.A typing proof for the command on the left-hand side is of the form:Π p Γ, a : A ⊢ p : B | ∆ Γ ⊢ λa.p : Π a:A B | ∆ (→ r ) Π q Γ ⊢ q : A ′ | ∆ Π e Γ | e : B ′ [q/a] ⊢ ∆; {•| †} Γ | q • e : Π a:A ′ B ′ ⊢ ∆; {•|λa.p} Γ | q • e : Π a:A B ⊢ ∆; {•|λa.p} (≡ l ) ⟨λa.p||q • e⟩ : Γ ⊢ ∆ (Cut)If q D, we define B ′ q ≜ B ′ which is the only type in B ′ {a |q } . Otherwise, we define B ′ q ≜ B ′ [q/a] which is a type in B ′ {a |q } . In both cases, we can build the following derivation:

for the (cut)-rule. Consequently, it can also be dropped for all the other cases. The case of the conversion rule is a direct consequence of the third case. For refl, we have by definition that refl * = λx .x : N * → N * .The only non-direct cases are subst p q, with p not a value, and (t, p). To prove the former with p V , we have to show that if:Γ ⊢ p : t = u | ∆; σ Γ ⊢ q : B[t/x] | ∆; σ Γ ⊢ subst p q : B[u/x] | ∆; σ (subst)then subst p q * = µα .⟨p * || μ_ .⟨µα .⟨q * ||α⟩||α⟩⟩ : B[u/x] * . According to Lemma 2.10, we have that B[u/x] * = B[t/x] * = B * . By induction hypothesis, we have proofs of Γ * ⊢ p * : N * → N * | ∆ * and of Γ * ⊢ q * : B | ∆ * . Using the notation η q * ≜ µα .⟨q * ||α⟩, we can derive:Γ * ⊢ p * : N * → N * | ∆ * Γ * ⊢ q * : B * | ∆ * Γ * ⊢ η q * : B * | ∆ * α : B * ⊢ α : B * ⟨η q * ||α⟩ : Γ ⊢ ∆ * , α : B * (Cut) Γ * | μ_ .⟨η q * ||α⟩ : B * ⊢ ∆ * , α : B * ( μ) ⟨p * || μ_ .⟨η q * ||α⟩⟩ : Γ * ⊢ ∆ * , α : B * (Cut) Γ * ⊢ µα .⟨p * || μ_ .⟨η q * ||α⟩⟩ : B * | ∆ * (µ)The case subst V q is easy since (subst V q) * = q p has type B * by induction. Similarly, the proof for the case (t, p) corresponds to the following derivation: Γ * ⊢ p * :A * | ∆ * Γ * ⊢ t * : N | ∆ * a : A * ⊢ a : A * Γ * , a : A * ⊢ (t * , a) : N∧ A * | ∆ * (∧ r ) α : N∧ A * ⊢ α : N∧ A * ⟨(t * , a)||α⟩ : Γ, a : A * ⊢ ∆ * , α : N∧A * (Cut)

We actually even consider α -conversion for delimited continuations t p, to be able to insert such terms inside a type. Even though this might seem strange at first sight, this will make sense when proving subject reduction.

Everything works as if when reaching a state where the reduction of a term is needed, we had an extra abstract machine to reduce it. Note that this abstract machine could possibly need another machine itself for reducing proofs embedded in terms, etc. We could actually solve this by making the reduction of terms explicit, introducing for instance commands and contexts for terms with the appropriate typing rules. However, this is not necessary from a logical point of view and it would significantly increase the complexity of the proofs, therefore we rather chose to stick to the actual presentation.

(µ) c : (Γ, a : A ⊢ ∆) Γ | μa.c : A ⊢ ∆ ( μ) Γ, a : A ⊢ p : B | ∆ Γ ⊢ λa.p : Π a:A B | ∆ (→ r ) Γ ⊢ q : A | ∆ Γ | e : B[q/a] ⊢ ∆ q D ⇒ a FV (B) Γ | q • e : Π a:A B ⊢ ∆ (→ l ) Γ, x : N ⊢ p : A | ∆ Γ ⊢ λx .p : ∀x N .A | ∆ (∀ r ) Γ ⊢ t : N ⊢ ∆ Γ | e : A[t/x] ⊢ ∆ Γ | t • e : ∀x N .A ⊢ ∆ (∀ l ) Γ ⊢ t : N | ∆ Γ ⊢ p : A(t) | ∆ Γ ⊢ (t, p) : ∃x N .A(x) | ∆ (∃ r ) Γ ⊢ p : ∃x N .A(x) | ∆ p ∈ D Γ ⊢ prf p : A(wit p) | ∆ prf Γ ⊢ p : A | ∆ A ≡ B Γ ⊢ p : B | ∆ (≡ r ) Γ | e : A ⊢ ∆ A ≡ B Γ | e : B ⊢ ∆ (≡ l ) Γ ⊢ p : t = u | ∆ Γ ⊢ q : B[t/x] | ∆

(→ I ) Γ ⊢ p : Π a:A B Γ ⊢ q : A Γ ⊢ p q : B[q/a] (→ E ) Γ, x : N ⊢ p : A Γ ⊢ λx .p : ∀x N A (∀ 1 I ) Γ ⊢ p : ∀x N .A Γ ⊢ t : N Γ ⊢ p t : A[t/x] (∀ 1 E ) Γ ⊢ p : A X FV (Γ) Γ ⊢ p : ∀X .A (∀ 2 I ) Γ ⊢ p : ∀X .A Γ ⊢ p : A[P/X ] (∀ 2 E ) Γ ⊢ t : N Γ ⊢ p : A[u/x] Γ ⊢ (t, p) : ∃x N A (∃ I ) Γ ⊢ p : ∃x N A Γ ⊢ prf p : A(wit p) (prf ) Γ ⊢ p : ∃x N A Γ ⊢ wit p : N (wit) Γ ⊢ refl : x = x (refl)

In fact, we could define it formally, which would require a kind of co-delimited continuation.

A classical proof might backtrack, thus it translation might use a former continuation. The return type of continuations thus need to be uniform (usually ⊥) and can not be parametrized by ∀R.

(Cut) Γ | μa.⟨q||⋆⟩ : A ⊢ ∆, ⋆ : B ( μ) ⟨p|| μa.⟨q||⋆⟩⟩ : Γ | ∆, ⋆ : B (Cut) Γ ⊢ µ⋆.⟨p|| μa.⟨q||⋆⟩ | ∆⟩ : B (µ)We want to show that for any X we can derive:Γ ∪ ∆ ⊢ λk. p p (λa. q p k) : Π b:B X (b) → X (q + [p + /a]).By induction, we have:Γ ∪ ∆ ⊢ p p : ∀Y .(Π a:A + Y (a) → Y (p + )) Γ ∪ ∆ , a : A + ⊢ q t : ∀Z .(Π b:B + Z (b) → Z (q + )),so that by choosing Z (b) ≜ X (b) and Y (a) ≜ X (q + ), we get the expected derivation:Γ ∪ ∆ ⊢ p p : . . . Γ ∪ ∆ , a : A + ⊢ q p : . . . k : Π b:B X (b) ⊢ k : k : Π b:B X (b) Γ ∪ ∆ , k : Π b:B X (b), a : A + ⊢ q p k : X (q + ) (→ E )

In particular, Lepigre's semantical restriction is so permissive that it is not decidable, while it is easy to decide whether a proof term of dL t p is in nef.

This will allow us to ease the definition of the translation to handle separately proofs and contexts. Otherwise, we would need formally to define ⟨p ||q • e ⟩ c all together by p p q p * e e .

Where 0 is defined as λzs .z and S (t ) as (λzs .s(t zs)), i.e. as the translation of the corresponding 0 and successor from dL t p .

⟨p||e⟩ c ≜ p p * e e µ t p.c p ≜ µα . c t p ⟨p|| t p⟩ t p ≜ p p ⟨p|| μa.c⟩ t p ≜ (µα . p p * [λa. c t p ]α) * α Fig. 11. Translation of proof terms into Lepigre's calculusΓ ⊢ t : A Γ ⊢ π : A ⊥ ⊥ Γ ⊢ t * π : B * Γ ⊢ • : ⊥ ⊥ ⊥ • Γ, α : A ⊥ ⊥ ⊢ α : A ⊥ ⊥ α Γ, α : A ⊥ ⊥ ⊢ t : A Γ ⊢ µα .t : A µ Γ ⊢ π : (A[x := t]) ⊥ ⊥

That is, the translation q p * [λa . p p * e e ]• of a command ⟨q || μa . ⟨p ||e ⟩ ⟩ (where e is of type B[q] and p of type B[a]) would have been ill-typed (because p p * e e is).

To be precise, for each arrow in the type, a double-negation (or its refinement) would be inserted. For instance, to recover a function of type N → N from a term t : ¬¬(N → ¬¬N) (where ¬¬A is in fact more precise, at least ∀R .(A → R) → R), the continuation needs to be forced at each level: λx .t I x I : N → N. We do not want to enter into to much details on this here, as it would lead us to much more than a paragraph to define the objects formally, but we claim that we could reproduce the results obtained for terms of type N in a language with terms representing arithmetic functions in finite types.

The interested reader could see for instance[START_REF] Miquey | Classical realizability and side-effects[END_REF] Chapter 8] where a similar language with pairs, patter-matching, inductive and coinductive fixed points is defined.

Acknowledgments. The author wishes to thank Pierre-Marie Pédrot for a discussion that led to the idea of using delimited continuations, Gabriel Scherer for his accurate observations and the constant interest he showed for this work, Hugo Herbelin who provided valuable help all along the writing of this paper, Rodolphe Lepigre for the example of the infinite tape lemma, as well as Alexandre Miquel and anonymous referees of this paper for their constructive remarks.

Regular mode: We can thus build the following derivation for the command on the right:

• Case ⟨prf p||e⟩ ⇝ ⟨µ t p.⟨p|| μa.⟨prf a|| t p⟩⟩||e⟩.

We prove it in the most general case, that is when this reduction occurs under a delimited continuation. A typing derivation for the command on the left to be of the form:

The proof p being nef, so is µ t p.⟨p|| μa.⟨prf a|| t p⟩⟩, and by definition of the reduction for types, we have for any type A that:

so that we can prove that for any b: σ {b|prf p} ⇛ σ {b|µ t p.⟨p|| μa.⟨prf a|| t p⟩⟩}.

Thus, we can turn Π e into Π ′ e a derivation of the same sequent except for the list of dependencies that is changed to σ {•|µ t p.⟨p|| μa.⟨prf a|| t p⟩⟩}. We conclude the proof of this case by giving the following derivation: • Case ⟨µ t p.⟨p|| t p⟩||e⟩ ⇝ ⟨p||e⟩.

This case is trivial, because in a typing derivation for the command on the left, t p is typed with an empty list of dependencies, thus the type of p, e and t p coincides.

prf (t, p) → β p subst refl q → β q (a) Language and formulas (b) Reduction rules

• Case (wit). In dL t p the typing rule for wit p is the following:

We want to show that:

By induction hypothesis, we have:

hence, it amounts to showing that for any X we can build the following derivation:

• Case (∃ I ). In dL t p the typing rule for (t, p) is the following:

Hence, we obtain by induction:

and we want to show that for any Z :

So we need to prove that:

We let the reader check that such a type is derivable by using X (x) ≜ Π a:A(x ) Z (x, a) in the type of t p , and using Y (a) ≜ Z (t + , a) in the type of p p :

□

Using the previous Lemma, we can now prove that the CPS translation is well-typed in the general case. Proposition 4.10 (Preservation of typing). The translation is well-typed, i.e. the following holds:

(1

Proof. The proof is done by induction on the typing derivation, distinguishing cases according to the typing rule used in the conclusion. It is clear that for the nef cases, Lemma 4.9 implies the result by taking X (a) = ⊥. The rest of the cases are straightforward, except for delimited continuations that we detail hereafter. We consider a command ⟨µ t p.⟨q|| μa.⟨p|| t p⟩⟩||e⟩ produced by the reduction of the command ⟨λa.p||q • e⟩ with q ∈ nef. Both commands are translated by a proof reducing to ( q p (λa. p p )) e e . The corresponding typing derivation in dL t p is of the form:

A Classical Sequent Calculus with Dependent Types 1:39 By induction hypothesis for e and p we obtain:

Applying Lemma 4.9 for q ∈ nef we can derive:

We can thus derive that: Γ ∪ ∆ ⊢ q p (λa. p p ) : B[q + ] * , and finally conclude that:

Γ ∪ ∆ ⊢ ( q p (λa. p p )) e e : ⊥ . □

We can finally deduce the correctness of dL t p through the translation:

Theorem 4.11 (Soundness). For any p ∈ dL t p , we have: ⊬ p : ⊥.

Proof. Any closed proof term of type ⊥ would be translated in a closed proof of (⊥ → ⊥) → ⊥. The correctness of the target language guarantees that such a proof cannot exist. □

EMBEDDING INTO LEPIGRE'S CALCULUS

In a recent paper [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF], Lepigre presented a classical system allowing the use of dependent types with a semantic value restriction. In practice, the type system of his calculus does not contain a dependent product Π a:A B strictly speaking, but it contains a predicate a ∈ A allowing the decomposition of the dependent product into ∀a.((a ∈ A) → B) as it is usual in Krivine's classical realizability [START_REF] Krivine | Realizability in classical logic. In interactive models of computation and program behaviour[END_REF]. In his system, the relativization a ∈ A is restricted to values, so that we can only type V : V ∈ A:

However, typing judgments are defined up to observational equivalence, so that if t is observationally equivalent to V , one can derive the judgment t : t ∈ A. Interestingly, as highlighted through the CPS translation by Lemma 4.1, any nef proof p : A is observationally equivalent to some value p + , so that we could derive p : (p ∈ A) from p + : (p + ∈ A). The nef fragment is thus compatible with the semantical value restriction. The converse is obviously false, observational equivalence allowing us to type realizers that would be untyped otherwise 24 .

We shall now detail an embedding of dL t p into Lepigre's calculus, and explain how to transfer normalization and correctness properties along this translation. Additionally, this has the benefits of providing us with a realizability interpretation for our calculus. While we do not use it in the current paper, we take advantage of this interpretation (and in particular of the interpretation of dependent types) in [START_REF] Miquey | Classical realizability and side-effects[END_REF]Chapter 8] to prove the normalization of dLPA ω , the sequent calculus which originally motivated this work and whose construction relies on dL t p .

Actually, his language is more expressive than ours, since it contains records and patternmatching (we will only use pairs, i.e. records with two fields), but it is not stratified: no distinction is made between a language of terms and a language of proofs. We only recall here the syntax and Γ ⊢ π : • the strong existential is encoded as a pair, hence wit (resp. prf ) is mapped to the projection π 1 (resp. π 2 ). In [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF], the coherence of the system is justified by a realizability model, and the type system does not allow us to type stacks. Thus, we cannot formally prove that the translation preserves typing, unless we extend the type system in which case this would imply the adequacy. We might also directly prove the adequacy of the realizability model (through the translation) with respect to the typing rules of dL t p . We will detail here a proof of adequacy using the former method. We then need to extend Lepigre's system to be able to type stacks. In fact, his proof of adequacy [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]Theorem 6] suggests a way to do so, since any typing rule for typing stacks is valid as long as it is adequate with the realizability model.

We denote by A ⊥ ⊥ the type A when typing a stack, in the same fashion we used to go from a type A in a left rule of two-sided sequent to the type A ⊥ ⊥ in a one-sided sequent (see the remark at the end of Section 2.5). We also add a distinguished bottom stack • to the syntax, which is given the most general type ⊥ ⊥ ⊥ . Finally, we change the rule ( * ) of the original type system in [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF] and add rules for stacks, whose definitions are guided by the proof of the adequacy [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]Theorem 6] in particular by the (⇒ e )-case. These rules are given in Figure 12.

We shall now show that these rules are adequate with respect to the realizability model defined in [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]Section 2]. Proposition 5.1 (Adeqacy). Let Γ be a (valid) context, A be a formula with FV (A) ⊂ dom(Γ) and σ be a substitution realizing Γ. The following statements hold:

Proof. The proof is done by induction on typing derivations, we only need to do the proof for the rules we defined above (all the other cases correspond to the proof of [START_REF] Lepigre | A classical realizability model for a semantical value restriction[END_REF]Theorem 6]).

1:46

Étienne Miquey

A fully sequent-style dependent calculus

While the aim of this paper was to design a sequent-style calculus embedding dependent types, we only presented the Π-type in sequent-style. Indeed, we wanted to be sure above all that it was possible to define a sound sequent-calculus with the key ingredients of dependent types (i.e. dependent pairs and dependently-typed functions). In particular, rather than having left-rules (as in sequent calculi) for every syntactic constructors, we presented the existential type and the equality type with the following elimination rules (as in natural deduction):

However, it is now easy to replace both elimination rules (and thus the corresponding destructors) by equivalent left-rules (and thus syntactic constructors for contexts). For instance, we could rather have contexts of the shape μ(x, a).c (to be dual to proofs (t, p)) and μ=.c (dual to refl). We could then define the following typing rules:

and define 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 definable if p is a nef proof term. Since for any p ∈ nef and any variables a, α, the formula A(wit p) belongs to A(wit (x, a)) {(x,a)|p } , this allows us to derive the admissibility of the former (prf )-rule: .

As for the reduction rules, we can define the following (call-by-value) reductions:

and check that they advantageously 30