David Baelde

According to our database, David Baelde authored at least 36 papers between 2007 and 2023.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2023

A Higher-Order Indistinguishability Logic for Cryptographic Reasoning.

David Baelde, Adrien Koutsos, Joseph Lallemand

LICS, 2023

Proving Unlinkability Using ProVerif Through Desynchronised Bi-Processes.

David Baelde, Alexandre Debant, Stéphanie Delaune

Proceedings of the 36th IEEE Computer Security Foundations Symposium, 2023

2022

Bouncing Threads for Circular and Non-Wellfounded Proofs: Towards Compositionality with Circular Proofs.

David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin

Proceedings of the LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2, 2022

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

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

2021

An Interactive Prover for Protocol Verification in the Computational Model.

David Baelde, Stéphanie Delaune, Charlie Jacomme, Adrien Koutsos, Solène Moreau

Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

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

David Baelde

, 2021

2020

Bouncing threads for infinitary and circular proofs.

David Baelde, Amina Doumane, Denis Kuperberg, Alexis Saurin

CoRR, 2020

A Method for Proving Unlinkability of Stateful Protocols.

David Baelde, Stéphanie Delaune, Solène Moreau

Proceedings of the 33rd IEEE Computer Security Foundations Symposium, 2020

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 unbounded verification of privacy-type properties.

Lucca Hirschi, David Baelde, Stéphanie Delaune

J. Comput. Secur., 2019

Decidable XPath Fragments in the Real World.

David Baelde, Anthony Lick, Sylvain Schmitz

Proceedings of the 38th ACM SIGMOD-SIGACT-SIGAI Symposium on Principles of Database Systems, 2019

2018

A Hypersequent Calculus with Clusters for Tense Logic over Ordinals.

David Baelde, Anthony Lick, Sylvain Schmitz

Proceedings of the 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, 2018

POR for Security Protocol Equivalences - Beyond Action-Determinism.

David Baelde, Stéphanie Delaune, Lucca Hirschi

Proceedings of the Computer Security, 2018

A Hypersequent Calculus with Clusters for Linear Frames.

David Baelde, Anthony Lick, Sylvain Schmitz

Proceedings of the Advances in Modal Logic 12, 2018

2017

A Reduced Semantics for Deciding Trace Equivalence.

David Baelde, Stéphanie Delaune, Lucca Hirschi

Log. Methods Comput. Sci., 2017

Preface.

David Baelde, Arnaud Carayol, Ralph Matthes, Igor Walukiewicz

Fundam. Informaticae, 2017

Symbolic Verification of Privacy-Type Properties for Security Protocols with XOR.

David Baelde, Stéphanie Delaune, Ivan Gazeau, Steve Kremer

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016

A Method for Verifying Privacy-Type Properties: The Unbounded Case.

Lucca Hirschi, David Baelde, Stéphanie Delaune

Proceedings of the IEEE Symposium on Security and Privacy, 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

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

A Sequent Calculus for a Modal Logic on Finite Data Trees.

David Baelde, Simon Lunel, Sylvain Schmitz

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

Infinitary Proof Theory: the Multiplicative Additive Case.

David Baelde, Amina Doumane, Alexis Saurin

Proceedings of the 25th EACSL Annual Conference on Computer Science Logic, 2016

2015

Least and Greatest Fixed Points in Ludics.

David Baelde, Amina Doumane, Alexis Saurin

Proceedings of the 24th EACSL Annual Conference on Computer Science Logic, 2015

Partial Order Reduction for Security Protocols.

David Baelde, Stéphanie Delaune, Lucca Hirschi

Proceedings of the 26th International Conference on Concurrency Theory, 2015

2014

Abella: A System for Reasoning about Relational Specifications.

David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang

J. Formaliz. Reason., 2014

A Reduced Semantics for Deciding Trace Equivalence Using Constraint Systems.

David Baelde, Stéphanie Delaune, Lucca Hirschi

Proceedings of the Principles of Security and Trust - Third International Conference, 2014

2012

Least and Greatest Fixed Points in Linear Logic.

David Baelde

ACM Trans. Comput. Log., 2012

Combining Deduction Modulo and Logics of Fixed-Point Definitions.

David Baelde, Gopalan Nadathur

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Towards Provably Robust Watermarking.

David Baelde, Pierre Courtieu, David Gross-Amblard, Christine Paulin-Mohring

Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

2011

Liquidsoap: A High-Level Programming Language for Multimedia Streaming.

David Baelde, Romain Beauxis, Samuel Mimram

Proceedings of the SOFSEM 2011: Theory and Practice of Computer Science, 2011

2010

Redundancies in Dependently Typed Lambda Calculi and Their Relevance to Proof Search

Zachary Snow, David Baelde, Gopalan Nadathur

CoRR, 2010

A meta-programming approach to realizing dependently typed logic programming.

Zachary Snow, David Baelde, Gopalan Nadathur

Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2010

Focused Inductive Theorem Proving.

David Baelde, Dale Miller, Zachary Snow

Proceedings of the Automated Reasoning, 5th International Joint Conference, 2010

2009

On the Proof Theory of Regular Fixed Points.

David Baelde

Proceedings of the Automated Reasoning with Analytic Tableaux and Related Methods, 2009

2008

On the Expressivity of Minimal Generic Quantification.

David Baelde

Proceedings of the International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, 2008

2007

Least and Greatest Fixed Points in Linear Logic.

David Baelde, Dale Miller

Proceedings of the Logic for Programming, 2007

The Bedwyr System for Model Checking over Syntactic Expressions.

David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu

Proceedings of the Automated Deduction, 2007