Date: Tuesday, April 1st 2025 – 13h00Place: A008Title: Infinite Algebraic Proofs Lors du séminaire du département du 7 janvier, Alejandro a montré comment étendre le fragment multiplicatif-additif de la logique linéaire intuitionniste au cas quantique.En particulier, il a montré comment représenter, à travers un système de preuve et par Curry-Howard,…
Date: May 6, 2025Place: A008Chair: Charlie Jacomme and Engel Lefaucheaux Program coming soon.
Date: Tuesday, February 20th 2025 – 13h00Place: A008Title: The Lisa Proof Assistant & Efficient and Predictable Tools with Orthologic-Based Reasoning In this talk, I will present my research efforts in improving and developing automated reasoning tools. First, I will present Lisa, a proof assistant based on Set Theory that I…
Date: Tuesday, February 4th 2025 – 13h00Place: A008Title: The Squirrel Prover The Squirrel Prover is a proof assistant dedicated to cryptographic protocols. It relies on a higher-order logic following the computationally complete symbolic attacker approach. It thus provides guarantees in the computational model. In this talk, we will introduce the…
Date: Tuesday, Janary 7th 2025 – 13h00Place: A008Title: Sup, Sum, and Scalars: In Linear Logic and in Non-Linear Logic In [1], we introduced a new connective, called “sup”, to intuitionistic propositional logic to model information erasure, non-reversibility, and non-determinism, as observed in quantum measurement, among other contexts. This connective features…
Date: Tuesday, March 4th 2025 – 13h00Place: A008Title: A scalable framework for backward bounded static symbolic executionMany programs (e.g. malware) hide their behavior by using obfuscations such as opaque predicates.Automatic methods have been developed to detect such obfuscations. In this presentation, we will focus on static symbolic backward bounded execution,…
Date: Tuesday, December 3rd 2024 – 13h00Place: A008Title: The Automation of Mathematics in Practice This presentation provides an overview of automated systems actively used in proving mathematical theorems, focusing on the practical successes achieved by SAT solvers, first-order theorem provers, and interactive theorem provers.Additionally, we present our progress towards improving…
Date: Tuesday, November 3rd 2024 – 13h00Place: A008Title: SC-TPTP : étendre le format TPTP pour les preuves basées sur les séquents
Date: Monday, February 19th 2024 – 13h00Place: B013 (Bob)Title: Communicating automata and k-synchronizability Distributed systems are ubiquitous and their implementation is complex and error-prone. In order to check for errors, they can be modeled as systems of communicating automata, where each automaton represents the behavior of an element of the…
Date: Thursday, March 14th 2024 – 13h00Place: visioTitle: Conception d’un prouveur automatique basé sur les tableaux analytiques et production de preuves vérifiables La déduction automatique est l’utilisation de programmes informatique afin d’automatiquement prouver des théorèmes mathématiques. Elle trouve son intérêt dans la détection de bogues au sein de systèmes critiques…
