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
48 rue Barrault
75013 Paris

Archive of the previous talks

Here is a history of the previous talks:

08/11/2024: Vincent Laviron, Compiling recursion in OCaml (announcement, slides)
14/10/2024: Denis Carnier, Type Inference Logics (announcement, slides)
09/10/2024: Pedro Abreu, A Translation of GADTs in OCaml into Coq (announcement, slides)
04/10/2024: Antonin Reitz, StarMalloc: Verifying a Modern, Hardened Memory Allocator (announcement, slides)
27/09/2024: Gabriel Scherer, Pattern-matching on mutable values: danger! (announcement, slides)
13/09/2024: Jacques Garrigue, Mechanized monadic equational reasoning for ML references (announcement, slides)
26/08/2024: Rudi Schneider, Slotted E-Graphs - E-Graphs with Name Binding (announcement, slides)
10/06/2024: Guillaume Bertholon, A practical Separation Logic typechecker (announcement, slides)
24/05/2024: Irene Yoon, Velliris: A Relational Program Logic for LLVM IR (announcement, slides)
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)