Date: Thursday, February 5 2026 – 13h00Place: A008Title: Thin spans and their modelling of rigid intersection types Thins spans were recently introduced as a quantitative, or proof-relevant, modelof programming languages based on spans of groupoids. As a model of linearlogic, they can be seen as an extension of the relational…
Date: Monday, January 12 2026 – 13h00Place: A008Title: Random Variate Generation with Formal Guarantees Standard software libraries for random variate generation are based on “Real-RAM” algorithms, which assume infinite precision. The “Real-RAM” assumption, however, is unrealistic as any software implementation must use only finite precision. As a result, existing libraries…
Date: Tuesday, December 9 2025 – 13h00Place: A008Title: Hardware-Software Co-Designs for Microarchitectural Security Microarchitectural optimizations, such as caches and speculative out-of-order execution, are essential for achieving high system performance. However, these same mechanisms also open the door to attacks that can undermine software-enforced security policies. The current gold standard for…
Date: Thursday, November 13 2025 – 13h00Place: A008Title: Breaking verifiability and vote privacy in CHVote CHVote is one of the two main electronic voting systems developed in the context of political elections in Switzerland, where the regulation requires a specific setting and specific trust assumptions. We show that actually, CHVote…
Date: Thursday, October 16 2025 – 13h00Place: A008Title: Formalizing Splitting in Isabelle/HOL In this talk, I will present a formalization in Isabelle/HOL of a framework for splitting, a theorem proving technique that extends saturation-based calculi with branching abilities. The framework preserves the completeness of the original calculus. This work focuse…
Date: Tuesday, March 18, 2025 – 13h00Place: B013 (Bob)Title: On reachability games played on graphs Nowadays computer systems are more and more involved in our everyday life. These systems become increasingly complex and interact either together or with humans. Moreover, in some situations bugs may have dramatic consequences. Thus, given…
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: 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…