Hello, and welcome to this online presentation. I am going to present you a work that we did with Hugo Herbelin about the definition of well-typed continuation and environment-passing style translations.

To that end, we had to introduce the new calculus, a calculus of expandable stores, and this is what I'm going to present right now. I assume that anyone listening to this talk is already very familiar with the lambda calculus, of which you may know that this is a very nice abstraction,

a nice computation of models with many expected properties. In particular, it has different evaluation strategies, there are different ways of computing things. You may also know, I assume, that these different evaluation strategies

can be specified through abstract machines, so there exists a huge variety of abstract machines. One nice thing about this is that if we want to reason about abstract machines within the lambda calculus, there exists a wonderful tool to abstract this notion, to reify it, which are continuation-passing style translations,

also called CPS, because they are internalizing somehow the operational semantics within the lambda calculus through a translation, that is also specifying an evaluation strategy, also making explicit the control flow. In addition to that, since they also induce a typed translation,

a translation at the level of types, not only for terms, we can see typed continuation-passing style translations as syntactic models, insofar as they allow to transfer logical properties, like soundness or normalization, from the target calculus to the source calculus.

Among the different evaluation strategies of the lambda calculus, you may know this evaluation, also called call-by-need. Call-by-need, just like in call-by-name, evaluates our argument of functions only if they are needed, so we don't do useless computations,

and more than that, as in call-by-value, when something has been computed, the evaluation, the value, is shared across all the places where it is needed. In some sense, it is a mix of call-by-name and call-by-value,

and to put it in a nutshell, call-by-need is just demand-driven computations, so you compute when you need it, plus a memorization technique to avoid recomputing arguments of functions. This evaluation strategy has many benefits. In particular, it is used in well-known computational systems,

like Haskell, Coq. In Haskell, for instance, it is the default evaluation strategy, and in Coq, you can use it as a tactic, but it is also present already in the kernel. Nonetheless, it has been less studied historically than call-by-name and call-by-value,

and it is treated here for many reasons that we will see. One of these reasons is that, if we consider the usual abstract machines, for instance, here, the Cribin abstract machine of call-by-name,

it uses local environments and closures. The term here is computed in front of the stack, and within an environment, and we can see that when we push, for instance, an argument to the stack, we are copying the environment to form a closure, here of U with the current environment, and when we pop an argument of the stack,

for instance, to apply the beta reduction rule, we are linking U with the closure, and U with its environment, so we are copying many environments, and they are local, but in two closures. Obviously, this is incompatible with lazy evaluation,

insofar as we want to share computations, so we need global environments. This is, for instance, the case of the minimal abstract machine, so also for the call-by-name evaluation strategy here, we can see that the term is computed in front of a stack, so these are with one global environment which is not copied,

so when we push onto the stack, we don't do any copy. When we abstract, when we perform the beta-relatron rule here, we get U, and we set the link X to U once in the environment, and the environment of U is given by the prefix of the environment here.

And one difficulty is that when we have a global environment, we need to explicitly say how we address the issues related to names, so one solution is to say that each time that we get a term out of the environment, we have to get a fresh copy with fresh names,

because otherwise T may be putting new terms into the store, but if the variables that are going to be put afterwards are already present, we are going to have some name clashes potentially.

But more than these difficulties that are somehow already handled, because we know how to define abstract machines with global environments, and there exists also binary abstract machines. The hard question is to know how to define some CPS translations,

and actually a typed CPS translation but already un-typed is a hard question, because it can not only be a continuation passing style translation, but it has to pass somehow the environment, because the environment is global, so it has to be passed around during the computations.

And for that, there are several difficulties to handle. The first one is to understand how the control and the environment should interact, so how to define, for instance, a classic whole-type police with leisure regulation. This is already done, I will explain this afterwards.

But what wasn't known when we started this, was to know how to soundly type environments, and in particular how to type them along the translation, while accounting for extensibility, because environments may grow along computations, and we need to have a type system which is going to account for that,

and also how to have a technique to avoid named crashes, which is especially tricky during the translation. In this paper, we are precisely defining typed, well-typed continuation and environment passing style, which I will call CPS afterwards,

and our main contribution is the introduction of a calculus, f-epsilon, which is generic as a target for CPS translations. This calculus, as we will see, is featuring two main things. The first one is the type for typed stores,

and the other one is a mechanism of explicit corrections, which is going to witness the extensions of stores. Why do we call it generic? Because our goal was not only to define well-typed CPS translations, but also to isolate the key ingredients necessary to these definitions.

As we will see, we can indeed use f-epsilon to define CPS translations for different calculi, at least in the paper we do it for three calculi, simply typed call-by-need, call-by-name, and call-by-value lambda-calculus, and we shall discuss the possibility of using it for more involved type systems,

so for instance system f has an input. What are continuation and invariant passing style translations? Actually, the very first question to answer is to understand how to define a correct operational semantics of a calculus with control operators and shared memory.

Indeed, to define a CPS translation is usually equivalent to define the operational semantics of a calculus with control operator. This question is actually very hard, and it was already tackled in 1993 by Okazaki and RDT. You can pause the video if you want to look in detail at this example,

but they had a semantic saying that what is not forcing an effect, what is not reaching a catch or throwing operation, shouldn't be shared. So this is wrong, I'm saying something wrong. Blah, blah, blah.

In order to define a CPS translation, the very first question to answer is to understand how should be the correct semantics of a control operator, so the mechanism related to continuation passing style, in presence of shared memory.

This question is hard, and it was already tackled in 1993 by Okazaki and RDT. You can pause the video if you want to look at the code example, which is on the left. But in their semantics, they were saying that what is not forcing an effect, what is not leading to a throw, has to be shared.

So in particular, in this example, f and q, q is shared and f is recomputed, and in the end, if you look at this very particular example, it is going to loop, while it shouldn't. And so their semantics wasn't correct, and that was shown later by Arroyola and several others.

And in turn, they proposed a semantic in which nothing is shared inside an effect, so in this example, f and q are recomputed, and indeed this codepiece is going to reduce correctly to the pair of identity. What was their method? In the paper, they defined a second calculus for a classical called binary calculus,

and then they derived from this one calculus an abstract machine, and then from the abstract machine, they derived an untyped PS translation, which is known as the method of Danvy semantic artifacts. And we show in the previous paper also, as you will have learned,

that their semantics can be typed, normal, and that it is normalizing and consistent. To that end, we use the realizability interpretation. What are the intuitions that we can get from previous works? Well, if we look at the sequence calculus defined in the paper of Arroyola et al., we can see that the sequence calculus has three components.

We have a term, which is evaluated in front of a context, as is usual in sequence calculus, plus an external environment, as we had in the abstract machine with global environments in the beginning. So, I'll let you pause the video if you want to look closer at the syntax, but in Broadline it has three categories

for terms, contexts, and environments. And the categories for terms and contexts are divided into the notion of terms, the notion of weak values, and the notion of strong values. And we have the corresponding notion for contexts, so the usual context, and co-values, and strong co-values, if you want.

And you can think of these three syntactic categories as the categories needed for the interaction defined by the lazy evaluation. We have less when we have call-by-name or call-by-value, and we need more because of the lazy evaluation. If you look at the reduction rule,

just to see that this is indeed a lazy evaluation, we can see that here, when we have T in front of mu tilde x, mu tilde x can be read as let x be T in C. Then what we do is we store lazyT together with the variable x here. And if at some point we need the variable x,

we need its value in front of demanding a forcing context here, and that x has been linked with the term T, we are going to froze the computation here, open the store, and do the computation for T. And if T eventually produces a value here, a value v, then we put back x together with the value v,

and we go on with the computation, now where x has been substituted by v. So this is really lazy, we lazyly store, and if really we need it, then we do the computation, and once we've done it, it is done forever. So this is lazy evaluation.

What about the untyped CPSE defines? Well, as we can imagine, it has an extra component, it has not only the component for the continuation passing part, but also something which is the environment passing part. And again, if you want really to look at the details,

but it's not necessary, you can pause the video, but what is important to see here is that we have everywhere a blue and a red part corresponding to the environment passing part and the continuation passing part. So the translation of a term or context is going to be something waiting for a store and then waiting for a term or continuation,

and then producing the computation. The second step consists in defining the type translation corresponding to the environment passing part. And to that end, let me give a bit of intuition. So in a set point, if we think of what is the role

that the context plays, actually we can think of the context as a specification for correct substitution to get T of the corresponding type A here. So gamma is saying what should be the type of variables, and actually the environments that we are handling

in the CPS and in the second calculus, there are some kind of explicit substitution. So the type of the explicit substitution should be the type of context and saying that T is of type A under the context gamma is saying that T is waiting for a substitution of type gamma, so the translation of gamma here

to return a term of type, the translation of A. So let us write this translation here with this notation and the index T saying that we are translating at the level of term rather than context value and so on and so on. So if we unfold, T is waiting for substitution and environments of type gamma,

and then a continuation of type A and the translation corresponding to the context gamma, and then returning bottom because of the continuation passing part. And again, if we translate here, if we unfold the definition of the translation of the level A, E, sorry, then we are going to get this definition.

So the continuation is itself waiting for a substitution of type, the translation of gamma, waiting for a value and then returning bottom and so on and so on. And we can define the translation for the six layers here. And again, we can see clearly the fact that we are waiting for an environment

and using a continuation. The next step has to do with the fact that the environment can grow. Indeed, look at this possible reduction scheme. Assume that we have a computation in which we are needing the value for X and X has been linked to T in the environment.

What do we do? We are frozen the computation for the moment, then computing the value of T in the prefix of the store because the store has been split into two parts. Then T is eventually going to produce a value. And if it does, we are going to put it back into the store. But while it was computing,

T may have been adding some new elements here to the store. So in the end, we get a store that has been extended. And of course, this is actually a bit more complex than that. It could be recursively at any place in T1 and T2. So the store might grow at any time at any place.

The key idea is that, just like we were saying that the translation of gamma was specifying what are the correct substitutions, our idea is to say that any substitution that contains at least gamma should be considered correct, meaning that if T is of type the translation of N or the context gamma,

it should be compatible with any extension whose type is an extension of the translation of gamma. To that end, we introduce a notion of store subtyping, which is really easy, the natural one saying that gamma prime here, this one is an extension of A1, A2,

because we have a way to find A1 and A2 both in the extension of the store and gamma prime here. About the translation, at that stage we were using this definition, and now we no longer want T to be waiting for a store of type gamma,

but any store whose type is an extension of gamma here, and again this has to be defined recursively, so the continuation itself is waiting for an extension of that store actually, and we can define the translation at the six layers.

The next and the last step is to understand how to avoid name clashes, and this is actually really important because in the previous work of Harry Lettau they were implicitly relying on the possibility of using an on-the-fly process of alpha renaming, and while this is perfectly fine with the second calculus, this is actually incompatible with the CPS translation.

Here, in terms, we will use debris levels, both in the source and the target, so in the source it means that the name here is actually N, rather than X, this is in hybrid notation, and N is referring to the position both here in the typing context, because we saw that the context

is the type of the substitution of the environment, and to the type of the position in the store here, and we can see that when we are looking for XN, we look at the Nth position into the store, and if, as we saw before,

we want to store back the value of V, but some extra element has been added to the store, so there is a mismatch between this level here, I and N, and then we have to explicitly say how we lift the mismatching debris levels.

In the target, we simply drop the names, so we now use this hybrid notation with our levels, and we just say that T is of type translation in the context A, B, C here, and we use correlations to witness store extensions, so correlations, they are simply functions saying how we can follow the extension

to find the expected competence, so if we are looking at the first position, we are expecting something of type A1, the correlation sigma is going to help us to find it into the extension.

So, we've seen how we can hope to type a CPS translation, and now we can present you the calculus we defined, f-epsilon, that has all the necessary features to define such translation. Remember that our wish was to define a parametric calculus

to serve as a target for different CPS translations. Each of the CPS translations we will see can be divided into three blocks. The first one is the source calculus, together with its type system, so here we only present simply type calculus, or at least in the paper, that's what is done. Then we use the syntax to handle stores and conversions,

and afterwards the target calculus, which is going to use the two first blocks, and it's going to be an instance of what we call f-epsilon. In the paper, we only use lists to represent store, but we could also imagine to use trees or whatsoever,

and so we can see that both store types are defined as list of types, while stores are defined as lists, so we have the anti-list, the list extended with one element, and the concatenation. And we have typing rules to say that 2 here is of type epsilon,

if it is attended to a store whose type is epsilon prime. We can see that, for instance, in the concatenation rule, here we need to take into account for the second component, the store of the first component here. And also, if the type of the store is always a list of source types, the way these types are translated,

here is a parameter of the target, so we can see that when we have one element, it is of type T here, under the context epsilon 0, if the term T is itself of the type here, we have this black triangle, which is going to be a parameter, which we instantiate with precisely

the type translation of the desired ceps. What about corrections? Well, they are the proof terms witnessing list inclusion, so we have the base case, we have a case for saying that we are adding

the same type in both sides of the list inclusion, and we have the case of a strict extension, so we say that this is an extension here of epsilon, if we have been adding something, and that the prefix epsilon prime is already an extension of epsilon.

So, for instance, you can pause the video if you want to look at this example, but here we have the proof term witnessing the extension of T U, T 0, T U, T 1, and if it can be helpful, you can think of this witness as something corresponding to the function, which maps the burning events, the position,

the star 0 to 1, 1 to 2, 1 to 2, to 4. So, what is system f epsilon? In broad lines, this is just system f extended with stars and corrections, and actually this is a bit more involved than that, but this is a good idea, I think, to have in mind.

As for the syntax, we have the syntax for star types, for stars and for corrections that we saw, and then the lambda calculus, so we have here something which corresponds to the source calculus, here it's simply typed, so we only have base k and n functions.

Theorems to abstract corrections here and to apply to corrections, the same for stars, the same here for star type, and one extra important term, which is the one explaining to us how to, giving us the ability of getting a star. So intuitively, speed here is used to look into a star of type epsilon prime,

which is the star 2 here, for the term that was expected in what epsilon prime is extending, at position n, here, using the correction,

so we were expecting here a star of type epsilon, we were looking at the nth position, and we are actually giving the star 2, whose type is an extension of epsilon, and what split is doing, it's looking through the correction to get the expected term, and splitting the corresponding star into three blocks.

We have three kinds of reduction rules, we have the rule for split that we just saw, the rule for normalizing corrections, because we need to abstract the variables, variables for star types and so on, so it's a bit more complicated than what I saw, but this is the same idea, and the usual beta reduction for abstractions and applications,

and we can show that the reduction we defined is preserving the typing of the system, and that type term can be shown to be normalizing. Also, if you want to have a look at the system, we define a shallow embedding in Coq of f epsilon, and you can look at this definition and see that they are really what we are showing here.

As an example, we show in the paper that we can take advantage of the genericity of our definition to define different CPS translations, so remember that here, to define the type of a term into the star, we are using a parameter that we can choose

depending on which translation we want, and indeed, in the paper, we define well-typed CPS using this for call-by-need, call-by-name, and call-by-value, and the only thing we have to do is to change, of course, the translation of terms, and here, change the parameter to use the correct translation for types.

All these translations follow exactly the intuitions we saw before, so we have a continuation passing part mixed with an environment passing part, and the environment passing part is corresponding somehow to a creepiest type forcing, and we discuss in the paper the possibility of extending the...

of not extending, and we discuss in the paper the possibility of considering different inputs, so no longer simply type-per-cubus, but for instance, system f, and this should be okay just by using the usual forcing translation for system f. To conclude,

we believe that we managed to isolate the key ingredients to define well-typed CPS, so the first thing is to have terms to represent and manipulate type stores, and the other one is to have a mechanism of explicit correlations. Then, we show that our calculus, our proposition,

f epsilon, has the benefits of being really parametric, we can use it for different CPS, we can use it with different source-type systems, and also we don't know if that can be of any use, we can use it with different implementation of tools. From a logical point of view,

we've seen that CPS amounts to some creep-cuff forcing translation interweaved with a negative translation, and actually the connection with creep-cuff forcing or with forcing in general does not come as a surprise, because it was already done that both forcing and state monad, for instance,

can be given a semantic through preshives, and also it is most mentioned in the work of Crivin to simulate forcing in classical realizability, and he uses an extra cell, so somehow state monads. A few open questions for further work. The first one is that we believe that this may constitute

a first step towards the definition of all-type translation processes for calculating combining. Also, we would like to know what is the exact expressiveness of f-epsilon, because we said that it was broadly f plus store-types and sub-typing-morality,

but actually it's a bit more than that, because we have some sized types, so we need at least a slight bit of dependent types. But of course, this is way less than the usual type theory. Finally, we would like to see whether we could define the type translation through modality. By this we mean that

if we look at what is the translation of A under some contexts, this function is mapping a store-type here to a type, and what we've been doing all the time is to use the transformation of such functions, saying that if f is such a function,

we consider a function mapping a store-type to the whole translation that is waiting for an extension, getting a store of that type, then using f to transform this extension and returning the bottom for the continuation. And then, with this definition, we can see that the translation under level A is the box under translation under level E,

and this is itself the box under translation under level D. Just like in the usual CPA translation, we would have the box being the negation and then having the negation here. So we would like to see if, just like the negation again, this box may have some interesting logical properties.

Thank you for your attention, and of course we would be happy to answer any of your questions, either at the dedicated slot at clicks or by simply sending us an email and we would be happy to answer them. Thanks.