The Bedwyr System for Model Checking over Syntactic Expressions. - David Baelde; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu (CADE, 2007)

Least and Greatest Fixed Points in Linear Logic. - David Baelde; Dale Miller 001 (LPAR, 2007)

On the Expressivity of Minimal Generic Quantification. - David Baelde (LFMTP@LICS, 2008)

On the Proof Theory of Regular Fixed Points. - David Baelde (TABLEAUX, 2009)

Focused Inductive Theorem Proving. - David Baelde; Dale Miller 001; Zachary Snow (IJCAR, 2010)

A meta-programming approach to realizing dependently typed logic programming. - Zachary Snow; David Baelde; Gopalan Nadathur (PPDP, 2010)

Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search - Zachary Snow; David Baelde; Gopalan Nadathur (CoRR, 2010)

Liquidsoap: A High-Level Programming Language for Multimedia Streaming. - David Baelde; Romain Beauxis; Samuel Mimram (SOFSEM, 2011)

Towards Provably Robust Watermarking. - David Baelde; Pierre Courtieu; David Gross-Amblard; Christine Paulin-Mohring (ITP, 2012)

Combining Deduction Modulo and Logics of Fixed-Point Definitions. - David Baelde; Gopalan Nadathur (LICS, 2012)

Least and Greatest Fixed Points in Linear Logic. - David Baelde (ACM Trans. Comput. Log., 2012)

A Reduced Semantics for Deciding Trace Equivalence Using Constraint Systems. - David Baelde; Stéphanie Delaune; Lucca Hirschi (POST, 2014)

Abella: A System for Reasoning about Relational Specifications. - David Baelde; Kaustuv Chaudhuri; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu; Yuting Wang 001 (J. Formaliz. Reason., 2014)

Partial Order Reduction for Security Protocols. - David Baelde; Stéphanie Delaune; Lucca Hirschi (CONCUR, 2015)

Least and Greatest Fixed Points in Ludics. - David Baelde; Amina Doumane; Alexis Saurin (CSL, 2015)

Infinitary Proof Theory: the Multiplicative Additive Case. - David Baelde; Amina Doumane; Alexis Saurin (CSL, 2016)

A Sequent Calculus for a Modal Logic on Finite Data Trees. - David Baelde; Simon Lunel; Sylvain Schmitz (CSL, 2016)

Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions. - Amina Doumane; David Baelde; Lucca Hirschi; Alexis Saurin (LICS, 2016)

A Method for Verifying Privacy-Type Properties: The Unbounded Case. - Lucca Hirschi; David Baelde; Stéphanie Delaune (IEEE Symposium on Security and Privacy, 2016)

Symbolic Verification of Privacy-Type Properties for Security Protocols with XOR. - David Baelde; Stéphanie Delaune; Ivan Gazeau; Steve Kremer (CSF, 2017)

Preface. - David Baelde; Arnaud Carayol; Ralph Matthes; Igor Walukiewicz (Fundam. Informaticae, 2017)

A Reduced Semantics for Deciding Trace Equivalence. - David Baelde; Stéphanie Delaune; Lucca Hirschi (Log. Methods Comput. Sci., 2017)

A Hypersequent Calculus with Clusters for Linear Frames. - David Baelde; Anthony Lick; Sylvain Schmitz (Advances in Modal Logic, 2018)

POR for Security Protocol Equivalences - Beyond Action-Determinism. - David Baelde; Stéphanie Delaune; Lucca Hirschi (ESORICS (1), 2018)

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. - David Baelde; Anthony Lick; Sylvain Schmitz (FSTTCS, 2018)

Decidable XPath Fragments in the Real World. - David Baelde; Anthony Lick; Sylvain Schmitz (PODS, 2019)

A method for unbounded verification of privacy-type properties. - Lucca Hirschi; David Baelde; Stéphanie Delaune (J. Comput. Secur., 2019)

A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday. - David Baelde; Amy P. Felty; Gopalan Nadathur; Alexis Saurin (Math. Struct. Comput. Sci., 2019)

A Method for Proving Unlinkability of Stateful Protocols. - David Baelde; Stéphanie Delaune; Solène Moreau (CSF, 2020)

Bouncing threads for infinitary and circular proofs. - David Baelde; Amina Doumane; Denis Kuperberg; Alexis Saurin (CoRR, 2020)

Contributions to the Verification of Cryptographic Protocols. (Contributions à la Vérification des Protocoles Cryptographiques). - David Baelde (2021)

An Interactive Prover for Protocol Verification in the Computational Model. - David Baelde; Stéphanie Delaune; Charlie Jacomme; Adrien Koutsos; Solène Moreau (SP, 2021)

Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant. - David Baelde; Stéphanie Delaune; Adrien Koutsos; Solène Moreau (CSF, 2022)

Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs. - David Baelde; Amina Doumane; Denis Kuperberg; Alexis Saurin (LICS, 2022)

Proving Unlinkability Using ProVerif Through Desynchronised Bi-Processes. - David Baelde; Alexandre Debant; Stéphanie Delaune (CSF, 2023)

A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. - David Baelde; Adrien Koutsos; Joseph Lallemand (LICS, 2023)

Foundations for Cryptographic Reductions in CCSA Logics. - David Baelde; Adrien Koutsos; Justine Sauvage (CCS, 2024)

A Probabilistic Logic for Concrete Security. - David Baelde; Caroline Fontaine; Adrien Koutsos; Guillaume Scerri; Théo Vignon (CSF, 2024)

The Squirrel Prover and its Logic. - David Baelde; Stéphanie Delaune; Charlie Jacomme; Adrien Koutsos; Joseph Lallemand (ACM SIGLOG News, 2024)

Propositional Logics of Overwhelming Truth. - Thibaut Antoine; David Baelde (CSL, 2025)