News & Events
Portraits de chercheurs : Evelyne Contejean
Un article sur Evelyne Contejean vient de paraitre dans la rubrique Portraits de chercheurs des Actualités de l'Université Paris-Saclay.
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.
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.
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.
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.
Start-up ’’innatelogic’’ sélectionné pour RISE - CNRS Innovation
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.