Journées 2023 du GT Scalp

Du 27 au 29 novembre 2023 à Orléans

Introduction

Les rencontres 2023 du GT Scalp se tiendront à Orléans du 27 au 29 novembre. Les journées débuteront lundi en milieu de journée (premier exposé vers 13H) et s'achèveront mercredi en début d'après-midi. (Une liste d'hôtels est fournie plus bas.)

Les inscriptions sont ouvertes, les informations sur les exposés invités et contribués, ainsi que l'organisation pratique des journées se trouvent ci-dessous.

Exposés invités

  • Sylvie Boldo (INRIA Saclay) Formalization of applied mathematics: a journey
    • Applied mathematics is an attractive application for formal verification of programs as it may help spread its use in other communities. But it requires a large corpus of formalized mathematics. I will describe various results in formalized applied mathematics, with a focus on the underlying axioms we chose to use.
  • Gianluca Curzi (U. Gothenburg) Non-wellfounded parsimonious logic, infinitary cut-elimination and (non-uniform) polynomial time
    • We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Also, we show that cut-elimination preserves the progressive criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Leveraging on the latter, we show that our non-wellfounded proof systems for parsimonious logic can be used to characterise the complexity class FPTIME and its non-uniform version FP/poly.
  • Laura Fontanella (LACL, UPEC) Realizability models for large cardinals
    • Realizabilty is a branch of logic that aims at extracting the computational content of mathematical proofs by establishing a correspondence between proofs and programs. Invented by S.C. Kleene in the 1945 to develop a connection between intuitionism and Turing computable functions, realizability has evolved to include not only classical logic but even set theory, thanks to the work of J-L. Krivine. Krivine’s work made possible to build realizability models for Zermelo-Frænkel set theory, ZF, assuming its consistency. Nevertheless, a large part of set theoretic research involves investigating further axioms that are known as large cardinals axioms; in this talk, we focus on four large cardinals axioms: the axioms of (strongly) inaccessible cardinal, Mahlo cardinals, measurable cardinals and Reinhardt cardinals; we show how to build realizability models for each of these four axioms assuming their consistency relative to ZFC or ZF.
  • Armaël Gueneau (INRIA Saclay) Melocoton: A Program Logic for Verified Interoperability Between OCaml and C
    • In recent years, there has been tremendous progress on developing program logics for verifying the correctness of programs in a rich and diverse array of languages. Thus far, however, such logics have assumed that programs are written entirely in a single programming language. In practice, this assumption rarely holds since programs are often composed of components written in different programming languages, which interact with one another via some kind of foreign function interface (FFI).
      In this talk, I will present our first steps towards the goal of developing program logics for multi-language verification. Specifically, I will present Melocoton, a multi-language program verification system for reasoning about OCaml, C, and their interactions through the OCaml FFI. Melocoton consists of the first formal semantics of (a large subset of) the OCaml FFI—previously only described in prose in the OCaml manual—as well as the first program logic to reason about the interactions of program components written in OCaml and C.
      Melocoton is fully mechanized in Coq on top of the Iris separation logic framework.

Inscriptions et propositions d'exposé

dupanloup.jpg

Inscription

L'inscription est gratuite mais obligatoire.

L'inscription se fait via ce lien.

Propositions d'exposé

La durée des exposés n'a pas encore été fixée, elle dépendra du nombre de propositions et des souhaits des orateurs/oratrices.

Comme d'habitude, nous apprécions spécialement les contributions des jeunes (doctorant(e)s et post-doc) et demandons aux encadrant(e)s d'encourager leurs encadré(e)s à présenter leurs travaux.

L'appel à contributions est clos, mais vous pouvez toujours vous inscrire pour participer!

Informations pratiques

Les rencontres se dérouleront dans l'Hôtel Dupanloup (1 rue Dupanloup - 45000 ORLÉANS).

Quelques suggestions d'hôtels

  • Le Jackotel (bien situé, parking, bon marché)
  • Hôtel St Martin (proche gare et conférence)
  • Hôtel d’Orléans (plein centre, donc proche de la gare et du lieu des journées
  • Campanile Orléans centre (proche gare)
  • Hôtel de l'Abeille (proche gare)
  • Appart Hôtel - Orléans Jeanne d'Arc (proche du lieu des rencontres)

Quelques suggestions de restauration à proximité

  • rue Ste Catherine :
    • Le brin de zinc (cuisine traditionnelle variée),
    • Don Camillo (italien),
    • Heureux comme Alexandre (fondues. petit espace, réserver pour le soir éventuellement pour petits effectifs).
  • rue de Bourgogne : La rue regorge de restaurants et bars, pour différents styles et budgets. Pas d'adresse spécifique à indiquer, se laisser aller à son intuition (ou aux recommandations d'applications dédiées)!

Programme préliminaire

En plus du programme scientifique stricto sensu, nous organiserons un “business meeting” ainsi que, comme convenu lors des dernières journées du GT, au CIRM, un temps de discussion politique.

Liste des exposés contribués

  • 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)
    • Generic bidirectional typing for dependent type theories
    • 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)
    • Characterization of robot tasks
  • 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)
    • Proof interoperability with a lambda-calculus
    • TBA
  • 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)
    • Functorial Models of Differential Linear Logic
    • 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é)
    • On non-commutative logic and process calculi
    • The calculus of communicating systems (CCS) is a process calculus for the specification and modelling of discrete communicating systems. In this talk we define a sequent calculus operating on formulas encoding CCS processes capturing the operational semantics for the recursion-free fragment of CCS. We establish a correspondence between executions of processes and (branches of) proofs. We show that these rules are derivable in a sequent system extending the multiplicative and additive linear logic with a non-commutative connective and we prove cut-elimination for this system. We conclude by discussing future research directions.
  • Vincent Moreau (IRIF, Université Paris Cité)
    • Finitary semantics and regular languages of lambda-terms
    • 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)
    • Normalization properties of lambda-mu-calculus using realizability semantics
    • 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)
    • Un système de types linéaires pour la confidentialité différentielle selon les métriques vectorielles
    • 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.

Participants

TBA

Comité d'organisation

  • Jules Chouquet
  • Pierre Clairambault
  • Chantal Keller
  • Alexis Saurin