BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//LORIA - ECPv6.16.2//NONSGML v1.0//EN
CALSCALE:GREGORIAN
METHOD:PUBLISH
X-WR-CALNAME:LORIA
X-ORIGINAL-URL:https://www.loria.fr
X-WR-CALDESC:Évènements pour LORIA
REFRESH-INTERVAL;VALUE=DURATION:PT1H
X-Robots-Tag:noindex
X-PUBLISHED-TTL:PT1H
BEGIN:VTIMEZONE
TZID:Europe/Paris
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20250330T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20251026T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20260329T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20261025T010000
END:STANDARD
BEGIN:DAYLIGHT
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
TZNAME:CEST
DTSTART:20270328T010000
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
TZNAME:CET
DTSTART:20271031T010000
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260108T093000
DTEND;TZID=Europe/Paris:20260108T113000
DTSTAMP:20260515T052520
CREATED:20251218T145216Z
LAST-MODIFIED:20251218T145216Z
UID:28801-1767864600-1767871800@www.loria.fr
SUMMARY:Séminaire Département 3
DESCRIPTION:Le Département 3 a le plaisir de proposer un talk de Sounak Kar\, TU Delft\, intitulé \nOn Efficiency and Fairness of Resource Distribution in Quantum\nRepeater Networks.\n\nEn visio sur https://u2l.fr/sounak
URL:https://www.loria.fr/event/seminaire-departement-3/
CATEGORIES:Séminaire
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260112T093000
DTEND;TZID=Europe/Paris:20260112T120000
DTSTAMP:20260515T052520
CREATED:20260113T120946Z
LAST-MODIFIED:20260115T142246Z
UID:28647-1768210200-1768219200@www.loria.fr
SUMMARY:Soutenance de thèse de Amandine LECOMTE
DESCRIPTION:Amandine LECOMTE (SEMAGRAMME)\, défendra sa thèse intitulée \nEtude des indices multimodaux discursifs au cours de la construction dialogique en entretien clinique auprès de sujets atteints de schizophrénie\n– Approche des conditions de possibilité ou de contrôle d’un « effet clinique ».\nLa soutenance aura lieu en public le lundi 12 janvier 2026 à 9h30 dans l’amphithéâtre Gilles Kahn. La présentation sera en français. \n\nComposition du jury :\n\n\nDirecteurs de thèse : Michel MUSIOL (Professeur\, Atilf-Cnrs\, Université de Lorraine)\, Alexandra KONÏG (HDR\, ki:elements\, Université Côte d’Azur)\nRapportrices : Emmanuèle AURIAC-SLUSARCZYK (Maîtresse de Conférence émérite\, INSPE Clermont-Auvergne\, Chamalières)\, Katia KOSTULSKI (Professeure\,CRTD Cnam\, Paris)\nExaminateurs: Maxime AMBLARD (Professeur\, LORIA\, Université de Lorraine)\, Christophe LEMEY(Docteur au CHU de Brest – Hôpital Morvan)\nPrésident de jury: Philippe De GROOTE (Directeur de recherche Inria Nancy – Grand Est) \n\n\n\n\nRésumé  :\nCette thèse propose de circonscrire un des effets possibles de l’entretien clinique dans le cadre particulier de la recherche.\nIl s’agit de mettre en évidence\, de manière précise et formelle\, des indicateurs de type comportementaux-discursifs et sémantico-représentationnels de l’évolution du sujet au niveau de la configuration des transactions dialogiques.\nCeci à partir d’une population atteinte d’une pathologie psychiatrique avérée\, d’une population témoin ne présentant pas de pathologie mentale ainsi qu’auprès d’une personne présentant des symptômes de première épisode psychotique.\nCe cadre exploratoire tente alors d’appréhender la multimodalité de l’interaction verbale à travers les réactions vocales\, verbales\, mimées voir oculomotrices.\n\n\n\n\nAbstract :\n\nThis thesis propose to define one of the possible effects of clinical interviews in the specific context of research.\nThe aim is to highlight\, in a precise and formal manner\, behavioral-discursive and semantic-representational indicators of the subject’s evolution in terms of the configuration of dialogic transactions.\nThis is based on a population with a proven psychiatric disorder\, a control population with no mental disorder\, and a person with symptoms of a first psychotic episode.\nThis exploratory framework attempts to understand the multimodality of verbal interaction through vocal\, verbal\, mimed\, and even oculomotor reactions.
URL:https://www.loria.fr/event/soutenance-de-these-amandine_lecomte/
CATEGORIES:Soutenance
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260115T140000
DTEND;TZID=Europe/Paris:20260115T160000
DTSTAMP:20260515T052520
CREATED:20251124T150839Z
LAST-MODIFIED:20251124T150923Z
UID:28674-1768485600-1768492800@www.loria.fr
SUMMARY:Théâtre Scientifique au Lycée
DESCRIPTION:Le Procès du Robot\n\nest un format original mêlant sciences\, société… et théâtre d’impro !\nUn moment d’échanges et de réflexions autour des grands enjeux de l’IA et ses applications quotidiennes… \n\nhttps://iww.inria.fr/NanSciNum/theatre-scientifique/le-proces-du-robot/
URL:https://www.loria.fr/event/theatre-scientifique-au-lycee/
LOCATION:Lycée Condorcet Schoeneck
CATEGORIES:Spectacle
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260122T140000
DTEND;TZID=Europe/Paris:20260122T173000
DTSTAMP:20260515T052520
CREATED:20260113T121205Z
LAST-MODIFIED:20260113T121205Z
UID:28728-1769090400-1769103000@www.loria.fr
SUMMARY:Visite des étudiant·es des classes prépa scientifiques du Lycée Henri Poincaré
DESCRIPTION:Le Loria a le plaisir d’accueillir des étudiant·es des classes prépa scientifiques du Lycée Henri Poincaré pour une demi-journées d’échanges et de conférences.
URL:https://www.loria.fr/event/visite-des-etudiant%c2%b7es-des-classes-prepa-scientifiques-du-lycee-henri-poincare/
LOCATION:A008
CATEGORIES:Conférence,Manifestation
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260126T110000
DTEND;TZID=Europe/Paris:20260126T130000
DTSTAMP:20260515T052520
CREATED:20251202T094348Z
LAST-MODIFIED:20260121T164100Z
UID:28721-1769425200-1769432400@www.loria.fr
SUMMARY:Colloquium du Loria : Laura Kovács
DESCRIPTION:The Loria is proud to announce a colloquium presentation by Laura Kovács on \nInduction and synthesis in saturation-based theorem proving.\nLaura Kovács is a professor at the Faculty of Informatics of Vienna University of Technology (Vienna\, Austria) and a leading researcher in the field of automated reasoning and symbolic computation. \nAbstract:\nProof by induction is commonplace in mathematics. logic\, formal verification\, cybersecurity\, and many more areas. This talk overviews recent progress in automating inductive reasoning in saturation-based first-order theorem proving We formalize applications of induction as new inference rules of the saturation process\, add instances of appropriate induction schemata to the search space\, and use these rules and instances immediately upon their addition for the purpose of guiding induction. We also synthesize code that satisfies a given (inductive) logical specification\, while proving the specification in a saturation-based framework. \n  \nPeople from outside the Loria must register by sending an email to Annabelle Chapron  –  annabelle.chapron (at) loria.fr  –  before January 25th.\nLes visiteurs devront se munir de leur pièce d’identité. \n——————————————————————————– \n\n\nLes membres du Loria sont fiers d’accueillir Laura Kovács\, qui présentera un exposé intitulé :  \nInduction and synthesis in saturation-based theorem proving.\nLaura Kovács\, professeure à la Faculté d’Informatique de l’Université de Technologie de Vienne (Autriche)\, est une chercheuse de premier plan dans le domaine du raisonnement automatisé et du calcul symbolique.  \nRésumé :  \nLa démonstration par induction est courante en mathématiques\, en logique\, en vérification formelle\, en cybersécurité et dans de nombreux autres domaines. Cette conférence présente les progrès récents en matière d’automatisation du raisonnement inductif dans la démonstration de théorèmes du premier ordre par saturation. Nous formalisons les applications de l’induction sous forme de nouvelles règles d’inférence du processus de saturation\, ajoutons des instances de schémas d’induction appropriés à l’espace de recherche et utilisons ces règles et instances dès leur ajout afin de guider l’induction. Nous synthétisons également du code qui satisfait une spécification logique (inductive) donnée\, tout en démontrant cette spécification dans un cadre basé sur la saturation. \n\n\nLes personnes extérieures au Loria doivent s’inscrire en envoyant un mail à Annabelle Chapron  –  annabelle.chapron (at) loria.fr  –  avant le 25 janvier.\nLes visiteurs devront se munir de leur pièce d’identité.
URL:https://www.loria.fr/event/colloquium-du-loria-laura-kovacs/
LOCATION:Amphithéâtre du Loria
CATEGORIES:Colloquium Loria
END:VEVENT
BEGIN:VEVENT
DTSTART;TZID=Europe/Paris:20260126T140000
DTEND;TZID=Europe/Paris:20260126T170000
DTSTAMP:20260515T052520
CREATED:20260115T141709Z
LAST-MODIFIED:20260115T141709Z
UID:28834-1769436000-1769446800@www.loria.fr
SUMMARY:Soutenance de thèse de Alessio Coltellacci
DESCRIPTION:Alessio Coltellacci (Veridis)\, défendra sa thèse intitulée \nReconstruction des preuves SMT dans Lambdapi.\nLa soutenance se déroulera en anglais le lundi 26 janvier 2026 à 14h au LORIA\, en salle C005. Elle sera suivie d’un pot devant la salle. \nPour ceux qui ne pourraient pas venir\, la soutenance sera diffusée en visio (accessible à partir de 14h00\, possibilité de rejoindre depuis un navigateur web) : \nhttps://cnrs.zoom.us/j/95435518789?pwd=RiIzDeE5HIJEofM1x4g3raM9KZ3Y5x.1 \nJury :\n\nLaura Kovács\, Vienna University of Technology (rapporteuse)\nAlexander Steen\, University of Greifswald (rapporteur)\nChantal Keller\, LMF/Université Paris-Saclay (examinatrice)\nMathias Fleury\, University of Freiburg (examinateur)\nRégine Laleau\, Université de Paris-Est Créteil (examinatrice)\nStephan Merz\, INRIA/Université de Lorraine (directeur de thèse)\n\nRésumé :\nLes démonstrateurs automatiques de théorèmes modernes sont de plus en plus plébiscités pour établir la correction de systèmes informatiques critiques. Parmi eux\, les solveurs de satisfiabilité modulo des théories (SMT) occupent une place centrale\, en raison de leur grande expressivité et de leur efficacité dans le traitement de raisonnements logiques complexes. Cependant\, l’ampleur de leur base de code\, conjuguée à la sophistication de leur architecture logicielle\, rend toute vérification formelle exhaustive impraticable\, soulevant ainsi une question fondamentale de confiance: \nDans quelle mesure peut-on accorder foi à la correction des résultats produits par ces solveurs ? \nUne réponse particulièrement prometteuse à cette problématique réside dans le recours à la journalisation de preuves (proof logging)\, approche consistant à faire produire par les solveurs des traces de preuve susceptibles d’être vérifiées de manière indépendante par des vérificateurs externes. Le format Alethe est récemment apparu comme un standard pour représenter de telles preuves SMT. Plusieurs solveurs SMT ont adopté le format Alethe. Néanmoins\, l’absence actuelle d’un vérificateur de preuves certifié pour Alethe en limite encore l’adoption. \nDans cette thèse\, nous proposons un outil permettant de traduire les preuves SMT produites au format Alethe vers l’assistant de preuve Lambdapi\, une implémentation du λΠ-calcul modulo la réécriture. Lambdapi est un assistant de preuve fondationnel\, basé sur la théorie des types dépendants et sur des règles de réécriture\, conçu pour servir de pivot pour l’échange de preuves entre assistants de preuve interactifs. Nous présentons un encodage modulaire de la logique SMT et des règles Alethe dans Lambdapi\, couvrant des théories fondamentales telles que le raisonnement du premier ordre et l’arithmétique linéaire. \nNous détaillons ensuite le processus de reconstruction\, qui requiert des techniques telles que la démonstration par réflexion et l’élaboration de simplifications spécifiques aux solveurs. Enfin\, nous évaluons notre implémentation sur des benchmarks et montrons que les preuves Alethe générées par des solveurs SMT modernes peuvent être reconstruites de manière efficace et fiable dans Lambdapi\, ouvrant ainsi la voie à des preuves SMT à la fois vérifiées et portables. \n  \n\n\nAlessio Coltellacci (Veridis)\, will defend his thesis entitled \nReconstructing SMT Proofs in Lambdapi.\nThe defense will be held in English on Monday 26th\, 2026 at 2:00 P.M. at LORIA\, in room C005.\nThe defense will be followed by a pot de thèse in front of the room. \nFor those who cannot attend in person\, the defense will be streamed online (accessible from 2 P.M.\, you can join directly from a web browser): \nhttps://cnrs.zoom.us/j/95435518789?pwd=RiIzDeE5HIJEofM1x4g3raM9KZ3Y5x.1 \nJury:\n\nLaura Kovács\, Vienna University of Technology (reviewer)\nAlexander Steen\, University of Greifswald (reviewer)\nChantal Keller\, LMF/University Paris-Saclay (examiner)\nMathias Fleury\, University of Freiburg (examiner)\nRégine Laleau\, University Paris-Est Créteil (examiner)\nStephan Merz\, Inria/University of Lorraine (PhD supervisor)\n\nAbstract:\nPowerful modern automated theorem provers are increasingly used to establish the correctness of critical computer systems. Among them\, Satisfiability Modulo Theories (SMT) solvers play a central role thanks to their expressive power and efficiency in handling complex logical reasoning tasks. However\, their size and complexity make full formal verification of their implementations impractical\, raising a fundamental question of trust: \nCan we trust the correctness of their results? \nA promising answer lies in proof logging\, where solvers produce proof traces that proof checkers can independently check. The Alethe format has recently emerged as a unified framework for representing such SMT proofs. Several SMT solvers have adopted the Alethe format. However\, Alethe lacks a certified proof checker\, limiting its adoption and trustworthiness. \nIn this thesis\, we propose a reconstruction framework that translates Alethe proof traces into the Lambdapi proof assistant\, an implementation of the λΠ-calculus modulo rewriting. Lambdapi is a foundational proof assistant based on dependent type theory and rewriting rules\, intended to serve as a pivot for exchanging proofs between interactive proof assistants. We present a modular encoding of SMT logic and Alethe rules in Lambdapi\, covering core theories such as first-order reasoning and linear arithmetic. \nWe detail the reconstruction process\, which requires techniques such as proof by reflection and the elaboration of solver specific simplifications. Finally\, we evaluate our implementation on benchmark examples and demonstrate that Alethe proofs generated by modern SMT solvers can be efficiently and reliably reconstructed in Lambdapi\, paving the way toward portable and independently verifiable SMT proofs. \n  \n 
URL:https://www.loria.fr/event/soutenance-de-these-alessio_coltellacci/
LOCATION:C005\, Loria
CATEGORIES:Soutenance
END:VEVENT
END:VCALENDAR