Aurore Alcolei (INRIA Rennes)
The exponential logic of sequentialization
Linear logic enjoys two ways of representing proofs: a classical sequent calculus and a graphical representation of them called proof nets. The purely graphical approach of proof-nets deprives them of any sequential structure that informes on the order in which arguments are presented. Rebuilding this order of presentation — sequentializing the graph — is thus a requirement for a graph to be logical. Jumps, extensively studied by Faggian and di Giamberardino, are graphical artifacts on nets that can express intermediate degrees of sequentialization between a sequent calculus proof and a fully desequentialized proof-net. In this talk, we propose to analyze the logical strength of jumps by internalizing them in an extention of MLL where axioms on a specific formula, the jumping formula, introduce constrains on the possible sequentializations. The jumping formula needs to be treated non-linearly, which we do either axiomatically, or by embedding it in a very controlled fragment of multiplicative-exponential linear logic, uncovering the exponential logic of sequentialization.
Victor Arrial (IRIF, Université Paris Cité)
The Benefits of Diligence
Both (distant) Call-by-Name (dCBN) and (distant) Call-by-Value (dCBV) can be embedded into a unifying framework called the (distant) Bang Calculus (dBANG). These embeddings allow us to establish (static and dynamic) properties of dCBN and dCBV through their respective counterparts in dBANG. While some specific static properties have been already successfully studied in the literature, the dynamic ones are more challenging and have been left unexplored. We accomplish that by using a standard embedding for the (easy) dCBN case, while a novel one must be introduced for the (difficult) case of dCBV. Moreover, a key point of our methodology is the identification of dBANG diligent reduction sequences, which eases the preservation of dynamic properties from dBANG to dCBV. We illustrate our methodology through a concrete application: factorizations for both dCBN and dCBV are derived from factorization in dBANG.
Esaïe Bauer (IRIF, Université Paris Cité)
Cut-elimination for modal mu-calculus: exploring the expressivity of muMALL
The exploration of logic with fix-points commenced with modal calculi. Various approaches was established to design proof systems for such logics. One of them involves permitting proofs to manifest as infinite trees, coinductively generated by the finitary system's rule and four additional rules (or two for the one-sided sequent version), addressing the least and greatest fix-points.
Conversely, investigations into logics featuring fix-points and infinitary proofs have delved into Linear Logic. By incorporating fix-point rules into the finitary system of Multiplicative-Additive Linear Logic, the resulting system, muMALL, adeptly eliminates cuts. Recent research by Saurin demonstrates that muMALL can express the entirety of Linear Logic with fix-points (muLL), along with proof systems for fix-point versions of LK or LJ, such as muLK or muLJ.
In our ongoing work, we leverage a translation from modal mu-calculus into muLL. Additionally, by applying the cut-elimination theorem of muLL, we aim to establish a constructive version of cut-elimination for the modal mu-calculus.
This work, still in progress, is a joint work with Alexis Saurin.
Baptiste Chanus (LIPN, Université Sorbonne Paris-Nord)
Characterizing complexity classes in categorical descriptive complexity
Fagin's theorem states that the class NP may be characterized as the class of problems which may be expressed in existential second order logic. It started the field of descriptive complexity, the development of which has shown a deep link between logic and complexity. In an attempt to understand this link from the categorical viewpoint, Damiano Mazza introduced an approach, based on Boolean lextensive categories and categorical logic, in which several standard complexity classes (recursivably enumerable languages, P, NP…) may be characterized in a natural way. In this talk, we will carry this approach further, showing how to characterize several more standard complexity classes: the polynomial hierarchy, PSPACE, the logarithmic time hierarchy and NL.
Rémi Di Guardia (LIP, ENS Lyon)
Rétractions en Logique Linéaire Multiplicative
Je vais parler de rétraction en logique. Pour des formules A et B, A est une rétraction de B s'il existe des preuves de A |- B et B |- A dont la composition par coupure sur B est égale à l'axiome sur A, à élimination des coupures et expansion des axiomes près. Cela correspond aux rétractions dans la catégorie des preuves : les objets sont des formules, les morphismes des preuves (considérées à élimination des coupures et expansion des axiomes près), la composition est la coupure et les identités les axiomes. Alors que les isomorphismes de MLL sont connus (Balat et Di Cosmo ont donné une théorie équationnelle correspondante), et qu'il y a une rétraction (qui n'est pas un isomorphisme) de bien connue, il n'y a même pas d'hypothèse sur ce que pourraient être l'ensemble des rétractions. Je vais présenter un travail en cours sur les rétractions de la forme “un atome X est une rétraction de B”, et quelles sont les difficultés pour étendre ce résultat au cas de formules quelconques.
Aloÿs Dufour (LIPN, Université Sorbonne Paris-Nord)
An Axiomatic Approach to Approximations in Programming Languages
The idea that programs may be approximated by “simple programs” (withoutconditionals and loops) appears in both the theory of computation and of programming languages, with examples ranging from the Cook-Levin theorem tothe Taylor expansion of lambda-terms. We present an axiomatic definition of“approximation system”, based on a notion of fibration, which is intended tocapture this phenomenon as generally as possible. In this talk, we willexplore the immediate consequences of the definition, introduce severalconcrete instances of it, and obtain well-known theorems as directapplications of the general framework.
Thiago Felicissimo (Deducteam, INRIA Paris Saclay)
-
Bidirectional typing is a discipline in which the typing judgment is decomposed explicitly into inference and checking modes, allowing to control the flow of type information in typing rules and to specify algorithmically how they should be used. Bidirectional typing has been fruitfully studied and bidirectional systems have been developed for many type theories. However, the formal development of bidirectional typing has until now been kept confined to specific theories, with general guidelines remaining informal. We contribute with a generic account of bidirectional typing for a general class of dependent type theories. This is done by first giving a general definition of type theories (or equivalently, a logical framework), for which we define declarative and bidirectional type systems. We then show, in a theory-independent fashion, that the two systems are equivalent. This equivalence is then explored to establish the decidability of typing for weak normalizing theories, yielding a generic type-checking algorithm that has been implemented in a prototype and used in practice with many theories.
Leandro Gomes (CRIStAL, Université de Lille)
An algebraic approach for union bound reasoning on probabilistic programs
Kleene Algebra with Tests (KAT) provides a framework for algebraic equational reasoning on imperative programs. The recent variant Guarded KAT (GKAT) allows to reason on non-probabilistic properties of probabilistic programs. Here we introduce an extension of this framework called aGKAT (approximate GKAT), a form of graded GKAT over a partially ordered monoid (real numbers) which enables to express satisfaction of (deterministic) properties except with a probability up to a certain bound. This allows to represent in equational reasoning ’à la KAT’ proofs of probabilistic programs based on the union bound, a technique from basic probability theory. We show how a propositional variant of approximate Hoare Logic (aHL), a program logic for union bound, can be soundly encoded in our system aGKAT. We then illustrate the use of aGKAT on an example of accuracy analysis from the field of differential privacy.
Bernardo Hummes Flores (LIX, École Polytechnique)
Adrienne Lancelot (IRIF, Université Paris Cité)
Light genericity
To better understand Barendregt's genericity for the untyped call-by-value lambda-calculus, we start by first revisiting it in call-by-name, adopting a lighter statement and establishing a connection with contextual equivalence. Then, we use it to give a new, lighter proof of maximality of head contextual equivalence, i.e. that H* is a maximal consistent equational theory. We move on to call-by-value, where we adapt these results and also introduce a new notion dual to light genericity, that we dub co-genericity. Lastly, we give alternative proofs of (co-)genericity based on applicative bisimilarity.
Amélie Ledein (Université de Strasbourg)
Louis Lemonnier (LMF, Université Paris Saclay)
Semantics of Recursion in Quantum Control
Denotational semantics is a cornerstone in the study of programming languages. It aims to translate syntax from a specific language into mathematical objects. The latter helps abstract away in order to prove some properties of the language. When recursion or loops are involved in the language, the mathematical interpretation must have corresponding fixed points or a similar theory. This is the case for classical and probabilistic languages and also quantum programming languages with classical control. Our focus will be on recursion in quantum control. We will show what problems arise on the mathematical side and why the usual tools do not apply in the desired setting. We end with a positive note with guarded quantum recursion.
Valentin Maestracci (I2M, Université Aix-Marseille)
-
There are two types of duality in Linear Logic. The first one is nega- tion, balancing positive and negative formulas. The second one is the duality between linear and non-linear proofs, made symmetrical by Differential Linear Logic. The first duality has been here since the beginning of Linear Logic and has a significance in terms of proof-search and programming operation. However, the computational content of the second is still to understand. In this paper, we reex- press models of Differential Linear Logic in terms of models of Polarized Linear Logic, hoping to get closer to the understanding of Differential Linear Logic. It formalizes Differentiation in terms of a functor on a coslice category, within the linear–non-linear adjunction models of Linear Logic. It is also a first step in studying models mixing polarization and differentiation, concrete instances of which arise in functional analysis.
Giulia Manara (IRIF, Université Paris Cité)
Vincent Moreau (IRIF, Université Paris Cité)
-
A fundamental theme in automata theory is regular languages of words and trees, and their many equivalent definitions. Salvati has proposed a generalization to regular languages of simply typed lambda-terms, defined using denotational semantics in finite sets. \\We provide some evidence for its robustness. First, we give an equivalent characterization that naturally extends the seminal work of Hillebrand and Kanellakis connecting regular languages of words and syntactic lambda-definability. Second, we exhibit a class of categorical models of the simply typed lambda-calculus which all recognize exactly the same class of languages of lambda-terms as the category of finite sets does, when used in Salvati's definition.
The proofs of these two results rely on a new technique called squeezing, inspired by previous categorical accounts of logical relations using the glueing construction. This is joint work with Lê Thành Dũng (Tito) Nguyễn.
Karim Nour (LIMD - LAMA - Université Savoie Mont Blanc)
-
We present a general realizability semantics for the simply typed $\lambda\mu$-calculus. Then we deduce, based on this semantics, a weak and a strong normalization result for two versions of the calculus equipped with certain simplification rules. The novelty in our method, besides its more systematic approach, is the property of its being applicable to a wider set of reduction rules.
Adrien Ragot (LIPN, Université Sorbonne Paris-Nord & Università Degli Studi Roma tre)
An algebraic structure for Linear Realisability
We give a simple algebraic structure M on which we can perform the realisability construction for second order multiplicative linear logic. We show that this structure is an implicative structure hence justifying the terminology of “Linear Realisability”. We show that many adequacy result for MLL2 can be obtain for a whole class of connectives. Enriching the structure M, we show that completeness for MLL can be obtained by chosing an interpretation basis which satisfies a property of commutation with the operation of M. Several known framework are an instances of ours: proof-structures, interaction graphs, positional games, partitions and so on…
Victor Sannier (CRIStAL, Université de Lille)
-
La confidentialité différentielle d'un algorithme, une formalisation statistique de l'idée de protection des données privées, peut être automatiquement garantie en ajoutant du bruit au résultat du calcul à condition de connaître la \emph{sensibilité} dudit algorithme en ses entrées selon une certaine distance. Ainsi Reed et Pierce ont introduit Fuzz, un système de types inspiré de la logique linéaire de Girard pour suivre statiquement la sensibilité des termes d'un langage fonctionnel selon la distance $L^1$. Nous proposons une extension de ce système qui permet de représenter des espaces munis de métriques plus générales, à savoir $L^p$ pour~$p\geq1$, et dont les types sont construits avec des versions paramétrées des connecteurs de la logique linéaire. Dans cet exposé nous donnerons des exemples de son utilisation, montrerons qu'il satisfait de bonnes propriétés syntaxiques et opérationnelles et que des applications de traductions le relie à Fuzz.