First meeting of the SeSTeRce project, lead by Jules Chouquet.
10h00 — 10h30 : Accueil-café
10h30 — 11h15 : Farzad Jafarrahmani (LIP6) On denotations of circular and non-wellfounded proofs
This talk investigates the question of denotational invariants of non-wellfounded 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.
11h15 — 12h00 : Esaïe Bauer [À venir]
12h00 — 12h30 : Questions/discussions/retards
12h30 — 13h30 : Pause repas
13h30 — 14h15 : Jordan Ischard (LIFO) Formalization of an FRP language with references
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.
14h15 — 15h00 : Basile Pesin (ENS,Inria) Vérification formelle d’un compilateur pour un langage synchrone à flots de données avec machines à états
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.
15h00 — 15h15 : Pause café
15h15 — 16h00 : Paul Jeanmaire (ENS,Inria) Mécanisation d’une sémantique dénotationnelle dans un compilateur Lustre vérifié.
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.