Nikos Paragios
email: nikos.paragios@ecp.fr

Nikos Komodakis
email: nikos.komodakis@enpc.fr

Gaspard Monge

Discrete Visual Perception

Computational vision and biomedical image have made tremendous progress of the past decade. This is mostly due the development of efficient learning and inference algorithms which allow better, faster and richer modeling of visual perception tasks. Graph-based representations are among the most prominent tools to address such perception through the casting of perception as a graph optimization problem. In this paper, we briefly introduce the interest of such representations, discuss their strength and limitations and present their application to address a variety of problems in computer vision and biomedical image analysis.

I. INTRODUCTION

Computational vision is one of the most challenging research domains in engineering sciences. The aim is to reproduce human visual perception through intelligent processing of visual data. The application domains span from computer aided diagnosis to industrial automation & robotics. The most common mathematical formulation to address such a challenge is through mathematical modeling. In such a context, first the solution of the desired vision task is expressed in the form of a parameterized mathematical model. Given such a model, the next task consists of associating the model parameters with the available observations, which is often called the model-to-data association. The aim of this task is to determine the impact of a parameter choice to the observations and eventually maximize/minimize the adequacy of these parameters with the visual observations. In simple words, the better the solution is, the better it will be able to express and fit the data. This is often achieved through the definition of an objective function on the parametric space of the model. Last, but not least given the definition of the objective function, visual perception is addressed through its optimization with respect to the model parameters. To summarize, computation visual perception involves three aspects, a task-specific definition of a parametric model, a data-specific association of this model with the available observations and last the optimization of the model parameters given the objective and the observations. Such a chain processing inherits important shortcomings. The curse of dimensionality is often used to express the importance of the model complexity. In simple words, the higher the complexity of the model is, the better its expressive power will be with counter effect the increase of the difficulty of the inference process. Non-linearity is another issue to be addressed which simply states that the association between the model and the data is a (highly) non-linear function and therefore direct inference is almost infeasible. The impact of this aspect is enforced from the curse of non-convexity that characterizes the objective function. Often it lives in highdimensional spaces and is ill posed making exact inference problematic (in many cases not possible) and computationally expensive. Last, but not least modularity and scalability is another important concern to be addressed in the context of computational vision. The use of task-specific modeling and algorithmic solutions make their portability infeasible and therefore transfer of knowledge from one task to another is not straightforward while the methods do not always scale well with respect either to the dimensionality of the representation or the data.

To address the above challenges, one can resort to discrete optimization formulations, which apply to a wide variety of tasks in medical image analysis. In very simple terms, a discrete optimization problem can be stated as follows: we are given a discrete set of variables V, all of which are vertices in a graph G. The edges of this graph (denoted by E) encode the variables' relationships. We are also given as input a discrete set of labels L. We must then assign one label from L to each variable in V. However, each time we choose to assign a label, say, x p1 to a variable p 1 , we are forced to pay a price according to the so-called singleton potential function g p (x p ), while each time we choose to assign a pair of labels, say, x p1 and x p2 to two interrelated variables p 1 and p 2 (i.e., two nodes that are connected by an edge in the graph G), we are also forced to pay another price, which is now determined by the so called pairwise potential function f p1p2 (x p1 , x p2 ). Both the singleton and pairwise potential functions are problem specific and are thus assumed to be provided as input. Our goal is then to choose a labeling which will allow us to pay the smallest total price. In other words, based on what we have mentioned above, we want to choose a labeling that minimizes the sum of all the MRF potentials, or equivalently the MRF energy. This amounts to solving the following optimization problem:

arg min {xp} P({x p }; g, f ) = p∈V g p (x p )+ (p1,p2)∈E f p1p2 (x p1 , x p2 ).
The use of such a model can describe a number of challenging problems in medical image analysis. However these simplistic models can only account for simple interactions between variables, a rather constrained scenario for high-level medical imaging perception tasks. One can augment the expression power of this model through higher order interactions between variables, or a number of cliques {C i } i∈ [1,n] with

C i = {p i 1 , • • • , p i |C i | } arg min {xp} P({x p }; g, f ) = p∈V g p (x p ) + (p1,p2)∈E f p1p2 (x p1 , x p2 ) + n i=1 f Ci (x Ci ) ,
here x Ci = {x p |p ∈ C i } and f Ci is the price to pay for associating the labels x Ci to the nodes in C i . Parameter inference, addressed by minimizing the problem above, is the most critical aspect in computational medicine and efficient optimization algorithms are to be evaluated both in terms of computational complexity as well as of inference performance. State of the art methods include deterministic and nondeterministic annealing, genetic algorithms, max-flow/min-cut techniques and convex relaxations. These methods offer certain strengths while exhibiting certain limitations, mostly related to the amount of interactions which can be tolerated among neighborhood nodes. In the area of medical imaging where domain knowledge is quite strong, one would expect that such interactions should be enforced at the largest scale possible.

The reminder of this paper reviews briefly our contributions in the field. Section 2 presents the work done in the area of inference algorithms while section 3 is dedicated to computer vision applications of such methods. Biomedical image analysis is discussed in section 4, while the last section concludes the paper and presents perspectives, future directions of our work.

II. DISCRETE OPTIMIZATION OF PAIR-WISE & HIGHER-ORDER MRFS

Discrete optimization has been an research topic in the vision community for the past decade [START_REF] Wang | Markov Random Field Modeling, Inference & Learning in Computer Vision & Image Understanding: A Survey[END_REF].

In [START_REF] Komodakis | Performance vs computational efficiency for optimizing single and dynamic MRFs: Setting the state of the art with primal-dual strategies[END_REF] we have introduced a novel linear-programming for efficient optimization of arbitrary pair-wise MRFs. The central idea was instead of solving the original problem to cast it as a linear programming one (using an LP relaxation) and then seek the solution that minimizes the primal-dual gap. Such a method exhibits computational efficiency and can handle arbitrary graphs and interactions between their elements (both in terms of connectivity as well as in terms of potentials) 1 .

The quality of MRF-MAP inference from LP-optimization methods heavily depends on the associated relaxation. In [START_REF] Komodakis | Beyond Loose LP-Relaxations: Optimizing MRFs by Repairing Cycles[END_REF] we have introduced a novel dynamic optimization method that updates the LP relaxation on the fly towards increasing its tightness and potentially achieving a globally optimal solution upon convergence. To this end, pair-wise terms of the graphical model become also inference variables under global constraints driven from the original objective function. The proposed formulation has led to state of the art results.

Despite the enormous speed up over conventional methods, the aforementioned solution is sequential and therefore couldn't benefit from recent progress on parallel architectures. In [START_REF] Alchatzidis | Efficient parallel message computation for MAP inference[END_REF], a novel efficient method was introduced for exchanging messages in the context of belief propagation through the jump flooding algorithm, an approach that was able to handle a significant number of labels while outperforming in terms of speed -assuming a basic GPU implementation -for at least one order of magnitude all existing optimization methods.

In [START_REF] Komodakis | MRF Energy Minimization and Beyond via Dual Decomposition[END_REF] we have re-visited belief propagation through dual decomposition, an approach that provides a common theoretical framework for message passing while at the same time introduces a novel, scalable, modular and flexible framework for the minimization of graphical models. Such a method allows the decomposition of your problem into a number of sub-problems over shared variables that can be solved efficiently, and a principled way of coordinating the subproblem solutions is employed such that at the end all of them converge to a unique common optimal solution. Interesting results in the context of blind deconvolution were obtained using such a framework [START_REF] Komodakis | MRF-Based blind image deconvolution[END_REF]. This framework has been further extended to deal with optimization of higher order MRFs [START_REF]Beyond pairwise energies: Efficient optimization for higherorder mrfs[END_REF] where efficient decomposition methods were proposed leading to state of the art results. 1 FastPD is an optimization platform in C++ for the computer vision and medical imaging community (publicly available at http://cvn.ecp.fr) developed at Ecole Centrale and University of Crete. This is the most efficient publicly available platform in terms of a compromise of computational efficiency and ability to converge to a good minimum for the optimization of generic MRFs.

III. IMAGE PROCESSING & COMPUTER VISION

A. Graph Matching & Image Representations

The problem of graph matching [START_REF] Wang | Modeling Shapes with Higher-Order Graphs: Methodology and Applications[END_REF] was initially studied in [START_REF] Zeng | Dense non-rigid surface registration using high-order graph matching[END_REF]. A Higher Order MRF formulation that is invariant to linear geometric transformations was proposed, which was seeking hierarchically a sparse to dense matching through a many-to-many formulation [START_REF] Zeng | Dense non-rigid surface registration using high-order graph matching[END_REF]. Such a formulation was extended in [START_REF]Intrinsic dense 3D surface tracking[END_REF] to track evolving/deforming surfaces and was endowed with a powerful local shape similarity metric that was the Mobius transform. This idea was further extended in [START_REF] Zeng | A Generic Deformation Model for Dense Non-Rigid Surface Registration: a Higher-Order MRF-based Approach[END_REF] towards handling non-rigid shapes through a discrete minimum distortion principle that was modular under various classes of deformations. More recently, such a higher order model was seamlessly integrated with a generic deformation model, called Canonical Distortion Coefficients (CDCs), that characterizes the deformation of every point on a surface using the distortions along its two principle directions leading to an efficient inference paradigm that can easily handle different types of geometry/texture similarity metrics. A different approach exploring shape maps [START_REF] Langs | Modeling the structure of multivariate manifolds: Shape maps[END_REF] was studied in [START_REF] Langs | Learning deformation and structure simultaneously: in situ endograft deformation analysis[END_REF] for the problem of multiple graphs being registered together towards understanding the motion dynamics of the different object parts.

Contextual representation of images using either local representations [START_REF] Znaidia | Bag-of-multimedia-words for image classification[END_REF] or graphs [START_REF] Ou | Detecting mutually-salient landmark pairs with MRF regularization[END_REF] is a well studied problem in the field. In [START_REF] Behmo | Graph commute times for image representation[END_REF] we introduced a new image representation encoding the general layout of groups of quantized local invariant descriptors as well as their relative frequency. This is achieved by embedding the image into a graph where nodes correspond to interest point clusters and links to commute times between the different clusters, and subsequently mapping this graph to lower dimension by exploiting its spectral properties. The proposed representation can be used for indexing [START_REF]An Application of Graph Commute Times to Image Indexing[END_REF] and classification using simple nearest neighbor methods [START_REF] Behmo | Towards optimal naive bayes nearest neighbor[END_REF] or complex classifiers. In [START_REF] Rubio | Image contextual representation and matching through hierarchies and higher order graphs[END_REF] a method for image matching was proposed that exploits hierarchical image representations through higher order graphs. The matching was achieved through a graph-based theoretical framework where the similarity and spatial consistency of the image semantic objects is encoded in a graph of commute times that is also endowed with singleton terms through shape descriptors. These ideas were further explored in the context of co-segmentation [START_REF]Unsupervised co-segmentation through region matching[END_REF] where a method to determine a consistent partition of multiple images was introduced through a multi-scale multiple-image generative model based on region matching that exploits interimage information and establishes correspondences between the common objects that appear in the scene.

B. Image-driven Procedural Modeling of Architectures

Given the deluge of satellite imagery and urban photo collections, an emerging application is computer vision techniques that can produce scalable representations of 3D models of urban environments. Our team has pursued the development of algorithms for inverse procedural modeling, namely the inference of a set of architectural rules that can explain observed building images. Initially, we have investigated the use of graphical models [START_REF] Koutsourakis | Single view reconstruction using shape grammars for urban environments[END_REF] towards inferring the optimal grammar instance and the associated parameters through local self-similarities of the graphical model (structure repetition). Complexity was the main limitation of the method since the optimization problem involves discrete and continuous variables with an unknown number in advances.

C. Pose Estimation, Articulated Models & Illumination/Reflectance

Inferring 3D geometry from 2D images in particular in the context of articulated objects is a highly interesting problem in computer vision. However at the same time it remains a great challenge due to the dimensionality of the model, and the ill-posedeness.

In [START_REF] Wang | Viewpoint invariant 3D landmark model inference from monocular 2D images using higher-order priors[END_REF] we have introduced a novel approach to 3D pose estimation of deformable objects from 2D images that simultaneously recovers the optimal model instance and the corresponding image projections. The main innovation of the method was the implicit handling of the camera pose parameters thanks to the use of a higher order graph where the order of cliques (depending on the projection model) allowed to determine a cost that could simultaneously cope with the unknown model deformation, projection matrix and image correspondences. A different approach was used in the context of articulated models (hand-pose estimation) where we first studied part-based representations [START_REF] La Gorce | A variational approach to monocular hand-pose estimation[END_REF] in which case geometric elements were used to determine the global shape of the object. The inference was then performed by seeking the optimal model projection to the image through a segmentation function that was aiming to separate skin-like properties from the background through an energy that was minimized using the divergence theorem. The simplicity of the representation made the approach sensitive to the initial conditions, as well as to occlusions and self-occlusions.

Understanding the position of light sources is also critical to a number of applications like hand pose estimation. In [START_REF] Panagopoulos | Robust shadow and illumination estimation using a mixture model[END_REF] a graphical model to estimate the illumination environment and detect the shadows of a scene with textured surfaces from a single image and only coarse 3D information was proposed. The central idea was to represent pixel-wise shadow observations as a mixture model of contributions coming from different illumination sources and then alternate between shadows detection and illumination sources parameter estimation. The same concept was further studied in [START_REF] Panagopoulos | Illumination estimation and cast shadow detection through a higher-order graphical model[END_REF], [START_REF] Panagoupolos | Estimating Shadows with the Bright Channel Cue[END_REF] where a higher-order Markov Random Field (MRF) illumination model was employed, which combines low-level shadow evidence with high-level prior knowledge for the joint estimation of cast shadows and the illumination environment. In such a context, a higher order approach is considered where illumination sources are coupled with the observed image and the latent variables corresponding to the shadow detection. Last, but not least approximate geometry estimation of the scene was also incorporated into this framework in [START_REF] Panagopoulos | Simultaneous Cast Shadows, Illumination and Geometry Inference Using Hypergraphs[END_REF].

IV. BIOMEDICAL IMAGE ANALYSIS

A. Medical Model-free and Model-based Segmentation

In [START_REF] Parisot | Graph Based Spatial Position Mapping of Low-grade Gliomas[END_REF] the problem of introducing sparse prior knowledge from small training sets was studied in the context of brain tumor segmentations. The idea was to decompose the population of training examples into small sets with locally consistent behavior, and then build individual statistics for each population locally. This was achieved through a graphical model formulation where the prior model decomposition was expressed as an unsupervised clustering problem involving the number of populations, their most representative elements and the assignments of the training set. Given such a prior model, then inference was expressed through a coupled formulation seeking the optimal class for the prior model and assigning labels to the image [START_REF]Graph-based Detection, Segmentation & Characterization of Brain Tumors[END_REF] according to it (given the class likelihoods [START_REF] Boussaid | Rapid Mode Estimation for 3D Brain MRI Tumor Segmentation[END_REF]). Such an approach was tested on the segmentation of brain tumors (Glioma II). In [START_REF] Honnorat | Guide-Wire Extraction through Perceptual Organization of Local Segments in Fluoroscopic Images[END_REF], [START_REF]Robust guidewire segmentation through boosting, clustering and linear programming[END_REF], [START_REF] Honnorat | Curvilinear structures extraction in cluttered bioimaging data with discrete optimization methods[END_REF], [START_REF] Honnorat | Graph-based guide-wire segmentation through fusion of contrast-enhanced and fluoroscopic images[END_REF] grouping was used for the segmentation of curvilinear structures in low signal to noise ratio images through an ordering of these segments using the elastica model in a linear programming framework. The problem was also considered in its temporal aspect [START_REF] Heibel | Needle tracking through higher-order MRF optimization[END_REF], [START_REF] Heibel | Discrete tracking of parametrized curves[END_REF], [START_REF] Honnorat | Graph-Based Geometric-Iconic Guide-Wire Tracking[END_REF] through a combined iconic-geometric approach [START_REF] Honnorat | Graph-Based Geometric-Iconic Guide-Wire Tracking[END_REF] seeking to determine the optimal deformation along with correspondences for a subset of interest points along this structure. In the context of multi-label segmentation [START_REF] Baudin | Manifoldenhanced Segmentation through Random Walks on Linear Subspace Priors[END_REF] studied two distinct cases of introducing prior knowledge to the random walker graphical model. The first was aiming to position automatically the seeds with respect to the different classes [START_REF]Automatic skeletal muscle segmentation through random walks and graph-based seed placement[END_REF] through the optimization of a graph-based objective function. Later the idea of introducing prior knowledge [START_REF] Baudin | Manifoldenhanced Segmentation through Random Walks on Linear Subspace Priors[END_REF], [START_REF]Prior Knowledge, Random Walks and Human Skeletal Muscle Segmentation[END_REF] in this context was studied using statistical models of varying complexity, like mono-modal distributions or linear sub-spaces per class. Multi-class segmentation of striated Muscles in NMR Images was the clinical case being investigated in this context where the problem of optimal parameter setting was also investigated through machine learning methods [START_REF] Baudin | Discriminative Parameter Estimation for Random Walks Segmentation[END_REF]. Continuous methods have certain strengths but also exhibit a number of limitations in particular during the inference process like for example their strong dependency from the initial conditions. This was an issue that was addressed in [START_REF] Besbes | Shape priors and discrete mrfs for knowledge-based segmentation[END_REF], [START_REF] Chittajallu | An Explicit Shape-constrained MRF-based Contour Evolution Method for 2D Medical Image Segmentation[END_REF], [START_REF] Ou | Detecting mutually-salient landmark pairs with MRF regularization[END_REF], [START_REF] Besbes | Landmark-based segmentation of lungs while handling partial correspondences using sparse graph-based priors[END_REF]. The central idea was to represent prior knowledge through a point distribution representation mapped to a pair-wise probabilistic graphical model. In such a context global shape priors could be built through the concatenation of local constraints resulting on a powerful and flexible model both in terms of learning as well as in terms of inference. The proposed formulation was translation and rotation invariant and was endowed with boundary and regional support (through approximation of the region probabilities based on a Voronoi decomposition of the image domain [START_REF] Besbes | Shape priors and discrete mrfs for knowledge-based segmentation[END_REF]). The method was able to handle missing correspondences and was tested in the context of lungs segmentation since in that case one has to handle an important number of miss-detections [START_REF] Besbes | Landmark-based segmentation of lungs while handling partial correspondences using sparse graph-based priors[END_REF]. This idea has been further expanded in [START_REF] Wang | 3D Knowledge-Based Segmentation Using Pose-Invariant Higher-Order Graphs[END_REF], [START_REF] Wang | Pose-Invariant 3D Proximal Femur Estimation through Bi-planar Image Segmentation with Hierarchical Higher-Order Graph-Based Priors[END_REF] where invariance to linear transformations has been introduced through the use of higher order interactions between the nodes of the probabilistic graphical model. This approach was extended to handle the case of 3D objects projected to multiple 2D images in [START_REF] Boussaid | 3D Model-based Reconstruction of the Proximal Femur from Low-dose Biplanar X-Ray Images[END_REF], [START_REF] Wang | 3D Knowledge-Based Segmentation Using Pose-Invariant Higher-Order Graphs[END_REF], [START_REF] Wang | Pose-Invariant 3D Proximal Femur Estimation through Bi-planar Image Segmentation with Hierarchical Higher-Order Graph-Based Priors[END_REF]. In order to determine the exact region probabilities, [START_REF] Xiang | 3D Cardiac Segmentation with Pose-Invariant Higher-Order MRFS[END_REF], [START_REF]Tagged cardiac MR image segmentation using boundary & regional-support and graph-based deformable priors[END_REF] re-expressed the exact integral using third order cliques through the use of Stokes/divergence theorem resulting on a novel local shape model that is invariant to global transformations while being able to determine exactly the associated image support. The model complexity was reduced through sparsity constraints [START_REF] Xiang | Pose Invariant Deformable Shape Priors Using L1 Higher Order Sparse Graphs[END_REF]. Last but not least the idea of decoupling image and model-based segmentation was also considered in [START_REF] Xiang | Joint Model-Pixel Segmentation with Pose-invariant Deformable Graph-Priors[END_REF], where the latent variables correspond both to the model deformation towards the image as well as to the individual labels of pixels (that are jointly optimized). Cardiac segmentation both in 2D (MR Tagged images) as well as in 3D (Computed Tomography) of the myocardium was the clinical example considered to demonstrate the interest of such a method. Introducing more complex geometric properties in the context of articulations [START_REF] Kadoury | Automatic inference of articulated spine models in CT images using high-order Markov Random Fields[END_REF], [START_REF] Kadoury | Multimodal inference of articulated spine models from higher order energy functions of discrete MRFS[END_REF] was a further development in the same direction targeting spine/vertebra segmentation. The idea was to represent the spine through a probabilistic graphical model endowed with higher order interactions encoding the relative geometric positions of successive vertebras. In order to cope with the gap between the dimensionality of the considered representation and the number of examples within the training set, non-linear manifold embedding methods were also introduced [START_REF] Kadoury | Spine Segmentation in Medical Images Using Manifold Embeddings and Higher-Order MRFs[END_REF], [START_REF] Kadoury | Nonlinear Embedding towards Articulated Spine Shape Inference Using Higher-Order MRFs[END_REF]. An alternative to point distribution models that has gained recently important attention refers to atlas-based methods [START_REF] Besbes | Graph-based knowledgedriven discrete segmentation of the left ventricle[END_REF]. The idea is to deform an annotated atlas to a new image and then use the deformation to determine the anatomical structures in the new image. Spine segmentation was investigated in [START_REF] Kadoury | Surface/volume-based articulated 3d spine inference through markov random fields[END_REF] while brain segmentation in the presence of tumors [START_REF] Parisot | Joint Tumor Segmentation and Dense Deformable Registration of Brain MR Images[END_REF], [START_REF] Parisot | Uncertainty-driven Efficiently-Sampled Sparse Graphical Models for Concurrent Tumor Segmentation and Atlas Registration[END_REF] was considered as well where the aim was to use a healthy anatomical atlas as a prior and relax the constraint of imageto-atlas registration in the tumorous area. This concept was explored in [START_REF] Sotiras | Atlas-based deformable mutual population segmentation[END_REF] through a population registration framework [START_REF] Sotiras | Graphical models and deformable diffeomorphic population registration using global and local metrics[END_REF] seeking to simultaneously deform n-images towards the target image and determine the optimal segmentation map in the new image through the combination of the deformed atlases labels.

B. Deformable Registration & Longitudinal Modeling

Global or linear registration is a preliminary step of almost all medical image analysis tools either for longitudinal modeling or for population studies. In [START_REF] Kokiopoulou | Optimal similarity registration of volumetric images[END_REF] we introduced the first method able to guarantee the globally optimal solution in the mono-modal case. This was achieved through a re-expression of the objective function as a difference of convex functions and the use of cutting planes algorithms to reach the optimal solution. Such a re-expression was based on a dictionary driven representation using a pre-defined base where both images were expressed as a linear combination of the dictionary elements. In order to deal with the multi-modal case, more recently we have investigated the use of graphical models [START_REF] Zikic | Linear intensity-based image registration by Markov random fields and discrete optimization[END_REF] and discrete optimization on the parameters acting directly on the linear transformation [START_REF] Glocker | Linear image registration through mrf optimization[END_REF] that was also considered for 3Dto-2D registration in [START_REF] Zikic | Markov Random Field Optimization for Intensity-based 2D-3D Registration[END_REF]. Concerning deformable registration [START_REF] Sotiras | Deformable Medical Image Registration: A Survey[END_REF], which is the pillar of medical image analysis, in [START_REF] Glocker | Dense image registration through mrfs and efficient linear programming[END_REF] 2 we have introduced a low graphical model formulation coupled with efficient linear programming to efficiently and precisely address mono and multi-modal iconic registration [START_REF] Glocker | Non-rigid Registration using Discrete MRFs: Application to Thoracic CT Images[END_REF]. The proposed approach was endowed with modularity, scalability and computational efficiency. Furthermore, inspired from [START_REF] Glocker | Dense image registration through mrfs and efficient linear programming[END_REF] the problem of coregistration of multiple volumes exhibiting partial overlap was addressed using graphical models leading to an efficient deformable stitching algorithm for whole body acquisitions [START_REF] Wachinger | Deformable mosaicing for whole-body mri[END_REF]. Improving computational efficiency and bringing the method closer to real clinical settings was investigated in [START_REF] Alchatzidis | Efficient parallel message computation for MAP inference[END_REF] where a novel fully parallelizable approach for the optimization of graphical models in graphics processing units was adopted leading to two orders of magnitude acceleration.

In [START_REF] Ou | DRAMMS: Deformable registration via attribute matching and mutual-saliency weighting[END_REF], [START_REF] Sotiras | A Kernel-based graphical model for diffusion tensor registration[END_REF] this framework has been extended to cope with multi-dimensional feature spaces while at the same time the idea of mutual saliency (on invariant Gabor features) [START_REF] Ou | DRAMMS: Deformable registration via attribute matching and mutual-saliency weighting[END_REF] was introduced that changes fundamentally the way image similarity costs are taken into account in a qualitative manner. Such a novel qualitative metric is able to handle missing correspondences and drive the registration to the optimal solution even from a very bad initial configuration. In the same direction but through a different concept that relies on objective function residuals with respect to the different labels in [START_REF] Glocker | Optical flow estimation with uncertainties through dynamic mrfs[END_REF] we have introduced the notion of uncertainties of the registration solution through the approximation of the solution covariance matrix using the min-marginal energies. This has led to an adaptive discrete sampling of the label space improving substantially the quality of the obtained results (due to the efficient handling of the search space) while providing novel means to appropriately quantify/qualify the physical solution.

Given that deformable registration is an ill-posed problem, it is often handled through the convexification of the objective function using the regularization term. An alternative, clinical context specific approach was introduced [START_REF] Glocker | Dense registration with deformation priors[END_REF] where we have proposed a novel learning method that was invariant to linear transformations to capture the relative displacements of organs with a deformable registration framework and consider them as priors subsequently.

Furthermore, integration of anatomical landmarks coupled with iconic registration was another step forward. An interconnected layer approach was considered in [START_REF] Glocker | Deformable Medical Image Registration: Setting the State of the Art with Discrete Methods[END_REF], [START_REF] Sotiras | Simultaneous Geometric -Iconic Registration[END_REF] where we are seeking simultaneously to determine the optimal iconic mapping and the optimal landmark association while imposing consistency with respect to the associated transformations. The parameters of the two graphical models were simultaneously inferred providing dense deformation along with landmarks correspondences. Symmetry was also a property that was naturally imposed to the formulation through a deformation from a common space to both modalities with inverse consistency [START_REF] Sotiras | Discrete symmetric image registration[END_REF]. Furthermore, the same idea was explored in the context of genetic imaging data either for registration [START_REF] Kurkure | Landmark/image-based deformable registration of gene expression data[END_REF] or for a model-based segmentation/partition [START_REF] Le | Similarity-based appearance-prior for fitting a subdivision mesh in gene expression images[END_REF], [START_REF] Kurkure | Markov Random Field-based fitting of a subdivision-based geometric atlas[END_REF].

The problem of image to volume registration, a more challenging component of fusion has been recently investigated [START_REF] Ferrante | Non-rigid 2D-3D Medical Image Registration using Markov Random Fields[END_REF]. The objective is to determine an optimal plane and within this plane the associated deformations that will map an intraoperative low resolution image (like for example radiography or ultrasound) to a high resolution anatomical data. Examples of use of such an approach refer to image-based surgery guidance and adaptive radiotherapy. The problem was formulated as an over-parameterized pair-wise graphical model in [START_REF] Ferrante | Non-rigid 2D-3D Medical Image Registration using Markov Random Fields[END_REF] where we seek both the optimal plane and the associated deformation model. Over-parameterization was adopted to impose unique plane consistency. An alternative higher order approach was recently adopted that implicitly imposes unique plane consistency and determines the optimal deformation through third and fourth order potentials estimated on the 3D deformable vectors.

V. CONCLUSION

Despite their tremendous use, graphical models have been mostly employed to handle low rank interactions that suffer from the ability to cope with rich models as well as encode better priors. Furthermore, the dimensionality of the label set space was a major issue.

In order to deal with a large number of labels, designing hierarchical divide-and-conquer style algorithms is a promising direction through multi-grid methods [START_REF] Komodakis | Towards more efficient and effective lp-based algorithms for mrf optimization[END_REF]. While divide-andconquer will increase the number of problems that will be required to be solved, each problem will be defined on a small set of similar labels, corresponding to a cluster within a hierarchical clustering of labels. In order to allow for general high-order potentials, we will design iterative algorithms that approximate arbitrary potentials with their sparse, non-linear envelope alternatives. The approximation will change dynamically over the iterations to ensure accuracy. Specifically, the parameters of the non-linear envelope will be determined by both the original clique potential as well as the current estimate of the solution. Finally, in order to handle a large number of variables, we will build on the dual decomposition framework which iteratively solves subproblems defined on a subgraph of the given model. The subproblem definitions will be changed dynamically in order to encourage faster convergence.

Learning task-specific graphical models is another promising direction. In the early years of graphical models, limited effort was invested on determining the optimal combination of such terms as they were mainly restricted to pair-wise graphical models of very limited complexity involving a small number of global parameters. Learning the optimal parameters of a model given a set of annotated data can be expressed as a problem of modeling dependencies between variables that minimize a loss function between the model prediction and the annotated solutions that in general is a non convex problem. Solving the convex relaxation of the expected loss through algorithms like the cutting plane, was a pioneering step forward to address such a learning problem. In [START_REF]Learning to cluster using high order graphical models with latent variables[END_REF] a framework for learning the optimal graph structure for clustering problems was introduced while in [START_REF]Efficient training for pairwise or higher order crfs via dual decomposition[END_REF] a generic framework for learning the potentials of pair-wise as well as high-order graphical models is presented combining the dual decomposition and the max-margin concept resulting on a fully distributed approach to parameter learning composed of subproblems of limited complexity.

Bridging the gap between data-driven & physics-based modeling is a promising step forward in artificial vision. Modeling in biomedical imaging has been either physicsbased driven or data-driven. The former case suffers from computational complexity and efficiency limitations, the later from interpretability while being also heavily dependent on the design of the objective function. The use of annotated data along with the progress made in the field of dimensionality reduction and in the optimization of higher order graphical models do make possible the training and use of large scale models. Consequently, reducing the gap between physical and data-driven modeling could be of great interest and could have tremendous impact on the efficient and automatic interpretation of the data in the future.

DROP is a deformable registration platform in C++ for the medical imaging community (publicly available at http://www.mrf-registration.net ) developed at Ecole Centrale de Paris, Technical University of Munich and University of Crete. This is the first publicly available platform which contains most of the existing metrics to perform registration under the same concept.

ACKNOWLEDGMENT

The authors would like to thank all contributors of the papers being cited in the reference section.


" Uillaume Munch-Maccagnoni
email: munch-maccagnoni@lipn.univ-paris13.fr

Formulae-as-Types for an Involutive Negation *

Keywords: ".3.3 [Logics and meanings of programs]: Studies of Program Constructs; ".4.1 [Mathematical logic and formal languages]: Mathematical Logic Lambda calculus and related systems, Proof theory Classical logic, "ormulae-as-types, Delimited control operators, Continuations, Polarization, "ocalization

Negation is not involutive in the calculus because it does not distinguish captured stacks from continuations. We show that there is a formulae-as-types correspondence between the involutive negation in proof theory, and a notion of high-level access to the stacks studied by "elleisen and Clements.

We introduce polarised, untyped, calculi compatible with extensionality, for both of classical sequent calculus and classical natural deduction, with connectives for an involutive negation. The involution is due to the ℓ delimited control operator that we introduce, which allows us to implement the idea that captured stacks, unlike continuations, can be inspected. Delimiting control also gives a constructive interpretation to falsity. We describe the isomorphism there is between and ¬¬ , and thus between ¬∀ and ∃¬.

Introduction

Constructiveness in classical logic is based on di erent assumptions than in intuitionistic logic. In order to give constructive contents to classical axioms such as excluded middle (∀ , ¬ ), we assume that we restrict the disjunction property, the property of existence… to formulae that are purely positive ("irard [START_REF] Muller | irard, A new constructive logic: Classical logic[END_REF]). "or instance, in arithmetic, purely positive formulae correspond to Σ 0 1 formulae. As a consequence, proofs of formulae ∀⃗ ⃗ ) → ⃗ )) where , are purely positive that is to say Π 0 2 formulae in arithmetic correspond to algorithms (Murthy [START_REF]An evaluation semantics for classical proofs[END_REF]).

One way to provide constructive contents to classical proofs is by considering variants of the "ödel-"entzen double-negation translations, such as "riedman's [START_REF] Harvey | riedman, Classically and intuitionistically provably recursive functions, Higher Set Theory[END_REF]. We can translate classical proofs of ⊢ into intuitionistic proofs of ⊢ → ) → , where is the translation of and where is chosen arbitrarily. When is does not depend on and, furthermore, we have = . Therefore, in this special case we can take = and deduce an intuitionistic proof of ⊢ → ) → and, in turn, one of ⊢ . In the other cases, the translation describes in fact how the behaviour of classical proofs depends on the context in which classical axioms are invoked. Thus the interpretation does not contradict intuitionism: the latter assumes that the behaviour of proofs is referentially transparent, while here we do not make such an assumption. This is why proofs of ∀ , ¬ do not provide a decision procedure for in general.

, ⩴ | . | | (a) Quasi-proof terms , ∶ ⊢ ∶ ⊢ ∶ ¬¬ → , ∶ ⊢ ∶ ⊢ . ∶ → ⊢ ∶ → ⊢ ∶ ⊢ ∶ ⊢ ∶ * ⊢ ∶ ∀x ⊢ ∶ ∀x ⊢ ∶ [∉/x]
In this article, we are interested in the constructive interpretation of reasoning by contrapositive, or, in other words, of an involutive negation. In terms of double-negation translations, we must consider two techniques:

• "irard's polarisation [START_REF] Muller | irard, A new constructive logic: Classical logic[END_REF], which distinguishes negative formulae (which are translated di erently, into ⊢ * → ) in addition to the positive , and which was introduced precisely for the purpose of interpreting a negation satisfying ¬¬ = ;

• The interpretation of falsity from Herbelin, Ariola and "hilezan [START_REF] Ariola | Minimal Classical Logic and Control Operators[END_REF][START_REF] Herbelin | hilezan, An Approach to Call-by-Name Delimited Continuations[END_REF][START_REF]A type-theoretic foundation of delimited continuations[END_REF], closely related to "riedman's trick [START_REF] Harvey | riedman, Classically and intuitionistically provably recursive functions, Higher Set Theory[END_REF].

Formulae-as-types

The previous notion of constructiveness is best understood through the interpretation of formulae as types in a programming language.

"riffin [START_REF]riffin, A Formulae-as-Types Notion of Control[END_REF] showed that double negation elimination can be implemented with "elleisen's variant [START_REF] Matthias "elleisen | Duba, A syntactic theory of sequential control[END_REF] of the call/cc operator of Scheme ("igure 1 recalls the calculus). Also, from this point of view, double-negation translations such as "irard's correspond to continuation-passing style compilation schemes for calculi with such [START_REF] Chetan | Extracting constructive content from classical proofs[END_REF][START_REF]A Computational Analysis of Girard's Translation and LC[END_REF]). Now, as is well known, in the presence of side-e ecting operations (control operators, state, input/output, etc.), programs of certain types (functions, thunks, etc.) are opaque at runtime. In fact, programming languages usually guarantee to respond with absolute values only for simple enough types (integers, etc.).

One may think that double-negation translations have reduced classical proof theory to intuitionistic proof theory. But, given the wealth of double-negation translations, understanding the translations is at least as important as understanding the intuitionistic target. A direct interpretation of classical logic, by means of dedicated term calculi, amounts to studying both at the same time. It brings the combined advantages of succinctness and exibility.

The simplest way to describe the reduction of calculi with control operators is with abstract machines. Let us recall Streicher and Reus's [START_REF] Streicher | Classical Logic, Continuation Semantics and Abstract Machines[END_REF] variant of the Krivine (call-by-name) abstract machine in "igure 1. One insight is to enrich the set of terms with an operation that appears during reduction, but which does not make sense for natural deduction.

The original terms, without , are quasi-proofs. This is because we consider that logical systems only approximate constructive behaviours, just like type systems approximate correct programs a point of view advocated by Krivine [START_REF]Realizability in Classical Logic[END_REF][START_REF] Krivine | Lambda-calculus, types and models[END_REF] and "irard [START_REF]Locus Solum: From the Rules of Logic to the Logic of Rules[END_REF]. Thus, quasi-proofs are algorithmically more diverse than proofs, because they need not be typable. But they are somehow compatible with natural deduction, unlike , in the sense that we could use them to extend the logic with new axioms. In this article, stating the results for untyped calculi guarantees more generality.

Involutive negation

Assuming ¬ ≝ → ⊥, then the control operator participates in an equivalence ¬¬ ↔ , but not in an isomorphism of types ¬¬ . The reason for asking more than a mere equivalence between and ¬¬ is that there are too many choices for the contrapositive of a proposition such as the following:

∀x, y , x) y)) → ∀x , x)) ∀y , y))
for instance:

¬ ∀x , x)) ∀y , y)) → ¬∀x, y , x) y)) ¬∀x , x)) ¬∀y , y)) → ∃x, y , ¬ x) y)) ∃x , ¬ x)) ∃y , ¬ y)) → ∃x, y , ¬ x) ¬ y))
We are no longer overwhelmed with choices once De Morgan laws are type isomorphisms: if there are too many proofs, then we must be able to choose a canonical one, one whose meaning is preserved.

In the calculus, however, a proposition as simple as the following (assuming that ∃ is obtained through the second-order encoding):

¬∀x ℕ, → ∃y ℕ, ¬

has a proof with the following skeleton:

. . . . )))))
Thus, in , such an elementary classical tautology has a nonobvious computational role, due to the presence of two control operators. More generally, reasoning by contrapositive is not immediate in the calculus due to the absence of isomorphisms of types such as ¬∀x ∃x ¬ , following from the absence of an involutive negation. But, works such as the one of Krivine [START_REF]Realizability in Classical Logic[END_REF] show from a technical standpoint the importance of reasoning by contrapositive; for instance, the axiom of countable choice is only realised through its contrapositive.

Captured contexts are not continuations

As we will see, the computational contents of the De Morgan law [START_REF] Ariola | Minimal Classical Logic and Control Operators[END_REF] is as simple to understand as: 1) capturing the stack of the form ⋅ that appears during the head reduction of the argument; 2) decomposing it into head and tail, and return a pair , ) where is the captured form of the tail. This contrasts with the proof in the calculus, which is convoluted because captured contexts are identi ed with continuations. By continuation we mean the functional abstraction of the remainder of a computation. Thus, the contents of the captured context, which is represented by a functional value, cannot be accessed in an immediate way.

That captured contexts are more primitive than continuations is obvious in programming languages, with the examples of the operation getcontext in the language C or the operation thisContext in the language Smalltalk, where the contents of captured contexts can be accessed. "elleisen sketched a control operator that would theorise this distinction in a note at the end of Ariola and Herbelin [START_REF]Control Reduction Theories: the Bene t of Structural Substitution[END_REF]. Then, Clements showed advantages of enabling a high-level access to the components of the contexts, such as obtaining portable, high-level implementations for debuggers [START_REF] Clements | Portable and high-level access to the stack with continuation marks[END_REF].

In this paper, we establish the link between the idea theorised by "elleisen and Clements and the remarks below by "irard and by Krivine by which negation should be treated di erently from the connective ⋅ → ⊥.

1) "irard gave with his sequent calculus LC [START_REF] Muller | irard, A new constructive logic: Classical logic[END_REF] an interpretation for an involutive negation. "irard's approach distinguishes positive ( , … ) and negative ( , … ) formulae. Negation is given as an involutive mapping that inverts the polarity of the formula, thus it is strictly involutive (¬¬ = ). It is therefore not given as a connective, which led some authors to qualify the computational contents of LC's negation as not clear . 1 However, according to "irard [15, p. 9], the identi cation of ¬¬ with is not essential to [his] approach .

In fact, the main insight of LC is, to us, the idea that the introduction rules in sequent calculus of negation, taken as a connective, hide cuts. In other words, the following focalisation steps have to be performed during cut-elimination in classical sequent calculus, when is not simple enough (i.e. linear):

, ⊢ ⊢ ¬ , , ¬ ⊢ , ⊢ , ⊢ ⊢ ¬ , , ¬ ⊢ ⊢ , , ⊢ , ⊢ , ⊢ ¬ , ⊢ , , ¬ ⊢ , ⊢ , ⊢ , ⊢ ¬ , ⊢ , ¬ ⊢ , ⊢ , ⊢ ,
These cut-elimination steps invert the order of and in the tree. As we will see, the rst cut-elimination step above is incompatible with the functional interpretation of negation ( → ⊥), and requires that ¬ is given a positive polarity. The second cut-elimination step above is compatible with interpreting ¬ as the negative type → ⊥, but will correspond to evaluating the argument by value.

2) A technique of Krivine alleviates the complexity of reasoning in the calculus, by allowing certain pseudo-types of a positive tinge to the left-hand side of implications [START_REF]Realizability in Classical Logic[END_REF][START_REF]Structures de réalisabilité, RAM et ultra ltre sur N[END_REF]. An essential pseudo-type in Krivine's work is -, de ned as the set ‡ | }. This also amounts to distinguishing a type of captured stacks from the type of continuations ( → ⊥). The di erence is, we will do so in a direct manner, making such types rst class, in the sense that we de ne their meaning also when they are on the right-hand side of implications.

Formulae-as-types for an involutive negation

Our goal is to describe a natural deduction for classical logic with an involutive negation inspired by "irard, which realises a formulae-astypes correspondence with the idea of exposing a high-level interface to captured stacks. "ollowing the above, we introduce a positive type ∼ of inspectable stacks, together with constants ( … ) that provide access to the components of these stacks. The type ∼ is therefore distinct from the negative type → ⊥ of continuations. The involutive negation is then de ned in function of the polarity:

¬ ≝ → ⊥ ¬ ≝ ∼
De ning the negation in function of the polarity of the sub-formula is reminiscent of Danos, Joinet and Schellinx [START_REF] Vincent Danos | A New Deconstructive Logic: Linear Logic[END_REF].

Our setting admits extensionality (-like) rules, which are used to establish the isomorphism between ¬¬ and . It is also untyped (Curry-style), so that there is generality in the involution result and it is not restricted to, say, predicate calculus.

Delimited control as an interpretation of falsity.

In the setting that we introduce, we use control delimiters to provide a constructive interpretation for falsity (⊥). Control delimiters model the fact that the context has a nite extent, and are absent from the calculus. In terms of continuation-passing-style translations, the presence of control delimiters means that continuations can return and be composed. In this aspect, we follow the proof theoretic interpretation of delimited control by Herbelin and others [START_REF] Herbelin | hilezan, An Approach to Call-by-Name Delimited Continuations[END_REF][START_REF]A type-theoretic foundation of delimited continuations[END_REF][START_REF] Herbelin | An Intuitionistic Logic that Proves Markov's Principle[END_REF][START_REF] Ilik | Delimited control operators prove double-negation shift[END_REF].

We found necessary to interpret falsity using delimited control because of our choice of being untyped. In this context, giving an interpretation to falsity compatible with extensionality, as we will see, is not immediate. 2 Thus our result shows how although delimited control does not prove new formulae compared to nondelimited control in the context of predicate calculus, it already gives better proofs from a constructive standpoint.

Computational interpretation of polarisation. Our approach, like "irard's, is only sound when both polarities are taken into account. One important contribution of this article is that we investigate a direct computational interpretation of polarities.

We build on our previous work [START_REF]uillaume Munch-Maccagnoni, Focalisation and Classical Realisability[END_REF] where negation was strictly involutive. There, we introduced the idea that positive and negative formulae are the types of strict and lazy terms (respectively) for the notion of polarity taken from "irard's LC. Strict involution meant that terms were identi ed with contexts. In this article, we restore the distinction between terms and contexts, and we also investigate how polarisation can be formulated in natural deduction, through a calculus with control operators (the ℓ calculus we introduce). We found that the latter task was not immediate, and we are not aware of any other model of an involutive negation in natural deduction which does not identify all proofs.

There is a technical reason for investigating a natural deduction variant of polarised classical logic. It is needed for having a notion of quasi-proofs. Yet quasi-proofs are essential in Krivine's programme for recovering models, in the sense of model theory, from classical realisability models [START_REF]Realizability algebras II : new models of ZF + DC[END_REF]. Like the calculus, the ℓ calculus determines such a language of quasi-proof terms, in a sense that we will make precise.

This article is a companion to M.-M. [START_REF]Models of a non-associative composition[END_REF] in which we give a direct characterisation of polarisation through a categorical structure where the associativity of composition is relaxed. The ℓ calculus fails to satisfy the associativity of composition, which is justi ed by the latter result.

Contributions

In Section 2, we review the relationship between sequent calculus and abstract machines and we introduce the untyped calculus L pol, and the corresponding sequent calculus. Not all proofs are identi ed, even in the presence of -like rules.

In Section 3, we introduce the untyped calculus ℓ which provides the notion of programs, or quasi-proof terms, and we introduce the corresponding natural deduction. The method is to decompose it through the calculus L pol, , from which it inherits an extensional equivalence on terms and therefore the type isomorphisms. "inally, in Section 4 we show that negation as de ned above is involutive.

References. This article can be seen as a successor to Murthy's computational analysis of "irard's LC [START_REF]A Computational Analysis of Girard's Translation and LC[END_REF], enriched with the subsequent advances in the proof theory of classical sequent calculus (in particular Danos, Joinet and Schellinx [START_REF] Vincent Danos | A New Deconstructive Logic: Linear Logic[END_REF] and Laurent [START_REF] Laurent | Etude de la polarisation en logique[END_REF]), in the representation and computational interpretation of sequent calculus (Curien and Herbelin [START_REF] Curien | The duality of computation[END_REF]) and in the theory of (delimited) control operators (in particular Herbelin et al. [START_REF] Ariola | A Type-Theoretic Foundation of Continuations and Prompts, IC"P '04[END_REF][START_REF]Control Reduction Theories: the Bene t of Structural Substitution[END_REF][START_REF]A type-theoretic foundation of delimited continuations[END_REF]).

Acknowledgements. I wish to thank Pierre-Louis Curien, Pierre-Évariste Dagand, Olivier Danvy and Thomas Streicher for their careful reading, criticisms and suggestions about the thesis chapter. I wish to thank Jean-Yves "irard, Hugo Herbelin, Paul-André Melliès and Alexandre Miquel for the related discussions. Thanks to the anonymous reviewers for criticisms and suggestions. This work has been partially supported by the "rench National Research Agency3 .

Involutive negation in sequent calculus

Notations

If is a rewriting relation, then * denotes the re exive and transitive closure of ; the compatible closure of is denoted by → and the compatible equivalence relation ← ∪ →) * is denoted by . Reductions are denoted with R and expansions with E . In this context we de ne RE ≝ R ∪ E .

The constructive interpretation of sequent calculus

The calculus is universal because it represents combinators abstractly by their reduction rules. "or instance, it suffices to write down the rule ≻ ) to not only infer . ), but also to propose = . ) as a de nition, as if the reduction rule was an equation in and the calculus a convenient mean to build solutions.

= ⊝ ⩴ | . | . = ⊝ ⩴ | . ⊝ ⩴ | | ⋅ ⩴ ‖
(a) Terms, contexts, stacks and commands

‖ . R [ / ] . ‖ R [/ ] . ‖ ⋅ R [ / ]‖ (b) Reduction rules E . ‖ E . ‖ E . . ‖ ⋅ (c) Expansion rules ≝ . ‖ ⋅ ≝ . . ‖ ≝ . . ‖ ⋅ (d) Embedding the calculus = ⃗ ∶ ⃗ , = ⃗ ∶ ⃗ ⊢ ∶ | , | ∶ ⊢ , ∶ ⊢ ) (e) Judgements (⊢ ax) ∶ ⊢ ∶ | (ax ⊢) | ∶ ⊢ ∶ ∶ , ∶ ⊢ ) ( ⊢) | . ∶ ⊢ ∶ ⊢ ∶ , ) (⊢ ) ⊢ . ∶ | ⊢ ∶ | | ∶ ⊢ (cut) ‖ ∶ , ⊢ , ) (f) Identity ∶ ⊢ ) (w ⊢) ∶ , ∶ ⊢ ) ∶ , ∶ , ∶ ⊢ ) (c ⊢) [ / ] ∶ , ∶ ⊢ ) ∶ ⊢ ) (⊢ w) ∶ ⊢ ∶ , ) ∶ ⊢ ∶ , ∶ , ) (⊢ c) [ / ] ∶ ⊢ ∶ , )
and 8 similar rules with and replacing .

(g) Structure The sequent calculus ( L ) approach, pictured by Curien and Herbelin's calculus ("igure 2, top), is universal because it extends the previous point of view to the transitions of abstract machines. The binder , which binds stacks to co-variables , … , is introduced to abstractly represent terms by their transitions in a machine. "or instance, the operations of the calculus are characterised by their action on stacks (below, on the left), which de ne equations that we solve in the calculus (on the right):

, ∶ ⊢ ∶ | (⊢ →) ⊢ . ∶ → | ⊢ ∶ | | ∶ ⊢ (→ ⊢ ) , | ⋅ ∶ → ⊢ , ⊢ ∶ | (⊢ ∀ 1 ) * ⊢ ∶ ∀x | | ∶ [∈/x] ⊢ (∀ 1 ⊢) | ∶ ∀x ⊢ (⊥ ⊢) | ∶ ⊥ ⊢ (h) Logic
∶ ↦ ‖ ⋅ ≝ . ‖ ⋅ ∶ ⋅ ↦ ‖ ≝ . . ‖ ∶ ⋅ ↦ ‖ ⋅ ≝ . . ‖ ⋅
These de nitions induce a translation from the calculus into the calculus that simulates reduction: Proposition 1 (Simulation). (Identifying machines of the calculus with commands of the calculus ,) If ≻ then + R . The abstract notation of reduction rules brings along three important simpli cations [START_REF] Curien | The duality of computation[END_REF][START_REF] Wadler | Call-by-value is dual to call-by-name[END_REF][START_REF]Control Reduction Theories: the Bene t of Structural Substitution[END_REF]: 1) thanks to the addition of explicit contexts, the equational theory is simpler to describe than in the calculus or its variants; 2) the possible choices regarding the order of evaluation appear clearer, as it displays a symmetry between call by value and call by name; 3) typing rules are in correspondence with the ones of the sequent calculus.

A correspondence with sequent calculus

The calculus gives a constructive interpretation in call-byname to the ∀, →, ⊥ fragment of "entzen's classical sequent calculus LK [START_REF]erhard "entzen, Untersuchungen über das logische Schließen[END_REF] ("igure 2, bottom). To "entzen's cut is associated the following typing rule:

⊢ ∶ | | ∶ ⊢ ‖ ∶ , ⊢ , ) becomes an environment of term variables ( 1 ∶ 1 , … , ∶ ) and becomes an environment of co-variables, ( 1 ∶ 1 , … , ∶ ). ✄ ✂ ✁ ⊢ ∶ | , | ∶ ⊢ , ‖ ∶ ⊢ )
In the above frame, the rst judgement is familiar: the type of a term is given by a conclusion of a sequent. The bar delineates which particular formula it is; this distinction corresponds in sequent calculus to the notion of principal or active formula. The second judgement describes the type of a stack by an hypothesis of the sequent, and reads is a refutation of in the context , . The third judgement gives types to variables of a machine ‖ , which has no type on its own. Notice that the cut is formulated in multiplicative rather than additive style (the contexts are split).

The slogan is that the reduction of commands corresponds to cut elimination (with the convention that we don't necessarily consider ‖ or ‖ a cut, as suggested by Wadler [44]).

Adjoints

Elimination rules are obtained as the adjoints of left introduction rules, through the de nition:

✄ ✂ ✁ * ) ≝ . ‖ )
The adjoint de nes an operation that satis es:

* )‖ R ‖ )
hence the name. "or instance, the derivation of the elimination rule of → in LK indeed gives = ⋅-) * ), since it corresponds to the following derivation:

⊢ ∶ → | ⊢ ∶ | (ax ⊢) | ∶ ⊢ ∶ (→⊢) | ⋅ ∶ → ⊢ ∶ , (cut) ‖ ⋅ ∶ , ⊢ ∶ , , ) (⊢ ) , ⊢ ⋅-) * ) ∶ | ,
The typing rules of the calculus can be derived (in multiplicative style 4 ) from the rules of "igure 2. The abstract notation and the de nition using adjoints solve the problem of commutative cuts in natural deduction (see M.-M. [START_REF]Syntax and models of a non-associative composition of programs and proofs[END_REF]). The name adjoint is taken from "irard [START_REF]Locus Solum: From the Rules of Logic to the Logic of Rules[END_REF].

Non-linear contexts

Stacks (notation ) are linear contexts, in the sense of linear logic (see Laurent [START_REF] Laurent | Etude de la polarisation en logique[END_REF]). Curien and Herbelin introduced the binder that builds non-linear contexts (notation ). They represent contexts de ned in terms of their interaction with a term. The abstract machine for the calculus only uses stacks: this is because stacks are sufficient if the goal is to describe the head reduction of a term. Adding is necessary to recover the correspondence between the syntax and the sequent calculus, as we will see below. It also makes the choice of evaluation order explicit, because it forces us to determine which of the binder or has the priority over the other in the reduction.

The context . ‖ is introduced by the following rule:

‖ ∶ , ∶ ⊢ ) ( ⊢) | . ‖ ∶ ⊢
Negative polarity Terms of the calculus are negative. Here this means that the reduction of is restricted to contexts that are stacks, and that the priority is given to the binder:

⊝ ‖ ⊝ . R [ ⊝ / ⊝ ] , ⊝ . ‖ ⊝ R [ ⊝ / ⊝ ]
Thus, the evaluation of a negative term is delayed until it comes in head position, in the terminology of the calculus. In the calculus , head position is determined by the fact that the context is a stack.

The distinction between stacks and negative contexts also appears in the rule → ⊢ ): only stacks are allowed as a premiss. This is a focalisation constraint: it essentially means that the generic rule, which can be derived in terms of the restricted rule, hides a cut:

⋅ ≝ . ‖ = . . ‖ ⋅ ‖ ⊢ ∶ | | ∶ ⊢ (→ ⊢) , | ⋅ ∶ → ⊢ ,
In other words, in the calculus, priority is given to the evaluation of the context inductively:

‖ ⋅ → * R . ‖ ⋅ ‖ when is not a stack
As noticed by Danos, Joinet and Schellinx [START_REF] Vincent Danos | A New Deconstructive Logic: Linear Logic[END_REF], focalisation is notably meant to ensure the compatibility of reductions with expansions. Indeed, if we were to treat ⋅ as a stack, i.e. if we considered the following rules:

. ‖ ⋅ R' [ ⋅ / ] , . ‖ ⋅ R'
[ / ]‖ then unsolvable critical pairs would arise in the presence of expansions:

[ ⋅ . / ] R' . ‖ ⋅ . → E . . . ‖ ⋅ ‖ ⋅ . R' . . . ‖ ⋅ ‖ . R [ . . . ‖ ⋅ / ]
Positive polarity In the L pol, calculus introduced in the next section, we add a positive polarity. The positive de nes a stack (in our terminology), and when a cut is between positive term and context, the reduction of is restricted to terms that are values ( , to be introduced), which gives the priority to the binder:

+ ‖ + . R [ + / + ] , + . ‖ + R [ + / + ]
This corresponds to a call-by-value evaluation of positive terms, de ned with their transition rules using the binder.

In the positive polarity, focalisation appears for terms. "or instance, in the calculus introduced next section, pairs hide cuts in general because they compute down to values by inductively computing their components via rules (reusing Wadler's [START_REF] Wadler | Call-by-value is dual to call-by-name[END_REF] terminology):

+ , )‖ + R + ‖ . , )‖ + when + is not a value , + )‖ + R + ‖ . , )‖ + when + is not a value

The calculus L pol,

In this section we introduce the calculus L pol, . We present the calculus L pol, in "igure 3. It enriches the calculus with: • The positive conjunction ⊗, with the corresponding focusing rules;

• The positive negation ∼, and the corresponding focusing rule;

• Alternate rules for ⊥ for which we introduce the operators and .

Let-bindings

The binder allows us to derive below a let-binding:

✄ ✂ ✁ ≝ . ‖ . ‖
The term has the same polarity as . Similarly, the binder is used to decompose pairs of values:

✄ ✂ ✁ , ) + ≝ . + ‖ , ). ‖

The operator

The goal with is to reconcile the rule (⊥ ⊢) with extensionality equations. The difficulty comes from the fact that at type ⊥, the natural equation for the calculus (∀, ) implies that all the terms are identi ed. In L pol, , is replaced by , whose essential di erence is to invalidate the following equation:

⊝ . ‖ ⋫ [ / ⊝ ]
The reduction of . is possible only when is of the form ⊝ ‖ :

. ⊝ ‖ R ⊝
The variable is bound dynamically: the above rule holds even if appears in ⊝ . Thus is not subject to the usual scoping andconversion rules.

In fact, the operator implements a list of stacks, de ned inductively as follows:

✄ ✂ ✁ ‡} ≝ ‡ 1 ⊝ , … , ⊝ } ≝ . ‖ 1 ⊝ ‡ 2
⊝ , … , ⊝ } And the context corresponds to an operation that extracts the head of the list:

⊝ ‖ ‡ 1 ⊝ , 2 ⊝ , … , ⊝ } → R ⊝ ‖ 1 ⊝ ‡ 2
⊝ , … , ⊝ } Per the above de nition,

. corresponds to the operation that adds a stack on top of the list. In typed settings we can expect these stacks to be of type ⊥. Using to interpret the elimination of falsity is inspired from Herbelin et al. [START_REF] Ariola | A Type-Theoretic Foundation of Continuations and Prompts, IC"P '04[END_REF][START_REF] Herbelin | hilezan, An Approach to Call-by-Name Delimited Continuations[END_REF].

Accessing stacks

In order to interpret the negation of a negative formula , we introduce the positive type ∼ of inspectable stacks. An inspectable stack is a value that denotes a captured stack and that exports accessors to its components. An inspectable stack is denoted with

+ = [].
The calculus L pol, introduces the binder [ ]. which is responsible for accessing the stacks. We extend it to a abstraction as follows:

[ ]. ≝ . . ‖ [ ]. ‖
"or instance, we can access the head of a captured stack and return it paired with the tail of the stack with the following function:

→ = [ ⋅ ]. , [ ]) ≝ [ ⊝ ]. + . . . , [ ])‖ + ‖ ⊝ ✄ ✂ ✁ … : Main additions to Figure 2. ⊝ ⩴ ⊝ | . | ⊝ . | ✄ ✂ ✁ . + ⩴ ✄ ✂ ✁ + | , ) | [ ] | + . { ⊝ + ⩴ ✄ ✂ ✁ + | , ) | [] ⊝ ⩴ ⊝ | ⋅ | ⊝ . | ✄ ✂ ✁ + ⩴ ✄ ✂ ✁ + | + . | , ). | [ ]. { ⊝ ⩴ ⊝ | ⋅ + ⩴ ✄ ✂ ✁ + ‖ + | ⊝ ‖ ⊝ (a)
Terms, values, contexts, stacks, and commands

) ‖ . R [ / ] ) . ‖ R [/ ] → ) . ‖ ⋅ R [ / ]‖ ✄ ✂ ✁ ⊗ ) , )‖ , ). R [ / , / ] ✄ ✂ ✁ ∼ ) [ ]‖ [ ]. R [ / ] ✄ ✂ ✁ ) . ⊝ ‖ R ⊝
When polarities match pairwise. Even if occurs in ⊝ .

✄ ✂ ✁

→ 1 )

⊝ ‖ + ⋅ R + ‖ . ⊝ ‖ ⋅ → 2 ) ⊝ ‖ ⋅ ⊝ R . ⊝ ‖ ⋅ ‖ ⊝ ✄ ✂ ✁ ⊗ 1 ) + , )‖ + R + ‖ . , )‖ + ✄ ✂ ✁ ⊗ 2 ) , + )‖ + R + ‖ . , )‖ + ✄ ✂ ✁ ∼ ) [ ⊝ ]‖ + R ⊝ . [ ⊝ ]‖ + ‖ ⊝ When + is not a value. When ⊝ is not a stack. (b) Reduction rules ) E . ‖ ) E . ‖ → ) ⊝ E . . ⊝ ‖ ⋅ ✄ ✂ ✁ ⊗ ) + E , ). , )‖ + ✄ ✂ ✁ ∼ ) + E [ ]. [ ]‖ + ✄ ✂ ✁ ) E . ‖ (c) Expansion rules , ⩴ → | ∀x | ⊥ ✄ ✂ ✁ , ⩴ ∈ 1 , … , ∈ ) | ⊗ | ∃x | ∼ , ⩴ | (d) "ormulae ¬ ≝ { ∼ if = → ⊥ if = (e) Negation ✄ ✂ ✁ ∶ ⩴ + ∶ | ⊝ ∶ for ‡ , , , } = ⃗ ∶ ⃗ , = ⃗ ∶ ⃗ ⊢ ∶ | , | ∶ ⊢ , ∶ ⊢ ) (f) Judgements (⊢ ax) ∶ ⊢ ∶ | (ax ⊢) | ∶ ⊢ ∶ ∶ , ∶ ⊢ ) ( ⊢) , . ∶ ⊢ ∶ ⊢ ∶ , ) (⊢ ) ⊢ . ∶ | ⊢ ∶ | | ∶ ⊢ (cut) ‖ ∶ , ⊢ , ) (g) Identity ∶ ⊢ ) (w ⊢) ∶ , ∶ ⊢ ) ∶ , ∶ , ∶ ⊢ ) (c ⊢) [ / ] ∶ , ∶ ⊢ ) ∶ ⊢ ) (⊢ w) ∶ ⊢ ∶ , ) ∶ ⊢ ∶ , ∶ , ) (⊢ c) [ / ] ∶ ⊢ ∶ , )
and 8 similar rules with and replacing .

(h) Structure , ∶ ⊢ ∶ | (⊢ →) ⊢ . ∶ → | ⊢ ∶ | | ∶ ⊢ (→ ⊢) , | ⋅ ∶ → ⊢ , ✄ ✂ ✁ ⊢ ∶ | ⊢ ∶ | (⊢ ⊗) , ⊢ , ) ∶ ⊗ | , ✄ ✂ ✁ ∶ , ∶ , ∶ ⊢ ) (⊗ ⊢) | , ). ∶ ⊗ ⊢ ✄ ✂ ✁ | ∶ ⊢ (⊢ ∼) ⊢ [ ] ∶ ∼ | ✄ ✂ ✁ ∶ ⊢ ∶ , ) (∼ ⊢) | [ ]. ∶ ∼ ⊢ ⊢ ⊝ ∶ | (⊢ ∀ 1 ) * ⊢ ⊝ ∶ ∀x | | ⊝ ∶ [∈/x] ⊢ (∀ 1 ⊢) | ⊝ ∶ ∀x ⊢ ✄ ✂ ✁ ⊢ + ∶ [∈/x] | (⊢ ∃) ⊢ + ∶ ∃x | ✄ ✂ ✁ | + ∶ ⊢ (∃ ⊢) * | + ∶ ∃x ⊢ ✄ ✂ ✁ ∶ ⊢ ) (⊢ ⊥) ⊢ . ∶ ⊥ | (⊥ ⊢) | ∶ ⊥ ⊢ (i) Logic ( * : x fv , ))
Figure 3. The L pol, calculus (top) and its typing rules in sequent calculus (bottom)

Properties

Proposition 2 (Con uence). The reduction → R is con uent.

Proof. Because the reduction R is left-linear and has no critical pairs (Nipkow [38]).

In Appendix A, we give a continuation-passing-style translation of L pol, into a calculus with surjective pairs. We show that the translation preserves equivalence and simulates reduction. Thus:

Proposition 3 (Coherence). If and are two distinct polarised variables, then

RE

.

In other words the calculus L pol, does not identify all proofs.

Proposition 4 (Strong normalisation). Typable commands of L pol, are strongly → R -normalising.

Of course the normalisation result is of limited interest given that our type system is inexpressive. Also, the orthogonality technique (adapted to the polarised case [START_REF]-calcul, machines et orthogonalité[END_REF][START_REF] Curien | Strong normalisation for focalising system L, Unpublished lectures notes for the Oregon Programming Languages Summer School[END_REF]) probably applies and gives more elegant proofs.

Call-by-name delimited continuations / Saurin's Λ

The calculus L pol, restricted to fully negative terms corresponds to Herbelin and "hilezan's n calculus [START_REF] Herbelin | hilezan, An Approach to Call-by-Name Delimited Continuations[END_REF]. Herbelin and "hilezan show that the calculus n is in correspondence with the Λ calculus of De "roote and Saurin [START_REF] De | roote, A CPS-Translation of the -Calculus[END_REF][START_REF] Saurin | Separation with Streams in the Λ -calculus[END_REF]. (The Λ calculus is interesting because Saurin showed that it satis es a Böhm theorem.) Shift 0 /Reset 0 We can show that the calculus implements (a variant of) the operators Shift 0 /Reset 0 [START_REF] Danvy | ilinski, Abstracting control, LISP and[END_REF][START_REF] Shan | A static simulation of dynamic delimited control[END_REF][START_REF] Materzok | A dynamic interpretation of the CPS hierarchy[END_REF]. (See M.-M. [33, Section IV.4.3].)

The involutive negation in natural deduction

In this section we introduce the ℓ calculus. The role of the ℓ calculus is to show how the calculus can be extended so as to correspond to a natural deduction with an involutive negation. This is why two constraints guided the design of the calculus:

1. Negation must be there as a connective;

2. There must be a clear distinction between quasi-proof terms and terms that appear during the evaluation in a machine.

Quasi-proof terms of the ℓ calculus are de ned in "igure 4 (top), together with a polarised predicate calculus in natural deduction. This calculus extends the calculus with a control operator ℓ that re nes the operator. Both terms and stacks have polarities determined by the function ; let us write + , ⊝ , + or ⊝ to refer to a term or a stack of a given polarity.

In "igure 4 (middle) we de ne the evaluation of terms with a machine that extends Krivine's. Initial stacks are in nitely many constants , … that have a xed polarity.

Constraints 1. and 2. above prevail at times over simplicity. "or instance, to ensure that we can statically determine a polarity for each term, application is annotated with the expected polarity of the result:

) + or ) ⊝
Note that an annotation is therefore a part of the grammar and de nes the term to be of polarity . By contrast, the notation only asserts that has this polarity and is not part of the grammar. We omit the annotation when it can be deduced from the context.

Negating a positive: polarised arrows

The negation of a positive formula is given with → ⊥. Let us rst explain the polarised arrow. The arrow is in call by value, by which we mean that in , the argument is evaluated rst, when it is not already a value:

✄ ✂ ✁ ⊝ + ‖ ≻ + ‖ + . ⊝ ‖ + ⋅ if + is not a value ⊝ ‖ ≻ ⊝ ‖ ⋅
In particular, contexts of the type → ⊥, when captured by control operators, are guaranteed to be stacks of the form ⋅ where is a value.

Remark 5. In this context, polarisation means that given three terms:

⊢ + ∶ , , + ∶ ⊢ ⊝ ∶ , , ⊝ ∶ ⊢ ∶
there are two ways of composing them:

⊝ . ) + . ⊝ + ) ⊝ and + . ⊝ . ) ⊝ ) + which correspond to the following distinct behaviours:

⊝ . ) + . ⊝ + ) ⊝ ‖ ≻ * [ + . ⊝ + ) ⊝ / ⊝ ]‖ + . ⊝ . ) ⊝ ) + ‖ ≻ * + ‖ + . ⊝ . ) ⊝ ‖
Thus, for lack of associativity of composition, the ℓ calculus escapes from the following argument of category theory, which historically opposed the existence of non-boolean categorical models of classical logic: as it is well-known, a cartesian-closed category never has a dualising object ⊥, that is to say satisfying the natural isomorphism ⊥ ⊥ , unless it is a boolean algebra. This follows more generally from the difficulty of interpreting negation in intuitionistic logic already: in a bi-cartesian-closed category, there is at most one morphism from any object to the initial object [26, p.67].

But, lack of associativity is only characteristic of polarisation, as we showed in M.-M. [START_REF]Models of a non-associative composition[END_REF].

Falsity: delimited control

We assume that execution happens in a machine of the following form:

✄ ✂ ✁ ‖ ‡ 1 ⊝ , … , ⊝ }
where = 1 ⊝ , … , ⊝ is a list of negative stacks. (As a consequence, the notation ≻ is an abbreviation which denotes ∀ , ‡ } ≻ ‡ }.)

The list interacts with control operators: we shall see that the operator lets it grow whereas the operator ℓ lets it shrink. Compared to the operator, the ℓ operator prefers to grab the nearest stack in the list to install it as the new context, instead of installing the stack from the calculus. We can think of as a list of exception handlers, with terms of type ⊥ being handled by raising an exception.

Inspectable stacks

The constants → , ∀5 and ⊥ let us access the components of an inspectable stack:

✄ ✂ ✁ → ∶ ∼ → ) → ⊗ ∼ ∀ ∶ ∼∀ ) → ∃ ∼ ⊥ ∶ ∼⊥ → → → ‖[ ⋅ 1 ]⋅ 2 ≻ , [ 1 ])‖ 2 ∀ ‖[ 1 ]⋅ 2 ≻ [ 1 ]‖ 2 ⊥ ‖[ ⊝ ]⋅ ⋅ ≻ ‖ ‡ ⊝ }
Also, a captured stack can be positive, which gives a value of the positive type ∼ . However it has no accessor. Example 6. We can combine ∀ and → to get a proof of: ¬∀x → ) → ∃x ⊗ ¬ ) Take = in the following:

∀→ ∶ ∼∀x → ) → ∃x ⊗ ∼ ) ∀→ ≝ + . + ∀ + → + ∀→ ‖[ ⋅]⋅ + ‡ } ≻ * , [])‖ + ‡ }
The immediateness of the operation is in sharp contrast with its homologue of the calculus given in the introduction. The essential di erence is that ∀→ accesses the components of a stack which is already captured, whereas the term of the calculus contains two control operators.

Example 7. We can combine → and ⊥ to obtain a proof in particular of ¬¬ → (take = ):

¬ ∶ ∼ → ⊥) → ¬ ≝ + . , + ) → + ⊥ + ) ¬ ‖[ ⋅ ⊝ ]⋅ ‡ } ≻ * ‖ ‡ ⊝ , }
The term ¬ keeps ⊝ at the head of the list . A variant erases ⊝ :

¬ ∶ ∼ → ⊥) → ¬ ≝ + . , + ) → + ¬ ‖[ ⋅ ⊝ ]⋅ ‡ } ≻ * ‖ ‡ }
But ¬ , and not ¬ , will take part in the isomorphism ¬¬ .

✄ ✂ ✁

… : Main additions to Figure 1.

⩴ + | ⊝ , ⩴ | . | ⊝ ) | ✄ ✂ ✁ + + | ✄ ✂ ✁ , ) | , ) + | | ℓ | → | ⊥ | ∀ ∶ term such that ) = ‡+, ⊝} (a) Quasi-proof terms ( is removed) ) … ) , ) . ,
, ℓ , → , ⊥ , ∀ ⊝ , ) + (b) Polarity ) ‡+, ⊝} of quasi-proof terms "ormulae: as in Figures 3d and3e.

✄ ✂ ✁ ∶ ⩴ + ∶ | ⊝ ∶ = ⃗ ∶ ⃗ ⊢ + ∶ , ⊢ ⊝ ∶ (c) Judgements (ax) , ∶ ⊢ ∶ ✄ ✂ ✁ ⊢ + ∶ , + ∶ ⊢ ∶ (let) ⊢ + + ∶ , ∶ ⊢ ∶ (→ ) ⊢ . ∶ → ⊢ ∶ → ⊢ ∶ (→ , = )) ⊢ ⊝ ) ∶ ✄ ✂ ✁ ⊢ ∶ ⊢ ∶ (⊗ ) ⊢ , ) ∶ ⊗ ✄ ✂ ✁ ⊢ + ∶ ⊗ , ∶ , ∶ ⊢ ∶ (⊗ ) ⊢ , ) + ∶ ⊢ ⊝ ∶ (∀ ) * ⊢ ⊝ ∶ ∀x ⊢ ⊝ ∶ ∀x (∀ ) ⊢ ⊝ ∶ [∈/x] ✄ ✂ ✁ ⊢ + ∶ [∈/x] (∃ ) ⊢ + ∶ ∃ ✄ ✂ ✁ ⊢ + ∶ ∃x , + ∶ ⊢ ∶ (∃ ) * ⊢ + + ∶ ✄ ✂ ✁ ℓ ∶ → ⊥) → ∼ , ∶ ∼ → → ⊥) , ⊥ ∶ ∼⊥ → → , → ∶ ∼ → ) → ⊗ ∼ , ∀ ∶ ∼∀ → ∃ ∼ * : x fv , ). (d) Rules ✄ ✂ ✁ ∀→ ≝ + . + ∀ + → + ∶ ∼∀x → ) → ∃x ⊗ ∼ ) ✄ ✂ ✁ ¬ ≝ + . , + ) → + ⊥ + ) ∶ ∼ → ⊥) → ≝ ⊝ . , + ) → ℓ_. ⊝ ∶ ⊥ → ✄ ✂ ✁ ≝ .ℓ ⊝ . ⊝ ) ⊝ ∶ → ∼ → ⊥) ✄ ✂ ✁ ≝ ⊝ . ¬ ℓ ⊝ . ⊝ ℓ ⊝ ) + )) ∶ ∼ → ⊥) → ≝ ⊝ . , + ) → ℓ ⊝ ) + ∶ → ⊥) → ⊥) → (e) Derived terms (notation ℓ . ⊝ ≝ ℓ . ⊝ ) + ) ⩴ … | ✄ ✂ ✁ [] | + ✄ ✂ ✁ , ⩴ ⊝ | + | , ) | [] ⩴ | ⋅ | ✄ ✂ ✁ + . | , ).
(f) Terms, values and stacks

⩴ ⊝ ‖ ⊝ | ✄ ✂ ✁ + ‖ + ⩴ ✄ ✂ ✁ ‡ } ⩴ ⋅ | ⊝ ,
(g) Commands and machines

) + ⊝ [] + )
⊝ , ⋅ ⊝ + , + . , , ). + (h) Polarity ), ) ‡+, ⊝} of terms and stacks

⊝ ) ‖ ‡ } ≻ { ⊝ ‖ ⋅ ‡ } if = ‖ + . ⊝ ‖ + ⋅ ‡ } otherwise . ‖ ⋅ ‡ } ≻ [ / ]‖ ‡ } ℓ‖ ⊝ ⋅ + ‡ ⊝ , } ≻ ⊝ ‖ + ⋅ ⊝ ‡ } + ‖ ‡ } ≻ + ‖ . ‖ ‡ } + ‖ ‡ } ≻ []‖ + ‡ } + ‖ + . ‡ } ≻ [ + / + ] ‡ } ‖[ ]⋅ ⋅ ⊝ ‡ } ≻ ‖ ‡ ⊝ , } + , )‖ ‡ } ≻ + ‖ + . + , )‖ ‡ } if + ≠ → ‖[ ⋅]⋅ + ‡ } ≻ , [])‖ + ‡ } , + )‖ ‡ } ≻ + ‖ + . , + )‖ ‡ } if + ≠ ⊥ ‖[ ⊝ ]⋅ ⋅ ‡ } ≻ ‖ ‡ ⊝ , } , )‖ , ). ‡ } ≻ [ / , / ] ‡ } ∀ ‖ ⋅ ‡ } ≻ ‖ ‡ } (i) Reductions ⊝ ) ≝ . ⊝ ‖ ⋅ ℓ ≝ ⊝ . + . ⊝ ‖ +⋅ + + ≝ . + ‖ + . ‖ → ≝ [ ⊝ ]. + . . . , [ ])‖ + ‖ ⊝ , ) + ≝ . + ‖ , ). ‖ ⊥ ≝ [ ⊝ ]. . . . ‖ ‖ ⊝ ≝ [ ]. . . ‖ ∀ ≝ [ ].[ ] where [ ]. ≝ . . ‖ [ ]. ‖ (j) Solving quasi-proof terms + ≝ . [ ]‖ + ‡} ≝ ≝ (free) ‡ 1 ⊝ , … , ⊝ } ≝ . ‖ 1 ⊝ ‡ 2 ⊝ , … , ⊝ } (

Capturing and installing stacks

"iven a captured stack [], the stack is re-installed as the context of another term by the constant :

‖[]⋅ ⋅ ⊝ ‡ } ≻ ‖ ‡ ⊝ , }
In other words, the constant converts a captured stack into a continuation :

✄ ✂ ✁ ∶ ∼ → → ⊥
The stack ⊝ , supposedly of type ⊥ according to the type of , is added on top of .

The operator responsible for the apparition of inspectable stacks is ℓ :

✄ ✂ ✁ ℓ ∶ → ⊥) → ∼
The notation ℓ . ⊝ stands for ℓ . ⊝ ) + . It evaluates ⊝ until comes in head position, that is to say in front of a stack . When this happens, the operator ℓ captures and supplies the inspectable stack [] to the context where ℓ was applied. Last, the operator ℓ falls back to the head of the list in case ⊝ returns without using . 6This operation is formally described by introducing the operator. The operator ℓ saves in the context + in which ℓ is applied, and installs the head ⊝ as the new context:

ℓ‖ ⊝ ⋅ + ‡ ⊝ , } ≻ ⊝ ‖ + ⋅ ⊝ ‡ }
Once the operator + comes in head position, it captures the stack and restores the context + :

+ ‖ ‡ } ≻ []‖ + ‡ } Example 8.
Using ℓ, we derive an operator (abort) which interprets the rule Ex Falso Quodlibet:

∶ ⊥ → ≝ ⊝ . , + ) → ℓ_. ⊝ ‖ ⊝ ⋅ ‡ ⊝ , } ≻ * ⊝ ‖ ⊝ ‡ } Example 9. By combining . ∶ → → ⊥) → ⊥) with ℓ
we obtain a proof of → ¬¬ (take = ):

∶ → ∼ → ⊥) ≝ .ℓ ⊝ . ⊝ ) ⊝ ‖ ⋅ + ‡ ⊝ , } ≻ * [ ⋅ ⊝ ]‖ + ‡ }
Example 10. We obtain the elimination of double negation ¬¬ → as follows (take = ):

∶ ∼ → ⊥) → ≝ ⊝ . ¬ ℓ ⊝ . ⊝ ℓ ⊝ ) + )) ‖ ⊝ ⋅ ‡ ⊝ , ⊝ , } ≻ * ⊝ ‖[]⋅ ⊝ ‡ ⊝ , }
The operator is a variant of the operator that supplies the context under the form of an inspectable stack, rather than a continuation.

Translating ℓ in L pol,

Like for the calculus, we can de ne the operations of the calculus in the calculus L pol, by solving the reduction rules as explained in Section 2.2. In addition to the de nitions in "igure 4 (bottom), stack constants of the ℓ calculus are interpreted by free co-variables of L pol, . 7 These de nitions induce a translation of ℓ into L pol, , which is de ned by induction. We identify elements of ℓ to their image in L pol, .

Remark 11. Like the quasi-proofs of (with respect to ), quasi-proofs of ℓ form a compositional sub-language of terms of L pol, that have no free co-variable.

We easily show:

ℓ ⊝ . + . ⊝ + + . + ))))
In other words we can obtain ℓ from . Interestingly, however, we could not derive the type ℓ ∶ → ⊥) → ∼ from the one of .

Thus we have to take ℓ (positive negation introduction) as a primitive rather than (double negation elimination). "inally, following from Proposition 3 we have:

Proposition 16 (Coherence). If and are two distinct polarised variables, then .

Negation is involutive in ℓ and L pol,

In terms of the equivalences RE on L pol, and on ℓ, we can prove that there are isomorphisms of type ¬¬ for both positive and negative. Due to lack of associativity of composition when and do not have the same polarity, we ask that is de ned only when they have the same polarity. Definition 17. Two types (or formulae) and are isomorphic if they have the same polarity and there exist two terms:

∶ ⊢ ) ∶ and ∶ ⊢ ) ∶ with: ) ) and
) )

In this case we write , . In the calculus L pol, , we take = RE above. In the ℓ calculus, we take = . In the latter case, notice that terms must be quasiproofs since only quasi-proofs are derivable in natural deduction.

Proposition 18 (

¬¬ ). One takes, referring to the terms from Examples 7 and 9 (also de ned in Figure 4e):

+ + ) ≝ + ) + + + ) ≝ ¬ + ) +
In L pol, and ℓ, one has + , + ∼ → ⊥). Proposition 19 ( ¬¬ ). We de ne, referring to the term from Example 10 (also de ned in Figure 4e):

⊝ ⊝ ) ≝ + . + ⊝ ) ⊝ ⊝ ⊝ ) ≝ ⊝ ) ⊝
In L pol, and ℓ, one has ⊝ , ⊝ ∼ → ⊥. The proofs are detailed in Appendix B.

Conclusion

The calculi L pol, and ℓ are shaped by a special constraint, that of having two readings: as proof systems and as programming languages. But we do not believe that they should be regarded as mere proof of concept, because the various ideas that they synchretise can be taken separately. "or instance, it should be possible to restrict the calculi L pol, and ℓ into direct-style languages for the more general Call-by-Push-Value models [START_REF] Blain | Adjunction models for call-by-push-value with stacks[END_REF].

Also, relaxing an equality ¬¬ = into an isomorphism as we do appears to be closely related to Melliès's dialogue chiralities [START_REF] Melliès | Dialogue categories and chiralities[END_REF]. But, if the simpler-to-manage strict involution is desired in a proof theoretic context, then it is certainly possible to recover a notion of quasi-proofs from the one we presented. Notably, it remains to see how much classical realisability results can be made simpler by using a setting where polarities are rst-class. But to my surprise, the distinction between continuations and inspectable contexts seems to also have some importance in the formulae-as-types interpretation of "ödel's Dialectica translation from the same proceedings (Pédrot [START_REF] Pédrot | A functional functional interpretation[END_REF], private communication).

The making of this article is the story of how to avoid useless complexity in the calculi and systems we introduce, which are already quite complex. It seems essential for this to use an L calculus as an intermediate language in which program constructs are de ned abstractly by their transition rules. Thus, "entzen's discovery that sequent calculus is easier to reason about than natural deduction [START_REF]erhard "entzen, Untersuchungen über das logische Schließen[END_REF] re ects in term calculi.

"inally, high-level access to the stacks is an interesting and natural feature of delimited control operators, but it does not seem to be very developed in the programming languages literature.

B Proof of the involution 13

A. Coherence

We de ne a CPS translation for the calculus L pol, that simulates the reduction and preserves equivalences. We deduce that RE and do not identify all the terms.

A.1 The target of the CPS translation

The target of the CPS translation is the call-by-name calculus with pairs considered by Herbelin and "hilezan [START_REF] Herbelin | hilezan, An Approach to Call-by-Name Delimited Continuations[END_REF].

✄ ✂ ✁ , ⩴ | . | | , ) | | , )
The calculus comes with the following reductions and expansions:

. ) R [ / ] R [ / ] , ) , ) R [ / , / ] [ , ) ] R , ) [ ] where [ ] ⩴ [ ] | [ ] | , ) [ ] E . E , ) , )
This calculus does not identify all terms.

Proposition 20. We have RE for any pair of distinct variables and .

Proof. We consider the more standard calculus with surjective pairs which is the calculus extended with pairs , ), projections

) and ) and rules:

, ) SP , ) SP SP ),
))

It is easy to see that the following de nition:

, ) ≝ . . . ) ) ))
induces a translation from Herbelin-"hilezan's calculus with pairs into the calculus with surjective pairing that preserves equivalences. We conclude RE , since we have SP (see for instance Støvring [START_REF] Støvring | Extending the extensional lambda calculus with surjective pairing is conservative[END_REF]).

A.2 One-pass CPS translation

We de ne in "igure 5 the CPS translation of the calculus L pol, into Herbelin-"hilezan's calculus with pairs. We assume that + , ⊝ , + , ⊝ , … (including co-variables) represent distinct subsets of variables of the calculus with pairs.

A value or a stack is translated into a -term. A negative term or a positive context is translated into a linear function from -terms into -terms (notation , ). By linear we mean the naive (syntactic) notion based on counting occurrences, which simply ensures that the translation hides no duplication or erasure of source terms.

Then, a positive term or a negative context is translated into a linear functional from the previous functions , into -terms. Then the command is translated into the application of the linear functional to the linear function. Thus, the continuation corresponding to a positive term is immediately applied, whereas the one for the negative term is passed.

c s + ‖ + ≝ c s + + c s ⊝ + ) c s ⊝ ‖ ⊝ ≝ c s + ⊝ c s ⊝ ⊝ )
This formulation with functionals is a reformulation of one-pass CPS transforms as introduced by Danvy and "ilinski [START_REF]Representing control: A study of the cps transformation[END_REF].

Lemma 21. Let , ) be a pair of a value and a variable or of a stack and a co-variable, with and of the same polarity. We write = val V or = val π depending on the case. For any command , any term or context , any context , any value , any stack , and any -term , one has:

c s [ / ] → * R c s [ / ] c s + )[ / ] → * R c s + [ / ] ) where ∶ ↦ )[ / ] c s ⊝ )[ / ] → * R c s ⊝ [ / ] [ / ]) val V [ / ] → * R val V [ / ] val π [ / ] → * R val π [ / ]
Proof. By induction on the de nition of the translation.

Case val V + . If + ≠ one has val V + [ / ] = + [ / ]; otherwise one has:

val V + [ / + ] = + [ / + ] =
One concludes with = + [ / + ] using the hypothesis that and + have the same polarity. Case val π ⊝ . Same reasoning. Case c s ⊝ ⊝ ). By hypothesis, is a term of the same polarity as ⊝ . Thus we have:

= val V = .c s ⊝ ) Hence: c s ⊝ ⊝ )[ / ⊝ ] = .c s ⊝ )) [ / ⊝ ] R c s ⊝ [ / ⊝ ])
Case c s ⊝ + ). Same reasoning. The remaining cases are easily deduced from induction hypothesis.

c s ⊝ . ⊝ ‖ ) R c s ⊝ ⊝ ) c s + ‖ + ≝ c s + + c s ⊝ + ) c s ⊝ ‖ ⊝ ≝ c s + ⊝ c s ⊝ ⊝ ) (a) c s ⋅ ∶ → c s ⊝ ⊝ ) ≝ ⊝ c s ⊝ + ) ≝ + c s ⊝ ⊝ . ) ≝ ⊝ c s c s ⊝ + . ) ≝ + c s c s ⊝ . ) ≝ , ) c s ⊝ ) c s ⊝ , ). ) ≝ , ) c s c s ⊝ . ) ≝ c s c s ⊝ [ ]. ) ≝ c s c s ⊝ + ) ≝ c s + + ) where ∶ ↦ c s ⊝ ⊝ ) ≝ c s + ⊝ ) where ∶ ↦ (b) c s ⊝ ⋅ ∶ ∪ → → c s + + ) ≝ val V + ) c s + + . ) ≝ + . ) c s c s + + , ) ) ≝ c s + + ) where ∶ ↦ + c s + + , ) ) c s + , + ) ) ≝ c s + + ) where ∶ ↦ + c s + , + ) ) c s + [ ⊝ ] ) ≝ c s + ⊝ ) where ∶ ↦ ⊝ c s + [ ⊝ ] ) c s + ⊝ ) ≝ val π ⊝ ) c s + ⊝ . ) ≝ ⊝ . ) c s c s + + ⋅ ) ≝ c s + + ) where ∶ ↦ + c s + + ⋅ ) c s + ⋅ ⊝ ) ≝ c s + ⊝ ) where ∶ ↦ ⊝ c s + ⋅ ⊝ ) c s + ) ≝ . ) If + is not a value. If ⊝ is not a stack. (c) c s + ⋅ ∶ + ∪ ⊝ → → ) → val V + ≝ + val V , ) ≝ val V , val V ) val V [] ≝ val π val V ⊝ ≝ .c s ⊝ ⊝ ) (d) val V ⋅ ∶ → val π ⊝ ≝ ⊝ val π ⋅ ≝ val V , val π ) val π + ≝ .c s ⊝ + ) (e
c s ‖ . = val V c s R c s [val V / ] → * R c s [ / ] Case . ‖ R [/ ] and []‖ [ ]. R [/ ]. Same reasoning. Case . ‖ ⋅ R [ / ]
‖ with of the same polarity as and of the same polarity as . One has:

c s . ‖ ⋅ = , ) val V , val π ) c s ⊝ ) R c s ⊝ )[val V / , val π / ] → * R c s ⊝ [ / ] )[val π / ] = c s ⊝ [ / ] val π )
We conclude depending on the polarity of [ / ]:

c s ⊝ ⊝ val π ) = c s ⊝ ‖ c s ⊝ + val π ) = c s + + ↦ .c s ⊝ ) ) → R c s + + c s ⊝ )) = c s + ‖ Case , )‖ , ). R [ / , / ]
c s ⊝ . ⊝ ‖ ) = .c s ⊝ ⊝ )) R c s ⊝ ⊝ ) 3. Case ⊝ E ⊝ . ⊝ ‖ ⊝ . One has: c s ⊝ ⊝ . ⊝ ‖ ⊝ ) = ⊝ c s ⊝ ⊝ ⊝ ) R c s ⊝ ⊝ ) Case + E + . + ‖ + and ⊝ E [ ⊝ ]. [ ⊝ ] ‖ + . Same reasoning.
Case ⊝ E . . ⊝ ‖ ⋅ . One has depending on the polarity of :

c s ⊝ . ⊝ . ⊝ ‖ ⋅ ⊝ ) = , ) ⊝ c s ⊝ ⊝ , . ⊝ ))) c s ⊝ . + . ⊝ ‖ ⋅ + ) = , ) + . ) c s ⊝ ⊝ , + ))
In both cases:

c s ⊝ . . ⊝ ‖ ⋅ ) R , ) , . )) c s ⊝ ⊝ ) ← E , ) , ) c s ⊝ ⊝ ) R , ) , )) c s ⊝ ⊝ ) ← E c s ⊝ ⊝ ) R c s ⊝ ⊝ ) Case ⊝ E , ) .
. + ‖ + ) = + . ) c s + + ↦ + ) R c s + + ↦ . ) ) → R c s + + ) Case ⊝ E ⊝ . ⊝ ‖ ⊝ . Same reasoning.
5. We have indeed: c s . ‖ = .c s E c s Theorem 23 (Simulation). Let and be two commands of the calculus L pol, .

1. If → R then c s → + R c s . 2. If RE then c s RE c s .
Proof. By immediate induction on the de nitions of → R and RE , using Lemma 22.

A fortiori, the translation simulates the reduction of machines of ℓ. We deduce the coherence of calculi ℓ and L pol, :

Corollary 24 (Coherence). If and are two distinct polarised variables, then RE , and therefore also .

Proof. Let and be two distinct variables of the calculus L pol, that we can assume to be of the same polarity. In order to show

B. Proof of the involution

We have de ned negation depending on the polarity:

¬ = { ∼ if = → ⊥ if =
We refer the reader to M.-M. [33, Section IV.5] for further explanations of this de nition in terms of focusing, for an explanation of why it is necessary to delimit control in order to model ⊥, and also for a motivation of our de nition of isomorphisms (De nition 17). We now prove that there exists an isomorphism between and ¬¬ for either positive or negative, rst in L pol, and then in ℓ.

We insist that the proofs are entirely algebraic. In particular, we need no hypothesis about the syntax being non-extensible or a particular typed setting being strongly normalising. As a consequence, the isomorphism remains true in all extensions of the calculi and of their type systems. (A counter-example to this property is an isomorphism such as ∀ → ) → in System ".) In L pol, , one has + , + ∼ → ⊥).

B
Proof. Indeed one has:

+ ∶ ⊢ [ + ⋅ ] ∶ ∼ → ⊥) + ∶ ∼ → ⊥) ⊢ + . + ‖ [ + ⋅ ]. + ‖ + ∶
Besides, one has: Proposition 30 ( ¬¬ in L pol, ). Let us take:

+ + + ) + + )‖ +
⊝ ⊝ ) ≝ [ ⊝ ]. . ⊝ ‖ ⊝ ⊝ ⊝ ) ≝ ⊝ . ⊝ ‖[ ⊝ ]⋅
In the calculus L pol, , one has:

⊝ , ⊝ ∼ ) → ⊥
Proof. Indeed one has:

⊝ ∶ ⊢ [ ⊝ ]. . ⊝ ‖ ⊝ ∶ ∼ ) → ⊥ ⊝ ∶ ∼ ) → ⊥ ⊢ ⊝ . ⊝ ‖[ ⊝ ]⋅
One also has: Proof. If ) and ) are quasi-proof terms, then it is also the case of

⊝ ⊝ ⊝ ) ⊝ ⊝ )‖ ⊝ R [ ⊝ ]. . ⊝ ‖ ⊝ ‖ ⊝ . ⊝ . ⊝ ‖[ ⊝ ]⋅ ‖ ⊝ → * R [ ⊝ ]. . ⊝ ‖ ⊝ ‖ [ ⊝ ]⋅ RE ⊝ ‖ ⊝ ⊝ ⊝ ⊝ ) ⊝ ⊝ )‖ ⊝
) ) and of ) ). Therefore by hypothesis and de nition one has:

) )

) )

Corollary 32 (

¬¬ in ℓ). One takes:

+ + ) ≝ + ) + + + ) ≝ ¬ + ) +
In ℓ, one has + , + ∼ → ⊥).

Proof. As we proved in Section 3:

+ ∶ ⊢ + ) + ∶ ∼ → ⊥) + ∶ ∼ → ⊥) ⊢ ¬ + ) + ∶
We also proved in particular:

+ ) + ‖ + [ ⊝ ] ≻ * [ + ⋅ ⊝ ]‖ + ¬ [ + ⋅ ⊝ ]) + ‖ + ≻ * + ‖ + [ ⊝ ]
According to Proposition 12, these reductions are equivalences between commands of L pol, . As a consequence one has by extensionality in L pol, :

+ ) + RE [ + ⋅ ] = + + ) ¬ + ) + RE + . + ‖ [ + ⋅ ]. + ‖ + = + )
According to Proposition 27, one therefore has + , + ∼ → ⊥) in L pol, . Since both + and + are quasi-proof terms, we have according to Proposition 31 + , + ∼ → ⊥) in ℓ.

Corollary 33 ( ¬¬ in ℓ). We de ne:

⊝ ⊝ ) ≝ + . + ⊝ ) ⊝ ⊝ ⊝ ) ≝ ⊝ ) ⊝
In ℓ, one has ⊝ , ⊝ ∼ → ⊥.

Proof. We proved in Section 3:

⊝ ∶ ⊢ + . + ⊝ ) ⊝ ∶ ∼ → ⊥ ⊝ ∶ ∼ → ⊥ ⊢ ⊝ ) ⊝ ∶
Besides, one has:

+ . + ⊝ ) ⊝ ‖[ ⊝ ]⋅ ⊝ ≻ * ⊝ ‖ ⊝ [ ⊝ ] ⊝ ) ⊝ ‖ ⊝ [ ⊝ , ⊝ ] ≻ * ⊝ ‖[ ⊝ ]⋅ ⊝ [ ⊝ ]
According to Proposition 12, these reductions are equivalences of commands of L pol, . As a consequence one again has by extensionality in L pol, :

+ . + ⊝ ) ⊝ RE [ ⊝ ]. . ⊝ ‖ ⊝ = ⊝ ⊝ ) ⊝ ) ⊝ RE ⊝ . ⊝ ‖[ ⊝ ]⋅ = ⊝ ⊝ )
According to Proposition 30, one therefore has ⊝ , ⊝ ∼ → ⊥ in L pol, . Again, since ⊝ and ⊝ are quasi-proof terms, one has according to Proposition 31 ⊝ , ⊝ ∼ → ⊥ in ℓ.

  (b) "irst-order predicate calculus ( * : x not free in )

Figure 1 .

 1 Figure 1. The calculus and its call-by-name abstract machine purely positive, thendoes not depend on and, furthermore, we have = . Therefore, in this special case we can take = and deduce an intuitionistic proof of ⊢ → ) → and, in turn, one of ⊢ . In the other cases, the translation describes in fact how the behaviour of classical proofs depends on the context in which classical axioms are invoked. Thus the interpretation does not contradict intuitionism: the latter assumes that the behaviour of proofs is referentially transparent, while here we do not make such an assumption. This is why proofs of ∀ , ¬ do not provide a decision procedure for in general.In this article, we are interested in the constructive interpretation of reasoning by contrapositive, or, in other words, of an involutive negation. In terms of double-negation translations, we must consider two techniques:

Figure 2 .

 2 Figure 2. The calculus (top) and its typing rules in sequent calculus (bottom)

  k) Solving terms, stack constants and machines

Figure 4 .

 4 Figure 4. The ℓ calculus and its typing rules (top) Its abstract machine (middle) De nition of its constructs in L pol, (bottom)

Proposition 12 (Proposition 13 .Definition 15 .

 121315 Simulation). If ≻ for two machines and of the calculus ℓ, then → + R in the calculus L pol, . If one has ⊢ ∶ in natural deduction, then one has ⊢ ∶ | in sequent calculus. Consequently: Proposition 14 (Normalisation). If is a typable term of ℓ, then the machine ‖ 0 ‡ ⊝ 1 , … , ⊝ } normalises (because it is a typable command of L pol, ). In ℓ, we de ne the compatible equivalence relation between quasi-proof terms with: def ⟺ RE "or instance, one can show:

Lemma 22 . 1 .

 221 "or any , such that R , one has:c s → + R c s 2. "or any ⊝ , one has:

Figure 5 .

 5 Figure 5. One-pass CPS translation of L pol,

RE,

  it is sufficient by the rule E to show for some of the proper polarity: ‖ RE ‖ . Let such an a . If ‡ , } is positive then one has c s ‖ = ; otherwise one has c s ‖ = . Yet according to Proposition 20, one has RE . Thus we also have c s ‖ RE c s ‖ ; and therefore ‖ RE ‖ using Theorem 23.

. 1 ≅Definition 25 .Lemma 26 . 27 (

 1252627 ¬¬ in L pol, B.1.1 Case ¬¬ ≅ We de ne the following notation: [ ⋅ ]. ≝ [ ⊝ ]. . . ‖ ⊝ This construct has the following introduction rule:∶ , ∶ ⊢ ) | [ ⋅ ]. ∶ ∼ → ⊥) ⊢ One has: [ ⋅ ]‖ [ ⋅ ]. RE [ / ] [ ⋅ ]. [ ⋅ ]‖ + RE +Proof. One has: ¬¬ in L pol, ). We de ne:+ + ) ≝ [ + ⋅ ] + + ) ≝ + . + ‖ [ + ⋅ ]. + ‖ +

Definition 28 .Lemma 29 .

 2829 We de ne the following notation:[ ⊝ ]. ≝ + . . + ‖ [ ⊝ ]. ‖This construction has the following derived rule:⊢ ∶ | ⊝ ∶ , ⊢ [ ⊝ ]. ∶ ∼ ) → One has: [ ⊝ ]. . ‖[ ⊝ ]⋅ RE [ ⊝ / ⊝ ] [ ⊝ ]. . + ‖[ ⊝ ]⋅

B. 2 ≅ ¬¬ in ℓ Proposition 31 .

 231 If we have, in the calculus L pol, , such that and are given by quasi-proof terms of ℓ, then one has , in the calculus ℓ.

Table 1 .

 1 A summary of the calculi presented in this article operators (Murthy

	1

  with of the same polarity as and of the same polarity as . Same reasoning.

	Case → 1 ) ∶ + not a value. By de nition, one has c s ⊝ ‖ + ⋅ R + ‖ . ⊝ ‖ ⋅ ⊝ ‖ + ⋅ c s + + ) where ∶ ↦ + c s ⊝ ‖ ⋅ Therefore one has = c s ⊝ and furthermore with = . . ⊝ ‖ + ⋅ c s ⊝ ‖ + ⋅ = c s + ‖ . ⊝ ‖ ⋅ . Other cases ). Same reasoning. 2. One has:

  , )‖ ⊝ . Same reasoning.

	Case + E reasoning as (4.) below. + . + ‖ + and ⊝ E 4. Case + E + . + ‖ + . One has:	⊝ . ⊝ ‖ ⊝ . Same
	c s +	+

See M.-M. [33, Section I.10.3] for a discussion.

We could also circumvent the issue of the connective ⊥ by replacing the de nition ¬ ≝ → ⊥ by an ad hoc dual to the connective ∼, but: 1) that would leave open the question of its interaction with implication, and 2) it is not clear that such a connective has a convincing formula-as-type interpretation.

ANR-07-BLAN-0324 Choco, ANR-12-JS02-006-01 Co uas, ANR-10-BLAN-0213 Logoi and ANR-11-BS02-0010 Rec e

The rules in additive style from "igure 1 can be recovered if and are allowed to overlap. We prefer the multiplicative style, because conversely in additive-style LK, →-elimination is not derivable but only admissible.

The behaviour of ∀ seems trivial because it corresponds to a sub-typing relation ∼∀ ) <∶ ∃ ∼ . Thus the examples that follow would be even simpler if we took the trouble of introducing a notion of sub-typing.

This explains why Murthy's computational interpretation of LC must evaluate under the -abstraction[START_REF]A Computational Analysis of Girard's Translation and LC[END_REF]. Murthy was in fact describing the behaviour of a ℓ-like operator, rather than a -

abstracttion.[START_REF] Curien | The duality of computation[END_REF] Interpreting such stack constants as open variables goes back to Hofmann and Streicher[START_REF] Hofmann | Completeness of continuation models for -calculus[END_REF].

Appendix