Pour l’accès au laboratoire, des indications se trouvent à cette adresse (le programme est prévu pour le train de Paris arrivant à 9h28. Pour le retour, il y a des départs d’Orléans à intervalles réguliers en fin de journée)
This talk investigates the question of denotational invariants of non-well-founded and circular proofs of the linear logic with least and greatest fixed-points. Indeed, while non-wellfounded and circular proof theory made significant progress in the last twenty years, the corresponding denotational semantics is still underdeveloped. We will talk about a denotational semantics for non-wellfounded proofs, based on a notion of totality. Several properties of the semantics will be then discussed: its soundness, the relation between totality and validity and the semantical content of the translation from finitary proofs to circular proofs. Finally, the talk focuses on circular proofs, trying to benefit from their regularity in order to define inductively the interpretation function. It is argued why the usual validity condition is too general for that purpose, while a fragment of circular proofs, strongly valid proofs, constitutes a well-behaved class for such an inductive interpretation. This presentation is based on joint work with Thomas Ehrhard and Alexis Saurin.
This talk, introduces extensions of Baelde et al's bouncing-validity criterion of $\mu MALL_\infty$, a non-wellfounded proof system extending linear logic with least and greatest fixed-points. Non-wellfounded proof systems, rely on a "validity criterion" to distinguish proofs from mere "pre-proofs". The basic idea is a thread-based validity which require every infinite branch to be supported by a thread, that is a sequence of formulas occurring in the branch. This thread should witness the infinite unfolding of an inductive hypothesis or of a coinductive conclusion; computationally, this corresponds to asking that an inductive input-data is consumed infinitely often or that a coinductive output-data is infinitely produced.
The first "validity criterion" has been framed in terms of "valid straight-threads," where the sequence of formulas are completely contained in the branch. In 2022, Baelde et al. proposed a novel criterion: the "bouncing validity criterion", accommodating a wider range of proofs by allowing threads to get in and out of branches by "bouncing on axiom and cut rules. Nevertheless, certain proofs still eluded this criterion. To address this, we propose two additional validity criteria that satisfy cut-elimination property.
These new bouncing criteria relax the requirement that the "visible part" of a validating thread must be entirely contained within the branch. Instead, they only necessitate that the visible part intersects the branch infinitely often. During the presentation, we will provide an intuitive understanding of why these criteria preserve the cut-elimination property while highlighting their limitations concerning the focalization property.
This is a joint work with Alexis Saurin."
Functional reactive programming (FRP) has been introduced by Elliott with FRAN in 1997. FRP is a concept aiming to describe interactive programming languages with a high level syntax, based on functional methods. Interest in FRP has been growing since then with many proposals. In most cases, language properties are established with handmade proofs and not with proof assistants, which can lead to the omission of important steps that appear to be crucial with respect to the language features.
As part of my thesis, we have chosen to formally prove the properties of language Wormholes using the proof assistant Coq. During this presentation, we will briefly introduce the main concepts, then we will talk about the specificity of the language and finally we will discuss the difficulties encountered during the formalization still in progress.
Le projet Vélus est une formalisation d'un sous-ensemble du langage Scade dans l'assistant de preuves Coq. Il propose une formalisation de la sémantique dynamique du langage sous forme de relations entre flots infinis d'entrées et de sorties. Il inclut aussi un compilateur qui utilise CompCert, un compilateur vérifié pour C, pour produire du code assembleur. Enfin, il fournit une preuve de bout en bout que ce compilateur préserve la sémantique à flots de données des programmes sources. Mon travail de thèse étends Vélus avec des blocs de contrôles inspirés de Scade 6 et Lucid Synchrone, qui permettent la définition de comportement modaux: blocs switch, variables partagées (last x), blocs de réinitialisation, et machines à états hiérarchiques.
Dans cette présentation, on montrera le nouveau modèle sémantique développé pour intégrer ces blocs dans la sémantique à flots de données de Vélus. On discutera des propriétés dynamiques de ce modèle, que nous avons pu prouver en utilisant une analyse de dépendance vérifiée et un schéma d'induction spécifique aux programmes ne contenant pas de cycle de dépendance. On présentera aussi la compilation de ces constructions, en montrant les adaptations nécessaires aux schémas de compilation source à source standard, et les invariants permettant de prouver la correction de ces schémas. Enfin, on expliquera pourquoi l'arrière du compilateur doit également être modifié pour compiler ces constructions efficacement.
Dans cette présentation, je décrirai comment on implémente dans Coq une sémantique dénotationnelle du langage Lustre et comment on prouve son équivalence avec le modèle relationnel existant dans le compilateur. Cette approche, constructive, permet de résoudre le problème d'existence d'une sémantique et facilite la preuve de certaines propriétés du langage.