First meeting of the SeSTeRce project, lead by Jules Chouquet.<\/p>\n\n\n\n
10h00 \u2014 10h30 : Accueil-caf\u00e9\u00a0<\/p>\n\n\n\n
10h30 \u2014 11h15 : Farzad Jafarrahmani (LIP6) On denotations of circular and non-wellfounded proofs\u00a0<\/strong><\/p>\n\n\n\n \u00a0\u00a0 \u00a0This 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 \u00a0years, the corresponding denotational semantics is still underdeveloped. We will talk about a denotational semantics for non-wellfounded proofs, based on a notion of totality. \u00a0Several 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 \u00a0from 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.\u00a0<\/p>\n\n\n\n 11h15 \u2014 12h00 : Esa\u00efe Bauer [\u00c0 venir]\u00a0<\/p>\n\n\n\n 12h00 \u2014 12h30 : Questions\/discussions\/retards <\/p>\n\n\n\n 12h30 \u2014 13h30 : Pause repas <\/p>\n\n\n\n 13h30 \u2014 14h15 : Jordan Ischard (LIFO)\u00a0Formalization of an FRP language with references\u00a0<\/strong><\/p>\n\n\n\n \u00a0\u00a0 \u00a0Functional 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.\u00a0<\/p>\n\n\n\n 14h15 \u2014 15h00 : Basile Pesin (ENS,Inria)\u00a0V\u00e9rification formelle d’un compilateur pour un langage synchrone \u00e0 flots de donn\u00e9es avec machines \u00e0 \u00e9tats<\/strong>\u00a0<\/p>\n\n\n\n \u00a0\u00a0 \u00a0Le projet V\u00e9lus est une formalisation d’un sous-ensemble du langage Scade dans l’assistant de preuves Coq. Il propose une formalisation de la s\u00e9mantique dynamique du langage sous forme de relations entre flots infinis d’entr\u00e9es et de sorties. Il inclut aussi un compilateur qui utilise CompCert, un compilateur v\u00e9rifi\u00e9 pour C, pour produire du code assembleur. Enfin, il fournit une preuve de bout en bout que ce compilateur pr\u00e9serve la s\u00e9mantique \u00e0 flots de donn\u00e9es des programmes sources. Mon travail de th\u00e8se \u00e9tends V\u00e9lus avec des blocs de contr\u00f4les inspir\u00e9s de Scade 6 et Lucid Synchrone, qui permettent la d\u00e9finition de comportement modaux: blocs switch, variables partag\u00e9es (last x), blocs de r\u00e9initialisation, et machines \u00e0 \u00e9tats hi\u00e9rarchiques.\u00a0Dans cette pr\u00e9sentation, on montrera le nouveau mod\u00e8le s\u00e9mantique d\u00e9velopp\u00e9 pour int\u00e9grer ces blocs dans la s\u00e9mantique \u00e0 flots de donn\u00e9es de V\u00e9lus. On discutera des propri\u00e9t\u00e9s dynamiques de ce mod\u00e8le, que nous avons pu prouver en utilisant une analyse de d\u00e9pendance v\u00e9rifi\u00e9e et un sch\u00e9ma d’induction sp\u00e9cifique aux programmes ne contenant pas de cycle de d\u00e9pendance. On pr\u00e9sentera aussi la compilation de ces constructions, en montrant les adaptations n\u00e9cessaires aux sch\u00e9mas de compilation source \u00e0 source standard, et les invariants permettant de prouver la correction de ces sch\u00e9mas. Enfin, on expliquera pourquoi l’arri\u00e8re du compilateur doit \u00e9galement \u00eatre modifi\u00e9 pour compiler ces constructions efficacement.\u00a0<\/p>\n\n\n\n 15h00 \u2014 15h15 : Pause caf\u00e9 <\/p>\n\n\n\n 15h15 \u2014 16h00 : Paul Jeanmaire (ENS,Inria) M\u00e9canisation d’une s\u00e9mantique d\u00e9notationnelle dans un compilateur Lustre v\u00e9rifi\u00e9.\u00a0<\/strong><\/p>\n\n\n\n \u00a0\u00a0 \u00a0Dans cette pr\u00e9sentation, je d\u00e9crirai comment on impl\u00e9mente dans Coq une s\u00e9mantique d\u00e9notationnelle du langage Lustre et comment on prouve son \u00e9quivalence avec le mod\u00e8le relationnel existant dans le compilateur. Cette approche, constructive, permet de r\u00e9soudre le probl\u00e8me d’existence d’une s\u00e9mantique et facilite la preuve de certaines propri\u00e9t\u00e9s du langage.\u00a0 First meeting of the SeSTeRce project, lead by Jules Chouquet. 10h00 \u2014 10h30 : Accueil-caf\u00e9\u00a0 10h30 \u2014 11h15 : Farzad Jafarrahmani (LIP6) On denotations of circular and non-wellfounded proofs\u00a0 \u00a0\u00a0 \u00a0This 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 … Continue reading “[September 2023] First SeSTeRce Day”<\/span><\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-568","post","type-post","status-publish","format-standard","hentry","category-non-classe"],"_links":{"self":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/568","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/comments?post=568"}],"version-history":[{"count":1,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/568\/revisions"}],"predecessor-version":[{"id":571,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/posts\/568\/revisions\/571"}],"wp:attachment":[{"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/media?parent=568"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/categories?post=568"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.univ-orleans.fr\/lifo\/equipes\/lmv\/index.php\/wp-json\/wp\/v2\/tags?post=568"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}
<\/p>\n","protected":false},"excerpt":{"rendered":"