| 2026 | IJCAR | Automating Proof Search when Equality is a Logical Connective. | Kaustuv Chaudhuri, Arunava Gantait, Dale Miller |
| 2025 | TABLEAUX | Designing a Safe Forward Chaining Tactic Using Productive Proofs. | Kaustuv Chaudhuri, Arunava Gantait, Dale Miller |
| 2021 | CADE | Subformula Linking for Intuitionistic Logic with Application to Type Theory. | Kaustuv Chaudhuri |
| 2019 | CPP | A proof-theoretic approach to certifying skolemization. | Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller |
| 2018 | CPP | A two-level logic perspective on (simultaneous) substitutions. | Kaustuv Chaudhuri |
| 2016 | FOSSACS | Focused and Synthetic Nested Sequents. | Kaustuv Chaudhuri, Sonia Marin, Lutz Straburger |
| 2015 | CPP | A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. | Kaustuv Chaudhuri, Matteo Cimini, Dale Miller |
| 2015 | LPAR | An Adequate Compositional Encoding of Bigraph Structure in Linear Logic with Subexponentials. | Kaustuv Chaudhuri, Giselle Reis |
| 2015 | TABLEAUX | Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations. | Taus Brock-Nannestad, Kaustuv Chaudhuri |
| 2014 | CSL | Equality and fixpoints in the calculus of structures. | Kaustuv Chaudhuri, Nicolas Guenot |
| 2013 | ITP | Subformula Linking as an Interaction Method. | Kaustuv Chaudhuri |
| 2013 | PPDP | Reasoning about higher-order relational specifications. | Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur |
| 2012 | CPP | Compact Proof Certificates for Linear Logic. | Kaustuv Chaudhuri |
| 2012 | CSL | A Systematic Approach to Canonicity in the Classical Sequent Calculus. | Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller |
| 2011 | CSL | The Focused Calculus of Structures. | Kaustuv Chaudhuri, Nicolas Guenot, Lutz Straburger |
| 2010 | CADE | Verifying Safety Properties with the TLA+ Proof System. | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2010 | CSL | Classical and Intuitionistic Subexponential Logics Are Equally Expressive. | Kaustuv Chaudhuri |
| 2010 | ICTAC | The TLA | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2010 | LPAR | Magically Constraining the Inverse Method Using Dynamic Polarity Assignment. | Kaustuv Chaudhuri |
| 2008 | LPAR | Focusing Strategies in the Sequent Calculus of Synthetic Connectives. | Kaustuv Chaudhuri |
| 2008 | LPAR | A TLA+ Proof System. | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz |
| 2006 | CADE | A Logical Characterization of Forward and Backward Chaining in the Inverse Method. | Kaustuv Chaudhuri, Frank Pfenning, Greg Price |
| 2005 | CADE | A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. | Kaustuv Chaudhuri, Frank Pfenning |
| 2005 | CSL | Focusing the Inverse Method for Linear Logic. | Kaustuv Chaudhuri, Frank Pfenning |