The Cambium seminar series

Our seminar takes place at Inria Paris, usually on Friday mornings at 10:30am. The live talks are accessible online. They are not recorded.

To receive our announcements, please subscribe to our mailing list, which is archived.

A history of the past talks is available further down on this page.

Upcoming talks

Coming to Inria Paris

Inria Paris
2 rue Simone Iff (ou: 41 rue du Charolais)
75012 Paris

Archive of the previous talks

Here is a history of the previous talks:

12/04/2024: Irene Yoon, Modular and executable semantics for LLVM IR (announcement, slides)
29/03/2024: Aymeric Fromherz et Denis Merigoux, Formalizing Date Arithmetic and Statically Detecting Ambiguities for the Law (announcement, slides)
12/03/2024: Daan Leijen, The Functional Essence of Imperative Binary Search Trees (announcement, slides)
12/01/2024: Youngju Song, One stuttering simulation to rule them all? (announcement)
13/12/2023: Jérôme Vouillon, Wasm_of_ocaml: compiling OCaml bytecode to WebAssembly (announcement, slides)
01/12/2023: Sergei Stepanenko, The Essence of Generalized Algebraic Data Types (announcement, slides)
27/11/2023: Alexandre Moine, DisLog: A Separation Logic for Disentanglement (announcement, slides)
24/11/2023: Son Ho, Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification (announcement, slides)
17/11/2023: Samuel Vivien, How to prove that you need Cake? (announcement, slides)
20/10/2023: Samuel Hym et Nicolas Osborne, Ortac/QCheck-STM 0.1, Gospel 0.2 (announcement, slides)
16/10/2023: Clément Blaudeau, A Conceptual Framework for Safe Object Initialization (announcement, slides)
13/10/2023: Magnus O. Myreen, The CakeML Project: Verified Compilation, Verified Bootstrapping, Just-In-Time Compilation, and Applications (announcement, slides)
09/10/2023: Andrei Paskevich, Coma: an intermediate verification language with explicit abstraction barriers (announcement, slides)
18/09/2023: Arnaud Daby-Seesaram, Osiris: an Iris-based program logic for OCaml (announcement, slides)
11/09/2023: Armaël Guéneau, Melocoton: A Program Logic for Verified Interoperability Between OCaml and C (announcement, slides)
28/08/2023: Vincent Laviron et Pierre Chambart, Static analysis in Flambda 2 (announcement, slides)
26/06/2023: Vincent Laviron et Pierre Chambart, Flambda 2 (announcement, slides)
15/05/2023: Clément Allain, Verification of the Chase-Lev work-stealing deque (announcement, slides)
12/04/2023: Olivier Nicole et Fabrice Buoro, Runtime Data Race Detection in OCaml 5 with ThreadSanitizer (announcement, slides)
13/03/2023: François Pottier, Thunks and Debits in Iris with Time Credits (announcement, slides)
08/02/2023: Clément Blaudeau, Retrofitting OCaml modules: An Fω-inspired approach for a modern module system (announcement, slides)
16/01/2023: Léon Gondelman, Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols (announcement, slides)
14/12/2022: Stephen Dolan, Extending OCaml with locality (announcement, slides)
07/12/2022: Yannick Forster, Towards Verified Extraction from Coq to OCaml (announcement, slides)
05/12/2022: Nicolas Chappe, Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq (announcement, slides)
28/11/2022: Alexandre Moine, A High-Level Separation Logic for Heap Space under Garbage Collection (announcement, slides)
07/11/2022: Daniel Mercier, Towards a solution to the expression problem for compilers: strongly typed nano-passes (announcement, slides)
26/09/2022: Vincent Laporte, High-Assurance Cryptography in Jasmin & Spectre Security (announcement, slides)
19/09/2022: Guilhem Jaber, From game semantics to verification of OCaml programs (announcement, slides)
09/09/2022: Jonathan Ragan-Kelley, Safe & Productive High-Performance Programming with User-Schedulable Languages (announcement, slides)
07/06/2022: Kartik Nagar, Certified Mergeable Replicated Data Types (announcement, slides)
30/05/2022: Aurèle Barrière, Un compilateur Just-In-Time formellement vérifié générant dynamiquement du code natif (announcement, slides)
16/05/2022: Son Ho, Aeneas: Rust Verification by Functional Translation (announcement, slides)
25/04/2022: Glen Mével, Time debits in nested thunks: a proof of the banker's queue (announcement, slides)
14/03/2022: Dougal Mclaurin, Designing Dex: differentiation, parallelism, and index types (announcement, slides)
07/03/2022: Nathanaëlle Courant, Camlboot: debootstrapping the OCaml compiler (announcement, slides)
28/02/2022: Quentin Carbonneaux, Applying Formal Verification to Microkernel IPC at Meta (announcement)
24/01/2022: Albert Cohen, MLIR: Compiler Construction for Heterogeneity (announcement, slides)
13/12/2021: Frédéric Bour, Une analyse d'accessibilité rapide pour les automates LR(1) (announcement, slides)
06/12/2021: François Pottier, A separation logic for heap space under garbage collection (announcement, slides)
29/11/2021: Paulo Emílio de Vilhena, Hazel: a Separation Logic for effect handlers (announcement, slides)
15/11/2021: Paul Iannetta, Compiling pattern matching to in-place modifications (announcement, slides)
08/11/2021: Mário Pereira, Cameleer: a Deductive Verification Tool for OCaml (announcement, slides)
25/10/2021: Léo Stefanesco, Trillium: Unifying Refinement and Higher-Order Distributed Separation Logic (announcement, slides)
18/10/2021: Gabriel Radanne, Fast Indexing for Search by Types (announcement, slides)
11/10/2021: Clément Blaudeau, OCaml modules made simple: insights, formalizations and improvements (announcement, slides)
27/09/2021: Son Ho, Noise∗: A Library of Verified High-Performance Secure Channel Protocol Implementations (announcement, slides)
06/09/2021: Émile Trotignon, Efficient, typed LR parsers (announcement, slides)
30/08/2021: Alexandre Moine, Formalisation d’une structure de donnée transiente et de ses itérateurs en logique de séparation (announcement, slides)
28/06/2021: François Pottier, Strong automated testing of OCaml libraries (announcement, slides)
14/06/2021: Benoît Montagu, Trace-Based Control-Flow Analysis (announcement, slides)
29/03/2021: Quentin Ladeveze, Preuve de la propriété DRF-SC du modèle RC11 en Coq (announcement, slides)
01/02/2021: Théo Winterhalter, Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq (announcement, slides)
25/01/2021: Clément Pit-Claudel, Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs (announcement, slides)
11/01/2021: Arthur Charguéraud, Sémantique big-step pour langages non-déterministes (announcement, slides)
07/12/2020: Raphaël Rieu-Helft, Verification of efficient C arithmetic algorithms with Why3 (announcement, slides)
30/11/2020: Aïna Linn Georges, Mechanized Program Verification on a Capability Machine in the Presence of Untrusted Code (announcement, slides)
23/11/2020: Xavier Denis, Verification of Rust programs through prophecies and ownership (announcement, slides)
09/11/2020: Thierry Martinez, Type-safe type reflection for OCaml (announcement, slides)
02/11/2020: Nathanaël Courant, Big-step semantics for the strong λ-calculus (announcement, slides)
05/10/2020: Basile Clément, Compilation using additive annotations to achieve high-performance on GPUs (announcement, slides)
28/09/2020: Léo Stefanesco, Scala Step-by-step: Soundness for DOT with a logical relation in Iris (announcement, slides)
20/02/2020: Eelco Visser, Statix: Type Checkers from Declarative Specifications (announcement, page dédiée à cet exposé, slides)
17/02/2020: Thomas Letan, Implementing and Certifying Impure Computations with FreeSpec (announcement, slides)
03/02/2020: Gabriel Radanne, Kindly Bent to Free Us (announcement, slides)
27/01/2020: Sylvain Conchon, Parameterized Model Checking with a Partial Order Reduction Technique for the TSO Weak Memory Model (announcement, slides)
07/01/2020: Lionel Parreaux, Partial Graph Reduction: A New Optimization Technique for Higher-Order Programs (announcement, slides)
06/01/2020: Lionel Parreaux, Type-Safe Metaprogramming and Compilation Techniques for Optimizing High-Level Programs (announcement, slides)
18/12/2019: Yannick Zakowski, From representing recursive and impure programs in Coq to a modular formal semantics of LLVM IR (announcement, slides)
16/12/2019: Jan Hoffmann, Nomos: Resource-Aware Session Types for Programming Digital Contracts (announcement, slides)
02/12/2019: Christophe Chareton, Qbrick, a core development framework for certified quantum programming (announcement, slides)
25/11/2019: Francesco Zappa Nardelli, Fast and Reliable DWARF-based Stack Unwinding (announcement, slides)
18/11/2019: Glen Mével, Towards a separation logic for Multicore OCaml (announcement, slides)
04/11/2019: Denis Merigoux, Formal study of the French tax code's implementation (announcement, slides)
14/10/2019: Jonathan Protzenko, The EverCrypt verified cryptographic provider (announcement, slides)
03/10/2019: Tahina Ramananandro, EverParse: verified efficient parsing for transport data formats (announcement, slides)
30/09/2019: Yann Régis-Gianas, Towards certified incremental functional programming (announcement, slides)
23/09/2019: Jacques Garrigue, Proving tree algorithms for succinct data structures (announcement, slides)
29/07/2019: Aquinas Hobor, Certifying Graph-Manipulating C Programs via Localizations within Data Structures (announcement, slides)
08/07/2019: Cyril Six, Certified and modular postpass-scheduling for VLIW processors in CompCert (announcement, slides)
17/06/2019: Armaël Guéneau, Formal Proof and Analysis of an Incremental Cycle Detection Algorithm (announcement, slides)
12/06/2019: Victor Miraldo, Lessons from Structural Differencing (announcement, slides)
27/05/2019: Benedikt Becker, Ghost Code in Action: Automated Verification of a Symbolic Interpreter using Why3 (announcement, slides)
13/05/2019: Gabriel Scherer, A right-to-left type system for mutually-recursive value definitions (announcement, slides)
06/05/2019: Denis Merigoux, Formally Verified Cryptographic Web Applications in WebAssembly (announcement, slides)
29/04/2019: Marc Chevalier, Proving the security of an embedded operating system using abstract interpretation (announcement, slides)
15/04/2019: Léon Gondelman, Semi-Automated Reasoning About Non-Determinism in C Expressions (announcement, slides)
12/04/2019: Andrew Tolmach, Enforcing C-level security policies using machine-level tags (announcement, slides)
21/02/2019: Jeremy Siek, Toward Efficient Gradual Typing (announcement, slides)
18/02/2019: Victor Lanvin, Gradual Typing: A New Perspective (announcement, slides)
11/02/2019: Chantal Keller, SMTCoq: safe and efficient automation in Coq (announcement, slides)
28/01/2019: Simon Colin, Unboxing Mutually Recursive Type Definitions in OCaml (announcement, slides, article)
21/01/2019: Frédéric Bour, CAMLroot: revisiting the OCaml FFI (announcement, slides)
27/11/2018: Simon Castellan, Event structures and weak memory models (announcement, slides)
22/11/2018: Gabriel Radanne, Kindly Bent to Free Us (announcement, slides)
15/11/2018: Martin Abadi, On the Theory and Practice of Software that Learns (announcement)
15/10/2018: Kenji Maillard, An introduction to polarised L calculi (announcement, slides)
08/10/2018: Éric Tanter, Gradual Parametricity, Revisited (announcement, slides)
01/10/2018: Rodolphe Lepigre, Abstract Representation of Binders using the Bindlib Library (announcement, slides)
17/09/2018: Ramon Fernandez I Mir, Formal Verification of Data Layout Transformations (announcement, slides)
10/09/2018: Robbert Krebbers, MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic (announcement, slides)
03/09/2018: Damien Rouhling, Asymptotic Reasoning in Coq (announcement, slides)
09/07/2018: Pierre-Étienne Meunier, Pijul, un système de contrôle de versions distribué basé sur des patchs (announcement)
25/06/2018: Guillaume Munch-Maccagnoni, A proposal for a resource management model for OCaml (announcement, slides)
18/06/2018: Germán Andrés Delbianco, Concurrent Data Structures Linked in Time (announcement, slides)
06/06/2018: Brigitte Pientka, POPLMark Reloaded: Mechanizing Logical Relations Proofs (announcement, slides)
04/06/2018: Léo Stefanesco, An asynchronous soundness theorem for concurrent separation logic (announcement, slides)
22/05/2018: Gabriel Scherer, Tout réussir en répétant beaucoup (announcement, slides)
26/03/2018: Raphaël Cauderlier, A Verified Implementation of the Bounded List Container (announcement, slides)
12/03/2018: Ulysse Gérard, Functional programming with lambda-tree syntax (announcement, slides)
08/03/2018: Rodolphe Lepigre, The PML₂ Language: Proving Programs in ML (announcement, slides, exemples)
05/03/2018: Hugo Illous, A Relational Shape Abstract Domain (announcement, slides)
23/01/2018: Adam Chlipala, Kami: Modular Verification of Digital Hardware in Coq (announcement, slides)
18/12/2017: Jacques-Henri Jourdan, RustBelt: Securing the Foundations of the Rust Programming Language (announcement, slides)
04/12/2017: Keryan Didier, A compilation-like approach to real-time systems implementation (announcement, slides)
06/11/2017: Adrien Guatto, A Functional Language with Time Warps (announcement, slides)
23/10/2017: Gergö Barany, Liveness-Driven Random Program Generation (announcement, slides)
13/10/2017: Arthur Charguéraud, A new axiom-free implementation of CFML for the verification of imperative programs (announcement, slides)
27/09/2017: Amal Ahmed, Compositional Compiler Verification for a Multi-Language World (announcement, slides)
25/09/2017: Francesco Zappa Nardelli, Julia Subtyping Reconstructed (announcement, slides)
18/09/2017: Yann Régis-Gianas, Parsing POSIX [s]hell (announcement, slides)
18/09/2017: Nicolas Jeannerod, Formalising an intermediate language for POSIX shell (announcement, slides)
21/06/2017: Olin Shivers, No-Brainer CPS Conversion (announcement)
22/05/2017: François Pottier, Visitors Unchained (announcement, slides)
15/05/2017: Stefan Ciobaca, The RMT Tool for Rewriting Modulo Theories (announcement)
15/05/2017: Cyprien Mangin, Equations: a tool for programming with dependent types (announcement, slides, démo)
04/05/2017: Pierre-Marie Pédrot, An Effectful Way to Eliminate Addiction to Dependence (announcement, slides)
18/04/2017: Armaël Guéneau, Verified Characteristic Formulae for CakeML (announcement, slides)
10/04/2017: François Pottier, Temporary Read-Only Permissions for Separation Logic (Making Separation Logic's Small Axioms Smaller) (announcement, slides)
27/03/2017: Thomas Williams, Refactoring ML programs using ornaments (announcement, slides)
21/02/2017: Jacques Garrigue, Units in the OCaml typechecker (announcement, slides)
21/02/2017: Pierrick Couderc, Verification of OCaml typing proofs (announcement, slides)
06/02/2017: Gabriel Scherer, Full abstraction for language design (announcement, slides)
09/01/2017: Jacques-Henri Jourdan, Formalizing the essence of Rust's type system with the Iris separation logic (announcement, slides)
12/12/2016: Gabriel Radanne, Eliom: A core ML language for tierless Web programming (announcement, slides)
05/12/2016: Leo White, Effective programming: bringing algebraic effects and handlers to OCaml (announcement, slides)
14/11/2016: Gergö Barany, Hybrid Information Flow Analysis for Real-World C Code (announcement, slides)
08/11/2016: Thibaut Girka, Explaining Program Differences Using Oracles (announcement, slides)
17/10/2016: Jonathan Protzenko, Extracting from F* to C (announcement, slides)
26/09/2016: Mike Rainey, Theory and practice of granularity control (announcement, slides)
12/09/2016: Damien Pous, Coinduction all the way up (announcement, slides)
05/09/2016: Jean-Karim Zinzindohoué, Verified, efficient cryptography in F* (announcement, slides)
02/09/2016: Cătălin Hriţcu, Efficient Formally Secure Compilers to a Tagged Architecture (announcement, slides)
28/07/2016: Adrien Guatto, The Lazy Task Creation Machine (announcement)
11/07/2016: Clément Pit-Claudel, Trigger Selection Strategies to Stabilize Program Verifiers (announcement, slides)
04/07/2016: Arthur Charguéraud, Interactive execution of a formal semantics (announcement, slides)
17/06/2016: Ohad Kammar, No value restriction is needed for algebraic effects and handlers (announcement, slides)
30/05/2016: Martin Bodin, Pushing the Frame Rule into Abstract Interpretation (announcement, slides)
09/05/2016: Pierre-Évariste Dagand, From Sets to Bits in Coq (announcement, slides)
02/05/2016: Timothy Bourke, Towards the verified compilation of Lustre (announcement, slides)
11/04/2016: Clément Fumex, Specification and Proof of High-Level Functional Properties of Bit-Level Programs (announcement, slides)
31/03/2016: Sam Lindley, Liberating effects with rows and handlers (joint work with Daniel Hillerström) (announcement, slides)
29/03/2016: Filip Sieczkowski, Transfinite Step-indexing: Decoupling Concrete and Logical Steps (announcement, slides)
25/03/2016: Simon Castellan, Weak memory models using event structures (announcement, slides)
14/03/2016: Jacques Garrigue, Modular implicits for OCaml, how to assert success (announcement, slides)
07/03/2016: Mário Parreira-Pereira, A Modular Way to Reason About Iteration (announcement, slides)
29/02/2016: Matthias Puech, Contextual types for multi-staged programming (announcement, slides)
23/02/2016: Chung-Kil Hur, A Formal C Memory Model Supporting Integer-Pointer Casts (announcement, slides)
15/02/2016: François Pottier, Can an LR parser produce good syntax error messages? (announcement, slides)
08/02/2016: Filip Sieczkowski, DAG-Calculus: A Calculus for Parallel Computation (announcement, slides)
25/01/2016: Jonathan Protzenko, The global sequence protocol: a memory model for distributed systems (announcement, slides)
04/01/2016: Jean-Marie Madiot, Verified reasoning for concurrent C programs (announcement, slides)
07/12/2015: Frédéric Bour, Étendre Menhir pour l'analyse d'entrées partiellement incorrectes (announcement, slides)
21/09/2015: Kenji Maillard, An equational presentation of the local state monad (announcement, slides)
24/08/2015: Tahina Ramananandro, CompCertX: verified separate compilation for compositional verification of layered systems (announcement, slides)
29/06/2015: Filip Sieczkowski, ModuRes: a Coq Library for Modular Reasoning about Concurrent Higher-Order Imperative Programming Languages (announcement)
11/05/2015: Nhat Minh Lê, A parallel runtime system for Kahn process networks (announcement, slides)
27/04/2015: Beniamino Accattoli, Lambda Calculus, Invariance, and Useful Sharing (announcement)
30/03/2015: Gabriel Scherer, Which simple types have a unique inhabitant? (announcement, slides)
09/03/2015: Danko Ilik, Proof theoretic results concerning sum types (type isomorphism and canonical eta-long normal forms) and control operators (announcement, slides)
02/02/2015: Adrien Guatto, A Functional Synchronous Language with Integer Clocks (announcement, slides)
21/01/2015: Clément Pit-Claudel, Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant, and beyond (announcement)
01/12/2014: Pierre Courtieu, Travaux formels autour de la plateforme SPARK/Ada (announcement, slides)
17/11/2014: Emilio Jesús Gallego Arias, Approximate Relational Refinement Types with Applications to Verification of Differential Privacy and Mechanism Design (announcement, slides)
03/11/2014: Jean-Baptiste Jeannin, NetKAT: Semantic Foundations for Networks (announcement)
27/10/2014: Frédéric Bour, Tail-recursion modulo constructor experiment in OCaml (announcement, slides)
14/10/2014: Antoine Toubhans, Composite Abstract Domains for Shape Analysis (announcement, slides)
06/10/2014: Benjamin Pierce, Micro-Policies: A Framework for Tag-Based Security Monitors (announcement, slides)
19/06/2014: Stéphane Graham-Lengrand, Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture (announcement, slides)
16/06/2014: Guy Blelloch, Cost Models based on the Lambda Calculus (announcement, slides)
02/06/2014: Sigurd Schneider, Towards Verification of GVN-CSE on a Functional Intermediate Language with System Calls (announcement, slides)
14/04/2014: Tahina Ramananandro, Formal verification of stack-space bounds for compiled machine code (announcement, slides)
24/03/2014: Umut Acar, Self-Adjusting Computation: Practical Abstractions for Dynamic Software (announcement)
17/03/2014: Sigurd Schneider, Translating In and Out of a Functional Intermediate Language (announcement, slides)
10/03/2014: Gabriel Scherer, Maximal multi-focusing for sum equivalence: an introduction (announcement)
17/02/2014: Guillaume Allais, Generic Generalised de Bruijn indices (announcement)
10/02/2014: Pierre-Évariste Dagand, Ornaments: a calculus of data structures (announcement)
31/01/2014: Mariangiola Dezani, On the Preciseness of Subtyping in Session Types (announcement)
19/12/2013: Olin Shivers, 3CPS: An intermediate representation for a lambda-calculus compiler (announcement)
16/12/2013: Francesco Zappa Nardelli, Types you can count on: Like types for JavaScript (announcement)
09/12/2013: Mike Rainey, Theory of chunked sequences and applications to parallel graph algorithms (announcement)
20/11/2013: Justin Slepak, Array computation and statically typing shape-polymorphic languages (announcement)
11/09/2013: Jules Villard, Parametric completeness for separation theories (via hybrid logic) (announcement)
09/09/2013: Andrew Tolmach, A Verified Information-Flow Architecture for SAFE (announcement)
01/07/2013: Daniel de Rauglaudre, Théorème de Puiseux en OCaml et en Coq (announcement)
24/06/2013: Benoît Valiron, Towards a formal analysis of quantum algorithms: The programming language Quipper (announcement)
14/06/2013: Dan Ghica, Semantic foundations of heterogeneous compilation (announcement)
10/06/2013: Arthur Charguéraud, Verification of Concurrent Programs Targeting the x86-TSO Weak Memory Model (announcement)
13/05/2013: Guillaume Claret, Lightweight proof by reflection using a posteriori simulation of effectful computation (announcement)
25/02/2013: Hyeonseung Im, Towards a syntactic type system for recursive modules (announcement)
04/02/2013: Robert Krebbers, Separation Logic for Non-local Control Flow and Block Scope Variables (announcement)
18/01/2013: Gregory Malecha, Reflecting Modular Automation (announcement)
08/10/2012: Francesco Zappa Nardelli, Sound Optimisations in the C11/C++11 Memory Model and Applications to Compiler Testing (announcement)
07/05/2012: Beniamino Accatoli, Abella formalization of lambda-calculus residual theory (announcement)
06/04/2012: Tim Sheard, Funlogic: Mixing logic and functional programming styles (announcement)
02/04/2012: Sylvain Conchon, Cubicle: A Parallel SMT-based Model Checker for Parameterized Systems (announcement)
22/03/2012: Séverine Maingaud, Certification de programmes impératifs en logique dynamique: le cas du lambda-calcul avec références (announcement)
27/02/2012: Thibaut Balabonski, Les stratégies pleinement paresseuses (announcement)
12/01/2012: Conor McBride, First Class Datatypes and their Ornaments (announcement)
28/11/2011: Julien Cretin, On the Power of Coercion Abstraction (announcement)
07/11/2011: Arthur Charguéraud, Programming and scheduling parallel computations on multicore systems (announcement)
28/10/2011: Benoît Montagu, Preliminary design of the SAFE platform (announcement)
21/10/2011: Peter O'Hearn, Algebra, Logic, Locality, Concurrency (announcement)
10/10/2011: Pierre-Yves Strub, An introduction to F*, a new dependently typed language for secure distributed programming (announcement)
16/09/2011: Mike Dodds, Recovering Disjointness from Concurrent Sharing (announcement)
12/09/2011: Jacques-Henri Jourdan, Validating LR(1) parsers (announcement)
24/06/2011: Mike Hicks, Lightweight Monadic Programming in ML (announcement)
20/06/2011: Paolo Herms, Certification d'une chaîne de vérification déductive de programmes (announcement)
10/06/2011: Jacques Garrigue, Adding GADTs to OCaml: the direct approach (announcement)
06/06/2011: Matthias Puech, A logical framework for incremental type-checking (announcement)
31/05/2011: Jan Vitek, The Rise of Dynamic Languages (announcement)
16/05/2011: Bruno Barras, Formalisation d'un modèle ensembliste du Calcul des Constructions Inductives (announcement)
09/05/2011: Francesco Zappa Nardelli, Verifying Fence Elimination Optimisations (announcement)
02/05/2011: Alexandre Miquel, Une analyse calculatoire de la transformation de preuve par forcing (announcement)
11/04/2011: Jerôme Vouillon, Software component co-installability (announcement)
31/03/2011: Andrew Myers, Family-level extensibility mechanisms (announcement)
29/03/2011: Yitzhak Mandelbaum, Yakker: revisiting the challenges and opportunities of parsing research (announcement)
07/03/2011: Roberto Di Cosmo, Some research results in package-based distributions (announcement)
10/01/2011: David Pichardie, Certified Abstract Interpretation (announcement)
07/01/2011: Gabriel Dos Reis, Moving a Mainstream Programming Language in Modern Times (announcement)
03/01/2011: Serguei Lenglet, Expansion for universal quantifiers (announcement)
14/12/2010: Claudio Russo, A Scalable Joins Library (announcement)
06/12/2010: Martin Hofmann, Automatic amortised resource inference for class-based OOP (announcement)
15/11/2010: Mark Batty, Mathematizing C++ Concurrency (announcement)
25/10/2010: Matthieu Sozeau, Equations: A Dependent Pattern-Matching Compiler (announcement)
20/09/2010: Xavier Leroy, Nondeterministic expressions in C and how to compile them away (announcement)
16/09/2010: Julien Cretin, Matching Lenses: Alignment and View Update (announcement)
13/09/2010: Dana Xu, Probabilistic contracts for component-based design (announcement)
21/06/2010: Brigitte Pientka, Programming proofs with contexts and ... (announcement)
14/06/2010: Steve Zdancewic, Aura: A Programming Language with Authorization and Audit (announcement)
07/06/2010: Benjamin Grégoire, Formal certification of code based cryptographic proofs (announcement)
25/05/2010: Jade Alglave, Fences in Weak Memory Models (announcement)
18/05/2010: Lars Birkedal, Step-Indexed Kripke Models over Recursive Worlds (announcement)
03/05/2010: Nicolas Pouillard, A fresh look at programming with names and binders (announcement)
12/04/2010: Gustavo Petri, Operational semantics for relaxed memory models (announcement)
15/03/2010: Stéphane Lescuyer, Vérification formelle et utilisation d'un solveur SMT dans Coq (announcement)
08/03/2010: Benoît Montagu, Small-step extensional equivalence for singleton types (announcement)
22/02/2010: Arthur Charguéraud, Le combinateur de "points fixes optimaux" (announcement)
19/02/2010: Christophe Calves, Design and Implementation of Nominal Algorithms (announcement)
15/02/2010: Dana Xu, A Practical and Precise Inference and Specializer for Array Bound Checks Elimination (PEPM'08) (announcement)
09/02/2010: Tahina Ramananandro, A machine-checked formalization of concrete object layout for C++ multiple inheritance (announcement)
08/02/2010: Virgile Prevosto, Specification and Proof of C Programs with Frama-C and ACSL (announcement)
05/02/2010: Karthik Bhargavan, Scalable Verification of Security Protocol Code by Typechecking (announcement)
04/01/2010: Jules Villard, Tracking Heaps that Hop with Heap-Hop (announcement)
07/12/2009: Jules Villard, Tracking Heaps that Hop with Heap-Hop (announcement)
30/11/2009: Julien Signoles, Typage dynamique dans un contexte statique (announcement)
27/11/2009: Aarne Ranta, Compiling Natural Language: Recent Developments in GF (announcement)
23/11/2009: Dimitrios Vytiniotis, Towards a more expressive core language for GHC (announcement)
16/11/2009: Suresh Jagannathan, Serializability Enforcement for Concurrent ML (announcement)
09/11/2009: Jean-Christophe Filliâtre, Ocamlviz (announcement)
26/10/2009: François Pottier, De ML à F_omega avec sortes récursives: une traduction monadique bien typée (announcement)
19/10/2009: Thomas Ehrhard, Logique linéaire et lambda-calcul différentiels: formule de Taylor et concurrence (announcement)
16/10/2009: Brigitte Pientka, Beluga: programming with dependent types and higher-order data (announcement)
12/10/2009: Basile Starynkevitch, MELT - pourquoi et comment mettre un LISP dans le compilateur GCC... (announcement)
05/10/2009: Silvain Rideau, Allocation de registre validée (announcement)
14/09/2009: Mathieu Boespflug, Europa, un vérificateur de types pour le lambda-pi modulo (announcement)
25/06/2009: Alexandre Pilkiewicz, Destins et prédictions: une autre approche de la monotonie (announcement)
24/06/2009: Armando Solar-Lezama, The Sketching approach to practical synthesis (announcement)
08/06/2009: Damien Pous, Kleene et Kozen en Coq (announcement)
02/06/2009: Zaynah Dargaye, Vérification formelle de l'interaction avec un gestionnaire de mémoire (announcement)
25/05/2009: Francesco Zappa Nardelli, Like types (announcement)
18/05/2009: Nicolas Pouillard, Towards a Not-so-FreshML (announcement)
11/05/2009: Arthur Charguéraud, Tutoriel : Vérification Interactive de Programmes Fonctionnels (announcement)
20/04/2009: Benoît Valiron, Ordre supérieur en calcul quantique (announcement)
06/04/2009: Stéphane Glondu, Coq : extraction certifiée ou certification extraite ? (announcement)
30/03/2009: Dimitrios Vytiniotis, Complete and Decidable Type Inference for GADTs (announcement)
16/03/2009: Benoît Robillard, Vérification formelle et optimisation de l'allocation de registres (announcement)
03/03/2009: Andrew Gacek, A Framework for Specification, Prototyping, and Reasoning (announcement)
16/02/2009: Dana Xu, Static Contract Checking for Haskell (announcement)
09/02/2009: Boris Yakobowski, xMLF : un langage à la Church pour MLF (announcement)
12/01/2009: Nicolas Tabareau, Compiling Functional Types to Relational Specifications for Low Level Imperative Code (announcement)
16/12/2008: Fritz Henglein, Domain-specific languages for next-generation enterprise systems (announcement)
15/12/2008: Alain Frisch, OCaml chez LexiFi (announcement)
01/12/2008: Damien Doligez, Pointeurs faibles et hash-consing dans OCaml (announcement)
24/11/2008: Guillaume Melquiond, Certification de programmes numériques (announcement)
17/11/2008: Marc Pouzet, Le compilateur MiniLustre (announcement)
03/11/2008: Matthieu Sozeau, Classes de types de première classe (announcement)
27/10/2008: Benjamin Canou, O'Browser: Une machine virtuelle OCaml en JavaScript (announcement)
20/10/2008: Bob Harper, Focusing on Binding and Computation (announcement)
13/10/2008: Luc Maranget, De bons arbres de décision pour effectuer le filtrage de ML (announcement)
15/09/2008: Francesco Zappa Nardelli, The Semantics of x86 Multiprocessor Machine Code (announcement)
08/09/2008: Keiko Nakata, Towards less painful verification of the full correctness for C (announcement)
23/06/2008: Gabriel Dos Reis, OpenAxiom: A Categorial Platform for Scientific Computation (announcement)
13/06/2008: Jacques Garrigue, Proving OCaml's type system? (announcement)
09/06/2008: Alexandre Pilkiewicz, Boomerang, a Quotiented Bidirectional Programming Language for Ordered String Data (announcement)
22/05/2008: Jan Vitek, Programming Models for Concurrency and Real-time (announcement)
05/05/2008: Xavier Rival, Shape analysis based on inductive invariant checkers (announcement)
28/04/2008: Jean-Baptiste Tristan, Vérification formelle de validateurs de traduction: une étude de cas sur le lazy code motion (announcement)
17/03/2008: Sylvain Lebresne, Un système d'exceptions pour le Système F (announcement)
10/03/2008: Tom Reps, WYSINWYX: What You See Is Not What You eXecute (announcement)
04/03/2008: Noam Zeilberger, From AHOS to HOAS (duality for fun AND profit) (announcement)
03/03/2008: Nicolas Pouillard, Le versionnement distribué pour tous (announcement)
26/02/2008: Pierre Corbineau, A Declarative Language For The Coq Proof Assistant (announcement)
18/02/2008: Alexandre Miquel, Extraction de programme classique dans le Calcul des Constructions (announcement)
11/02/2008: Didier Rémy, Une explication moderne de MLF (announcement)
11/02/2008: Boris Yakobowski, Types et contraintes graphiques pour MLF (announcement)
28/01/2008: François Pottier, Effets cachés en style direct, ou: une règle d'anti-encadrement d'ordre supérieur (announcement)
21/01/2008: Boris Yakobowski, Le caractère ` à la rescousse (announcement)
14/12/2007: Olivier Danvy, On the equivalence between small-step and big-step abstract machines using lightweight fusion (announcement)
07/12/2007: Jean-Baptiste Tristan, Formal verification of translation validation (a 15-minute talk, plus ample time for discussion) (announcement)
07/12/2007: Arthur Charguéraud, Engineering Formal Metatheory (a 15-minute talk, plus ample time for discussion) (announcement)
30/11/2007: Simon Peyton Jones, Indexed type families for Haskell (announcement)
29/11/2007: Yann Régis-Gianas, Des types aux assertions logiques: preuve automatique ou assistée de propriétés sur les programmes fonctionnels (announcement)
23/11/2007: Benoît Razet, Les machines d'Eilenberg finies (announcement)
23/11/2007: Assia Mahboubi, Preuve formelle à grande échelle et réflexion à petite échelle (announcement)
09/11/2007: Nataliya Guts, A Formal Implementation of Value Commitment (announcement)
26/10/2007: Benoît Montagu, Vers des modules de première classe (announcement)
12/10/2007: Benjamin Werner, Normalisation par Evaluation et HOAS en Coq (announcement)
28/09/2007: Luc Maranget, Programmer en JoCaml (announcement)
21/09/2007: Xavier Leroy, Raisonner sur les programmes qui divergent: deux approches suivies dans la vérification du compilateur Compcert (announcement)
14/09/2007: Arthur Charguéraud, Traduction de programmes impératifs vers un langage fonctionnel à l'aide d'un système de types à base de capacités et de régions (announcement)
07/09/2007: David Baelde, Model-checking sur des théories avec liaison de variable (announcement)
29/08/2007: Andrew Tolmach, Proving Properties of Imperative Gallina Programs (announcement)
06/07/2007: Jean-Baptiste Tristan, Certification par Validation de Traduction (announcement)
02/07/2007: Jacques Garrigue, Union de variants abstraits (announcement)
18/06/2007: Andrew Appel, Threads Can Be Implemented As a Library (announcement)
15/06/2007: Keiko Nakata, Exploring a type system for recursive modules with applicative functors (announcement)
08/06/2007: Emmanuel Chailloux, Ocamil : Objective Caml sur .NET (announcement)
01/06/2007: Zaynah Dargaye, Transformation CPS certifiée (announcement)
24/05/2007: François Pottier, Wandering through linear types, capabilities, and regions (announcement)
16/05/2007: Nicolas Pouillard, Surcharge, une autre alternative ? (announcement)
14/05/2007: Bruno Bernardo, Certification de Programmes avec le Calcul des Constructions Implicites (announcement)
11/05/2007: Viktor Vafeiadis, A marriage of rely/guarantee and separation logic (announcement)
24/04/2007: Gabriel Dos Reis, Concepts: A structured approach to Generic Programming (announcement)
20/04/2007: Paul-André Mellies, Types polymorphes et récursifs dans un cadre opérationnel (announcement)
20/04/2007: Jerôme Vouillon, Une approche sémantique et modale du typage des langages machine (announcement)
12/04/2007: Yann Régis-Gianas, Mise en pratique de la logique de Hoare pour les programmes fonctionnels purs (announcement)
27/03/2007: Alexandre Miquel, Sémantiques dénotationnelles du calcul des constructions (announcement)
23/03/2007: Yannick Moy, Checking Memory Safety with Abstract Interpretation and Deductive Verification (announcement)
16/03/2007: Matthieu Sozeau, Program-ing in Coq (announcement)
16/02/2007: Ricardo Corin, Secure Implementations for Typed Session Abstractions (announcement)
16/02/2007: Berke Durak, Ocamlbuild, un outil pour la compilation automatique de projets OCaml (announcement)
12/02/2007: Francois Maurel, Types dynamiques en MLFi, une extension du langage OCaml (announcement)
09/02/2007: Julien Narboux, Quelques preuves typiques dans les langages avec lieurs en utilisant l'approche nominale (announcement)
26/01/2007: Zaynah Dargaye, Décurryfication certifiée (announcement)
24/01/2007: Mandana Vaziri, A data-centric approach to synchronization (announcement)
22/01/2007: Adam Chlipala, A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language (announcement)
24/11/2006: Boris Yakobowski, MLF avec des graphes: instance et unification (announcement)
10/11/2006: Sylvain Conchon, Ergo, un petit démonstrateur automatique dédié à la preuve de programmes (announcement)
09/10/2006: Daan Leijen, First-class polymorphism with existential types. (announcement)
29/09/2006: Dick Kieburtz, Programmed strategies for program verification (announcement)
14/09/2006: Arthur Charguéraud, Proofs with Binders - Working on the POPLMark Challenge (announcement)
27/06/2006: George Necula, Using Dependent Types for Low-Level Systems Programming (announcement)
01/06/2006: Matt Parkinson, Concurrent Separation Logic: a message from the front line (announcement)
05/05/2006: Alain Frisch, OCaml + XDuce = OCamlDuce (announcement)
28/04/2006: Julien Signoles, Obligations de preuve pour une extension de ML avec raffinement (announcement)
31/03/2006: Vincent Balat, Ocsigen : un peu d'air frais en programmation Web (announcement)
24/03/2006: Andrew Tolmach, A Principled Approach to Operating System Construction in Haskell (announcement)
22/03/2006: John O'Leary, Using a reflective functional language for hardware verification and theorem proving (announcement)
17/03/2006: Benjamin Pierce, The Weird World of Bi-Directional Programming (announcement)
24/02/2006: Albert Cohen, N-Synchronous Kahn Networks: Relaxing a Clock Calculus for Periodic Real-Time Systems through Sub-Typing (announcement)
17/02/2006: Sébastien Carlier, Expansion: Connecting Intersection Types, Type Inference, Principal Typings, Interaction Nets, etc. (announcement)
06/02/2006: Peter O'Hearn, Smallfoot: Modular Automatic Verification with Separation Logic (announcement)
03/02/2006: David Teller, Un pi-calcul pour parler des ressources et pour mieux les contrôler (announcement)
23/01/2006: Grégoire Henry, Typer la désérialisation sans sérialiser les types (announcement)
25/11/2005: Xavier Leroy, Vérification en Coq d'un back-end de compilateur (announcement)
22/11/2005: Jacques Garrigue, Types structurels, modules récursifs, et le problème des expressions (announcement)
19/10/2005: Ugo Montanari, Models and Languages for Service Oriented Computing (announcement)
07/10/2005: Massimo Merro, Formal Description and Verification of Distributed Consensus via Operational Semantics (announcement)
03/06/2005: George Necula, Randomized Algorithms for Program Analysis and Verification (announcement)
27/05/2005: Louis Mandel, Reactive ML, une extension réactive de Ocaml (announcement)
20/05/2005: Steve Kremer, *** ANNULÉ *** (announcement)
22/04/2005: Pierre Weis, Les types à relations (announcement)
04/03/2005: Fabio Mancinelli, A Resource-Aware Framework for Adaptable Java Applications (announcement)
23/02/2005: Jaap Boender, A tactic for proving primitive recursive formulas in Coq (announcement)
17/12/2004: Olin Shivers, Bottom-up beta reduction: uplinks and lambda-DAGs (announcement)
14/12/2004: Martin Odersky, Scalable Component Abstractions (announcement)
10/12/2004: Didier Le Botlan, An Overview of the Alice Programming Language: Open Programming, Constraint Programming, Concurrency and Distribution in a Strongly Typed Environment. (announcement)
08/12/2004: Olivier Tardieu, De la sémantique opérationnelle à la spécification formelle de compilateur L'exemple des boucles en Esterel (announcement)
03/12/2004: Cédric Fournet, Verifying Web Services Security (announcement)
03/12/2004: Barry Jay, Unifiable Subtyping (announcement)
26/11/2004: Jean-Christophe Filliâtre, Le foncteur sonne toujours deux fois (announcement)
19/11/2004: Alan Schmitt, Equivalences dans le Kell Calcul (announcement)
29/10/2004: Tom Chothia, Type-based Distributed Access Control (announcement)
22/10/2004: Peter Sewell, Acute: high-level programming language design for distributed computation (announcement)
18/10/2004: Didier Rémy, Inférence partielle dans le System F predicatif (announcement)
15/10/2004: Alain Frisch, Aperçu de CDuce (announcement)
08/10/2004: Basile Starynkevitch, Ocamljit - un traducteur Just In Time du bytecode Ocaml (announcement)
01/10/2004: Haruo Hosoya, Parametric Polymorphism for XML (announcement)
30/09/2004: David Monniaux, Analyse statique de code de grande taille par interprétation abstraite (announcement)
24/09/2004: Bernadette Charron-Bost, Reductions in Distributed Computing: Applications to Agreement Tasks (announcement)
07/05/2004: Benjamin Pierce, Native XML processing in a statically typed language (announcement)
19/12/2003: Davide Ancona, A Calculus for Symbolic Names Management (announcement)
27/11/2003: Aarne Ranta, GF: A Framework for Defining Grammars (announcement)
30/09/2003: Mark Shinwell, Fresh Objective Caml: new directions for the FreshML project (announcement)
01/09/2003: Jérôme Siméon, A Web Services Binding for XQuery (announcement)
11/07/2003: Gilles Peskine, Types abstraits et programmation distribuée (announcement)
27/06/2003: Olivier Tardieu, Instantaneous Termination in Pure Esterel (announcement)
20/06/2003: Stéphane Fechter et Virgile Prevosto, Matinee FOC: semantique et compilation. (announcement)
24/04/2003: Hayo Thielecke, From Control Effects to Typed Continuation Passing (announcement)
25/03/2003: Manuel Serrano, Scheme FairThreads (announcement)
14/03/2003: Haruo Hosoya, Principles of typed XML processing (announcement)
31/01/2003: Alberto Momigliano, An Hybrid Logical Framework (announcement)
17/01/2003: Dale Miller, Encryption as an Abstract Datatype (announcement)
14/01/2003: Dominique Cansell, La Balbulette (announcement)
19/12/2002: Simon Peyton Jones, Template meta-programming in Haskell (announcement)
19/12/2002: Atsushi Ohori, Register Allocation by Proof Transformation (announcement)
17/12/2002: Dick Kieburtz, Programatica -- Certifying properties of Haskell programs (announcement)
16/12/2002: Robert Harley, Algorithmes avancés pour l'arithmétique des courbes (soutenance) (announcement)
13/12/2002: Takakazu Satoh, Generalized division polynomials (announcement)
06/12/2002: Olivier Danvy, A lambda-revelation of the SECD machine (announcement)
04/12/2002: Leslie Lamport, Paxos Made Simple and Fast (announcement)
21/10/2002: Marino Miculan, Formal reasoning on HOAS specifications of nominal calculi using the Theory of Contexts (announcement)
11/10/2002: Jamie Gabbay, Fraenkel-Mostowski: semantics, logics, and languages for binding (announcement)
20/09/2002: Vladimiro Sassone, Communication Interference in Mobile Boxed Ambients (announcement)
12/09/2002: Cosimo Laneve, The Fusion Machine (announcement)
15/07/2002: Carlos Varela, A Language and Architecture for Distributed Computing over the Internet (announcement)
04/07/2002: Kwangkeun Yi, Monotonicity Analysis for lambda-Definable Functions over Lattices (announcement)
28/06/2002: Patrick Loiseleur, logiques temporelles pour les objets distribués (announcement)
21/06/2002: Eugenio Moggi, Higher-Order Types and Meta-Programming for Global Computing (announcement)
14/06/2002: Don Syme, Over the hump from C# to F#/Caml.NET (announcement)
26/04/2002: Sylvain Pogodalla, Réseaux de preuve et grammaires de types logiques (announcement)
29/03/2002: Tyng-Ruey Chuang, On Modular Transformation of Structural Content (announcement)
22/03/2002: Areski Nait Abdallah, The logic of partial information (announcement)
01/03/2002: Roberto Di Cosmo, Programmation fonctionnelle parallele: l'experience OcamlP3L (announcement)
21/12/2001: Cesar Munoz, Safety on New Air Traffic Technologies (from a Formal Methods perspective) (announcement)
05/10/2001: Jean-Marc Andreoli, Vers un paradigme de programmation fondé sur la construction de preuves en Logique Linéaire (announcement)
28/09/2001: Peter Sewell, The UDP Calculus: Rigorous Semantics for Real Networking (announcement)
14/09/2001: Jean-Marc Andreoli, Vers un paradigme de programmation fondé sur la construction de preuves en Logique Linéaire (announcement)
06/07/2001: K. Gopinath, Verification of Highly Available Local Leader Election Service in Timed Asynchronous Systems (announcement)
29/06/2001: Pierre-Louis Curien, Introduction à la ludique (announcement)
26/06/2001: Yves Bertot, Formalisation d'algorithmes d'enveloppe convexes (announcement)
22/06/2001: Gérard Boudol, Sur le typage de la récursion (announcement)
15/06/2001: Didier Rémy, Héritage dans le Join Calcul (announcement)
01/06/2001: Gilles Dowek, La détection et la résolution de conflits entre avions sans contrôleurs aériens et/ou sans pilotes : une approche géométrique (announcement)
18/05/2001: Pierre-Louis Curien, Introduction à la ludique (announcement)
11/05/2001: Andrew Tolmach, Modular Lazy Search Algorithms (announcement)
27/04/2001: Martijn Oostdijk, How to prove Prime(1234567891) in Coq (announcement)
25/04/2001: Martin Abadi, Reconciling Two Views of Cryptography (announcement)
20/04/2001: Marieke Huisman, The LOOP project: Reasoning about Java programs (announcement)
30/03/2001: Bruno Blanchet, Preuve de propriétés de secret dans des protocoles cryptographiques, par typage d'une part et par un vérificateur automatique d'autre part. (announcement)
16/03/2001: Luigi Liquori, The Rho-calculus (revisited): its syntax, semantics, and pragmatics (announcement)
09/03/2001: Pablo Argon, Formalisation et extraction en Coq du prouveur de l'outil Cadence-SMV (announcement)
07/03/2001: Luca Cardelli, Logical Properties of Name Restriction (announcement)
02/03/2001: Dilian Gurov, Verification of Erlang programs (announcement)
02/02/2001: Francois Pottier, Inférence de flots d'information pour ML (announcement)
26/01/2001: Eric Meijer, A general overview of Microsoft's .NET framework (announcement)
15/12/2000: Michel Authier, Utilisation de la cartographie pour la prise de connaissance rapide de base documentaire. (announcement)
14/11/2000: John Harrison, Verifying floating-point algorithms using formalized mathematics (announcement)
20/10/2000: Vassily Litvinov, Constraint-based Polymorphism in Cecil (announcement)
13/10/2000: Éric Deplagne, L'induction comme déduction modulo (announcement)
06/10/2000: Journée Cristal (announcement)
23/06/2000: Dominic Duggan, Recursive DLLs and Shared Libraries: A Type-Based Approach (announcement)
16/06/2000: Frédéric Prost, Dépendances et typage (announcement)
06/06/2000: Randy Pollack, Dependently Types Records for Representing Mathematical Structure (announcement)
26/05/2000: Dick Kieburtz, A Logic for Strategies (announcement)
26/05/2000: Laurent Théry, Une comparaison de Coq, Hol, Pvs: une preuve élémentaire de l'algorithme à clé public RSA (announcement)
24/05/2000 (exact date unknown): Jacek Chrzaszcz, Rewriting in modular setting (announcement)
24/05/2000 (exact date unknown): Daniel Hirschkoff, Enriching Coq with primitive records (announcement)
24/05/2000 (exact date unknown): Claudio Sacerdoti, Towards an Hypertextual Electronic Library of Formal Mathematical knowledge (announcement)
23/05/2000: Daniel Bonniot, Typage precis des multimethodes polymorphes dans ML-Sub (announcement)
05/05/2000: Eelco Visser, A Stratego Tutorial (announcement)
21/04/2000: Silvano Dal-Zilio, Modélisation des régions dans un pi-calcul avec groupe (announcement)
21/04/2000: Pierre-Louis Curien, Sur la dualité du calcul (announcement)
07/04/2000: Jean-Vincent Loddo, Alpha-Beta, un algorithme polyvalent pour jouer aux échecs et pour résoudre (efficacement) un but dans un programme logique (announcement)
24/03/2000: Alexandre Miquel, Les coulisses Caml d'un exposé interactif écrit en Caml (announcement)
17/03/2000: James Leifer, Bisimulation congruences by general magic (announcement)
14/03/2000: Journée Comparaison des Prouveurs (announcement)
11/02/2000: Michele Bugliesi, Typed Mobile Objects (announcement)
26/11/1999: Shen Wei Yu, Integrating theorem proving with model checking (announcement)
16/11/1999: Journée Math in Coq (announcement)
16/11/1999: Herman Geuvers, A constructive proof of the Fundamental Theorem of Algebra in Coq (announcement)
15/10/1999: Eve Coste-Maniere, Robotique médicale et programmation sure (announcement)
15/10/1999: Cristina Cornes, Théorie des types et Vérification de modèles (announcement)
01/10/1999: Cesar Munoz, Structural Embedding: Mechanization with Method (announcement)
21/09/1999: Chaochen Zhou, An Introduction to Duration Calculus (announcement)
10/09/1999: John Field, Equations as a Uniform Framework for Operational Semantics, Partial Evaluation, and Abstract Interpretation (announcement)
25/06/1999: Giuseppe Castagna, Le Seal-calcul: (encore) un nouveau calcul pour la mobilité (announcement)
18/05/1999: Peter Selinger, Control Categories and Duality (announcement)
22/03/1999: Trybulec Andrzej, The development of Mizar Mathematical Library (announcement)
19/02/1999: Jacques Garrigue, LablGL: une interface bien typée pour OpenGL (announcement)
15/01/1999: Alexandre Frey, Pratique de la reconstruction de types en ML-sub (announcement)
14/12/1998: Arvind, Synthesis Titre-long : Synthesis and Verification of Modern Microprocessors (announcement)
04/12/1998: Martin Strecker, Proof construction in type theory - the Typelab system (announcement)
13/11/1998: Hugo Herbelin, Une analyse de l'interaction dans le système F (et des conséquences) (announcement)
23/10/1998: Philippa Gardner, Graphical Descriptions of Interactive Systems (announcement)
16/10/1998: Catherine Dubois, Mécanisation des fonctions partielles (announcement)
13/10/1998: Yves Bertot, Vérification mécanique de la correction d'un compilateur en Théorie des Types (announcement)
02/10/1998: Pascal Brisset, Vers un vérifieur de byte-code Java certifié (announcement)
22/09/1998: David Basin, Structured Metatheory and Inductive Definitions (announcement)
19/06/1998: Georges Gonthier, Une gamme d'équivalences de processus (announcement)
12/06/1998: Gang Chen, Coercion Subtyping to the Calculus of Constructions (announcement)
20/03/1998: Chouhed Bouabana, Un langage à arité variable (announcement)
13/03/1998: Cédric Fournet, Implémentation sécurisée de programmes distribués. (announcement)
10/03/1998: Eva Rose, A tour of a Java subset operational-semantics and its proofs (announcement)
06/02/1998: Susumu Nisimura, Static Typing for Dynamic Messages (announcement)
28/11/1997: Jieh Hsiang, Some Fundamental Properties of Boolean Rings (announcement)
03/11/1997: Klaus Madlener, Relating Rewriting Techniques on Monoids and Rings: Congruences on Monoids and Ideals in Monoid Rings (announcement)
26/09/1997: Healfdene Goguen, An abstract formulation of memory management (announcement)
03/09/1997: Scott Alexander, The Active Bridge (announcement)