A fine-grained computational interpretation of Girard’s intuitionistic proof-nets

This paper introduces a functional term calculus, called pn, that captures the essence of the operational semantics of Intuitionistic Linear Logic Proof-Nets with a faithful degree of granularity, both statically and dynamically. On the static side, we identify an equivalence relation on pn-terms which is sound and complete with respect to the classical notion of structural equivalence for proof-nets. On the dynamic side, we show that every single (exponential) step in the term calculus translates to a different single (exponential) step in the graphical formalism, thus capturing the original Girard’s granularity of proof-nets but on the level of terms. We also show some fundamental properties of the calculus such as confluence, strong normalization, preservation of β-strong normalization and the existence of a strong bisimulation that captures pairs of pn-terms having the same graph reduction.

Decomposing Probabilistic Lambda-Calculi

A notion of probabilistic lambda-calculus usually comes with a prescribed reduction strategy, typically call-by-name or call-by-value, as the calculus is non-confluent and these strategies yield different results. This is a break with one of the main advantages of lambda-calculus: confluence, which means results are independent from the choice of strategy. We present a probabilistic lambda-calculus where the probabilistic operator is decomposed into two syntactic constructs: a generator, which represents a probabilistic event; and a consumer, which acts on the term depending on a given event. The resulting calculus, the Probabilistic Event Lambda-Calculus, is confluent, and interprets the call-by-name and call-by-value strategies through different interpretations of the probabilistic operator into our generator and consumer constructs. We present two notions of reduction, one via fine-grained local rewrite steps, and one by generation and consumption of probabilistic events. Simple types for the calculus are essentially standard, and they convey strong normalization. We demonstrate how we can encode call-by-name and call-by-value probabilistic evaluation.

About an analogue of Neifeld’s connection on the space of centred planes with one-index basic-fibre forms

This research is realized by Cartan — Laptev method (with prolongations and scopes, moving frame and exterior forms). In this paper we consider a space П of centered m-planes (a space of all centered planes of the dimension m). This space is considered in the projective space n P . For the space П we have: dim П=n + (n – m)m. Principal fiber bundle is arised above it. The Lie group is a typical fiber of the principal fiber. This group acts in the tangent space to the П. Analogue of Neifeld’s connection with multivariate glueing is given in this fibering by Laptev — Lumiste way. The case when one-index forms are basic-fibre forms is considered. We realize an analogue of the Norden strong normalization of the space П by fields of the geometrical images: (n – m – 1)-plane which is not having the common points with a centered m-plane and (m – 1)-plane which is belonging to the m-plane and not passing through its centre. It is proved that the analog of the Norden strong normalization of the space of centered planes induces this connection.

A resource aware semantics for a focused intuitionistic calculus

We investigate a new computational interpretation for an intuitionistic focused sequent calculus which is compatible with a resource aware semantics. For that, we associate to Herbelin's syntax a type system based on non-idempotent intersection types, together with a set of reduction rules – inspired from thesubstitution at a distanceparadigm – that preserves (and decreases the size of) typing derivations. The non-idempotent approach allows us to use very simple combinatorial arguments, only based on this measure decreasingness, to characterizelinear-headandstronglynormalizing terms by means of typability. For the sake of completeness, we also study typability (and the corresponding strong normalization characterization) in the calculus obtained from the former one by projecting the explicit cuts.

Jump from parallel to sequential proofs: exponentials

In previous works, by importing ideas from game semantics (notably Faggian–Maurel–Curien'sludics nets), we defined a new class of multiplicative/additive polarized proof nets, calledJ-proof nets. The distinctive feature of J-proof nets with respect to other proof net syntaxes, is the possibility of representing proof nets which are partially sequentialized, by usingjumps(that is, untyped extra edges) as sequentiality constraints. Starting from this result, in the present work, we extend J-proof nets to the multiplicative/exponential fragment, in order to take into account structural rules: More precisely, we replace the familiar linear logic notion of exponential box with a less restricting one (calledcone) defined by means of jumps. As a consequence, we get a syntax for polarized nets where, instead of a structure of boxes nested one into the other, we have one of cones which can bepartially overlapping. Moreover, we define cut-elimination for exponential J-proof nets, proving, by a variant of Gandy's method, that even in case of ‘superposed’ cones, reduction enjoys confluence and strong normalization.