News & Events
PhD Defence: Gabriel Hondet
Expressing Predicate Subtyping in Computational Logical Frameworks
by Gabriel Hondet
Tuesday 27 September 2022 at 5pm
ENS Paris-Saclay, Room 1Z14
Abstract: Safe programming as well as most proof systems rely on typing. The more a type system is expressive, the more these types can be used to encode invariants which are therefore verified mechanically through type checking procedures. Predicate subtyping extends simple type theory by allowing terms to be defined by predicates. A predicate subtype { x : A | P(x) } is inhabited by terms t of type A for which P(t) holds. This extension provides a rich and intuitive but undecidable type system.
Prix Doctorants STIC du plateau de Saclay pour Pierre Vandenhove
Pierre Vandenhove est lauréat d'un accessit au Prix « Doctorants » du plateau de Saclay dans la domaine STIC - Sciences et Technologies de l'Information et la Communication.
Le prix "Meilleure production scientifique en STIC du plateau de Saclay" soutenu par le LabEX DigiCosme récompense chaque année les travaux de recherche de doctorants de l’École doctorale STIC de l’Université Paris-Saclay et de l’École doctorale IP Paris pour leur excellence. L’objectif de ce prix est de dynamiser et de motiver les doctorants en les récompensant et en exposant leurs travaux à la communauté, en particulier aux jeunes chercheurs qui débutent leur thèse.
Nouveau livre : Informatique MPI
Fin août 2022, vient de sortir un nouveau livre par Thibaut Balabonski, Sylvain Conchon, Jean-Christophe Filliâtre, Kim Nguyễn, Laurent Sartre.
Il s'intitule "Informatique - MPI2/MPI - CPGE 1re et 2e années: Cours et exercices corrigés" et vise les enseignants d'informatique et les élèves des nouvelles classes préparatoires MP2I et MPI. En voici la table des matières.
En plus de son poids, il faut souligner le site lié qui fournit tous les codes et données du livre.
Philippe Schnoebelen receives LICS 2022 Test-of-Time Award
Philippe Schnoebelen receives the LICS Test-of-Time Award 2022 for the article Temporal Logic with Forgettable Past co-authored with François Laroussinie (Université Paris-Cité) and Nicolas Markey (IRISA, CNRS). At the time of the writing of the article in 2002, the three authors were members of the same laboratory LSV which integrated the LMF in 2021.
The LICS - Logic in Computer Science conference is the most prestigious annual forum on theoretical and practical topics in computer science related to logic in a broad sense. The LICS Test-of-Time Award award recognizes a small number of papers from the LICS proceedings over the past 20 years (i.e., the paper in question dates from LICS 2002 and was considered this year) that have best stood the "test of time." In selecting these papers, the award committee considers the influence they have had since their publication; due to the fundamental nature of LICS work, the impact is often not felt immediately, hence the 20-year perspective.
Lasting impact on the foundations of automatic verification
According to the awarding jury, "This extraordinarily clear and elegant paper provides well-motivated and complete characterizations of succinctness and complexity of linear temporal logic with past operators and with forgettable past. It has contributed to spur a vibrant research program on logics and automata over infinite alphabets, from hardness results to the translations of logical formulas into alternating register automata, along with the attendant powerful algorithmic consequences for model checking. It has also strongly influenced the development of the field of nominal computation, and it is no exaggeration to state that the present paper has tangibly led to a number of invited talks, Dagstuhl-type workshops, research grants, academic positions, and prizes, and continues to have an ongoing and lasting impact in the areas of automata theory and the foundations of automated verification."
The award will be presented at the conference awards session LICS 2022 organized from August 2 to 5 in the framework of FLOC 2022 -- Federated Logic Conference in Haifa, Israel.
LICS Test-of-Time Award pour Philippe Schnoebelen
Philippe Schnoebelen reçoit le LICS Test-of-Time Award 2022 pour l'article Temporal Logic with Forgettable Past cosigné avec François Laroussinie (Université Paris-Cité) et Nicolas Markey (IRISA, CNRS). Au moment de la rédaction de l'article en 2002, les trois auteurs étaient membres du même laboratoire LSV qui a intégré le LMF en 2021.
La conférence LICS — Logic in Computer Science est le plus prestigieux forum annuel sur des sujets théoriques et pratiques en informatique liés à la logique au sens large. Le prix LICS Test-of-Time Award récompense un petit nombre d'articles tirés des actes du LICS des 20 dernières années (c'est-à-dire que l'article en question date du LICS 2002 et a été pris en considération cette année) qui ont le mieux résisté à "l'épreuve du temps”. En sélectionnant ces articles, le comité d'attribution tient compte de l'influence qu'ils ont eue depuis leur publication ; en raison de la nature fondamentale des travaux de la LICS, l'impact n'est souvent pas ressenti immédiatement, d'où la perspective de 20 ans.
Fondaments de la vérification automatique
Selon le jury d'attribution : “Cet article extraordinairement clair et élégant fournit des caractérisations complètes et bien motivées de la succinctivité et de la complexité de la logique temporelle linéaire avec opérateurs passés et avec passé oubliable. Il a contribué à stimuler un programme de recherche dynamique sur les logiques et les automates sur les alphabets infinis, depuis les résultats de dureté jusqu'aux traductions des formules logiques en automates à registre alternatif, avec les conséquences algorithmiques puissantes qui en découlent pour le model checking. Il a également fortement influencé le développement du domaine du calcul nominal, et il n'est pas exagéré d'affirmer que le présent article a conduit de manière tangible à un certain nombre de conférences invitées, d'ateliers de type Dagstuhl, de subventions de recherche, de postes universitaires et de prix, et continue d'avoir un impact continu et durable dans les domaines de la théorie des automates et des fondements de la vérification automatique.”
Le prix a été remis lors de la conférence LICS 2022 organisée du 2 au 5 aout dans le cadre de FLOC 2022 -- Federated Logic Conference à Haifa, Israel.
PhD Defence: Dongho Lee
Formal Methods for Quantum Programming Languages
by Dongho Lee
Thursday 21 July 2022 at 2pm
Online
Abstract: The quantum random-access machine (QRAM) model is a practical model of quantum computation composed of a classical computer and a quantum processor communicating with each other. The program is executed on the classical computer. It can send instructions corresponding to quantum operations and receive measurement outcomes from the quantum co-processor. This model is expected to be the model of quantum computation in the near future, and a group of quantum programming languages has been developed based on it.
PLDI'22 Distinguished Paper Award for Xavier Denis, Jacques-Henri Jourdan
Xavier Denis, Jacques-Henri Jourdan and their co-authors Yusuke Matsushita and Derek Dreyer received a Distinguished Paper Award for their contribution RustHornBelt: A semantic foundation for functional verification of Rust programs with unsafe code at PLDI 2022, the 43rd ACM SIGPLAN Conference on Programming Language Design and Implementation.
PLDI is "the premier forum in the field of programming languages and programming systems research, covering the areas of design, implementation, theory, applications, and performance". It is one of the four prestigious conferences of SIGPLAN, ACM's special interest group on programming languages. Each year, among the 60-80 papers presented at the conference, only a few are selected to receive the distinguished paper award, based on their quality, and RustHornBelt is one of them for the year 2022!
Start-up ’’innatelogic’’ selectionné pour RISE - CNRS Innovations
Le projet innatelogic, porté par Benedikt Bollig, Matthias Függer et Thomas Nowak, a été sélectionné pour faire partie de la prochaine promotion du programme RISE de CNRS Innovation. RISE accompagne, pendant un an, des projets de startup deeptech exploitant une technologie issue d'un laboratoire du CNRS.
Dans la quête de la prochaine génération de circuits en biologie synthétique, l'objectif d'innatelogic est de développer des logiciels innovants, basés sur l'intelligence artificielle, pour la découverte automatisée de modèles biochimiques. Ces modèles servent à optimiser les processus de la bio-production et à développer de nouveaux produits en pharmacocinétique.
Journées nationales du GDR Sécurité Informatique
Caroline Fontaine organise les Journées Nationales du GDR Sécurité Informatique au Campus Cyber de La Défense du 22 au 24 juin 2022.
Le GDR Sécurité Informatique est un outil d'animation de la recherche française créé par l'Institut des sciences de l’information et de leurs interactions (INS2I) du CNRS, et ouvert à toute la communauté. Les thématiques couvertes incluent le codage et la cryptographie, les méthodes formelles pour la sécurité, la protection de la vie privée, la sécurité des systèmes, des logiciels et des réseaux, la sécurité des systèmes matériels, la sécurité et les données multimédia. Caroline Fontaine dirige le GDR depuis juillet 2021.
JFLA 2022
Chantal Keller co-organise le 33e édition des Journées Francophones des Langages Applicatifs (JFLA 2022) à Saint-Médard-d'Excideuil, dans le Périgord.
