David Baelde

Publication Activity (10 Years)

Years Active: 2007-2023
Publications (10 Years): 26

Top Topics

Automated Design

Theorem Proving

Sequent Calculus

Top Venues

Publications

David Baelde, Alexandre Debant, Stéphanie Delaune
Proving Unlinkability Using ProVerif Through Desynchronised Bi-Processes. CSF (2023)
David Baelde, Adrien Koutsos, Joseph Lallemand
A Higher-Order Indistinguishability Logic for Cryptographic Reasoning. LICS (2023)
David Baelde, Stéphanie Delaune, Adrien Koutsos, Solène Moreau
Cracking the Stateful Nut: Computational Proofs of Stateful Security Protocols using the Squirrel Proof Assistant. CSF (2022)
David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin
Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs. LICS (2022)
David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Solène Moreau
An Interactive Prover for Protocol Verification in the Computational Model. IEEE Symposium on Security and Privacy (2021)
David Baelde, Stéphanie Delaune, Solène Moreau
A Method for Proving Unlinkability of Stateful Protocols. CSF (2020)
David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin
Bouncing threads for infinitary and circular proofs. CoRR (2020)
Lucca Hirschi, David Baelde, Stéphanie Delaune
A method for unbounded verification of privacy-type properties. J. Comput. Secur. 27 (3) (2019)
David Baelde, Amy P. Felty, Gopalan Nadathur, Alexis Saurin
A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller's 60th birthday. Math. Struct. Comput. Sci. 29 (8) (2019)
David Baelde, Anthony Lick, Sylvain Schmitz
Decidable XPath Fragments in the Real World. PODS (2019)
David Baelde, Stéphanie Delaune, Lucca Hirschi
POR for Security Protocol Equivalences - Beyond Action-Determinism. ESORICS (1) (2018)
David Baelde, Anthony Lick, Sylvain Schmitz
A Hypersequent Calculus with Clusters for Linear Frames. Advances in Modal Logic (2018)
David Baelde, Anthony Lick, Sylvain Schmitz
A Hypersequent Calculus with Clusters for Tense Logic over Ordinals. FSTTCS (2018)
David Baelde, Stéphanie Delaune, Lucca Hirschi
POR for Security Protocol Equivalences: Beyond Action-Determinism. CoRR (2018)
David Baelde, Stéphanie Delaune, Lucca Hirschi
A Reduced Semantics for Deciding Trace Equivalence. CoRR (2017)
David Baelde, Stéphanie Delaune, Lucca Hirschi
A Reduced Semantics for Deciding Trace Equivalence. Log. Methods Comput. Sci. 13 (2) (2017)
David Baelde, Stéphanie Delaune, Ivan Gazeau, Steve Kremer
Symbolic Verification of Privacy-Type Properties for Security Protocols with XOR. CSF (2017)
Lucca Hirschi, David Baelde, Stéphanie Delaune
A method for unbounded verification of privacy-type properties. CoRR (2017)
David Baelde, Arnaud Carayol, Ralph Matthes, Igor Walukiewicz
Preface. Fundam. Informaticae 150 (3-4) (2017)
David Baelde, Simon Lunel, Sylvain Schmitz
A Sequent Calculus for a Modal Logic on Finite Data Trees. CSL (2016)
David Baelde, Amina Doumane, Alexis Saurin
Infinitary Proof Theory: the Multiplicative Additive Case. CSL (2016)
Amina Doumane, David Baelde, Lucca Hirschi, Alexis Saurin
Towards Completeness via Proof Search in the Linear Time μ-calculus: The case of Büchi inclusions. LICS (2016)
Lucca Hirschi, David Baelde, Stéphanie Delaune
A Method for Verifying Privacy-Type Properties: The Unbounded Case. IEEE Symposium on Security and Privacy (2016)
David Baelde, Stéphanie Delaune, Lucca Hirschi
Partial Order Reduction for Security Protocols. CoRR (2015)
David Baelde, Stéphanie Delaune, Lucca Hirschi
Partial Order Reduction for Security Protocols. CONCUR (2015)
David Baelde, Amina Doumane, Alexis Saurin
Least and Greatest Fixed Points in Ludics. CSL (2015)
David Baelde, Stéphanie Delaune, Lucca Hirschi
A reduced semantics for deciding trace equivalence using constraint systems. CoRR (2014)
David Baelde, Stéphanie Delaune, Lucca Hirschi
A Reduced Semantics for Deciding Trace Equivalence Using Constraint Systems. POST (2014)
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
Abella: A System for Reasoning about Relational Specifications. J. Formaliz. Reason. 7 (2) (2014)
David Baelde
Least and Greatest Fixed Points in Linear Logic. ACM Trans. Comput. Log. 13 (1) (2012)
David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring
Towards Provably Robust Watermarking. ITP (2012)
David Baelde, Gopalan Nadathur
Combining Deduction Modulo and Logics of Fixed-Point Definitions CoRR (2012)
David Baelde, Gopalan Nadathur
Combining Deduction Modulo and Logics of Fixed-Point Definitions. LICS (2012)
David Baelde, Romain Beauxis, Samuel Mimram
Liquidsoap: A High-Level Programming Language for Multimedia Streaming. SOFSEM (2011)
David Baelde, Romain Beauxis, Samuel Mimram
Liquidsoap: a High-Level Programming Language for Multimedia Streaming CoRR (2011)
David Baelde, Dale Miller, Zachary Snow
Focused Inductive Theorem Proving. IJCAR (2010)
Zachary Snow, David Baelde, Gopalan Nadathur
A Meta-Programming Approach to Realizing Dependently Typed Logic Programming CoRR (2010)
Zachary Snow, David Baelde, Gopalan Nadathur
A meta-programming approach to realizing dependently typed logic programming. PPDP (2010)
Zachary Snow, David Baelde, Gopalan Nadathur
Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search CoRR (2010)
David Baelde
Least and greatest fixed points in linear logic CoRR (2009)
David Baelde
On the Expressivity of Minimal Generic Quantification. Electron. Notes Theor. Comput. Sci. 228 (2009)
David Baelde
On the Proof Theory of Regular Fixed Points. TABLEAUX (2009)
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
The Bedwyr system for model checking over syntactic expressions CoRR (2007)
David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu
The Bedwyr System for Model Checking over Syntactic Expressions. CADE (2007)
David Baelde, Dale Miller
Least and Greatest Fixed Points in Linear Logic. LPAR (2007)