| 2025 | CSL | Propositional Logics of Overwhelming Truth. | Thibaut Antoine, David Baelde |
| 2024 | CCS | Foundations for Cryptographic Reductions in CCSA Logics. | David Baelde, Adrien Koutsos, Justine Sauvage |
| 2023 | LICS | A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. | David Baelde, Adrien Koutsos, Joseph Lallemand |
| 2022 | LICS | Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs. | David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin |
| 2021 | SP | An Interactive Prover for Protocol Verification in the Computational Model. | David Baelde, Stphanie Delaune, Charlie Jacomme, Adrien Koutsos, Solne Moreau |
| 2019 | PODS | Decidable XPath Fragments in the Real World. | David Baelde, Anthony Lick, Sylvain Schmitz |
| 2018 | AiML | A Hypersequent Calculus with Clusters for Linear Frames. | David Baelde, Anthony Lick, Sylvain Schmitz |
| 2018 | ESORICS | POR for Security Protocol Equivalences - Beyond Action-Determinism. | David Baelde, Stphanie Delaune, Lucca Hirschi |
| 2016 | CSL | Infinitary Proof Theory: the Multiplicative Additive Case. | David Baelde, Amina Doumane, Alexis Saurin |
| 2016 | CSL | A Sequent Calculus for a Modal Logic on Finite Data Trees. | David Baelde, Simon Lunel, Sylvain Schmitz |
| 2016 | LICS | Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Bchi inclusions. | Amina Doumane, David Baelde, Lucca Hirschi, Alexis Saurin |
| 2016 | SP | A Method for Verifying Privacy-Type Properties: The Unbounded Case. | Lucca Hirschi, David Baelde, Stphanie Delaune |
| 2015 | CONCUR | Partial Order Reduction for Security Protocols. | David Baelde, Stphanie Delaune, Lucca Hirschi |
| 2015 | CSL | Least and Greatest Fixed Points in Ludics. | David Baelde, Amina Doumane, Alexis Saurin |
| 2012 | ITP | Towards Provably Robust Watermarking. | David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring |
| 2012 | LICS | Combining Deduction Modulo and Logics of Fixed-Point Definitions. | David Baelde, Gopalan Nadathur |
| 2011 | SOFSEM | Liquidsoap: A High-Level Programming Language for Multimedia Streaming. | David Baelde, Romain Beauxis, Samuel Mimram |
| 2010 | CADE | Focused Inductive Theorem Proving. | David Baelde, Dale Miller, Zachary Snow |
| 2010 | PPDP | A meta-programming approach to realizing dependently typed logic programming. | Zachary Snow, David Baelde, Gopalan Nadathur |
| 2009 | TABLEAUX | On the Proof Theory of Regular Fixed Points. | David Baelde |
| 2007 | CADE | The Bedwyr System for Model Checking over Syntactic Expressions. | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu |
| 2007 | LPAR | Least and Greatest Fixed Points in Linear Logic. | David Baelde, Dale Miller |