### By type

#### Journals

- K. Chaudhuri.
*Encoding Additives Using Multiplicatives and Subexponentials*. To appear in*Mathematical Structures in Computer Science*. Draft of August 2015. 2016. -
D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, and Y. Wang.
*Abella: A System for Reasoning about Relational Specifications*. Journal of Formalized Reasoning. Volume 7(2). 2014. - K. Chaudhuri, S. Hetzl, and D. Miller.
*A multi-focused proof system isomorphic to expansion proofs*. Journal of Logic and Computation. 26 (2), pp. 577–603. 2016. ©Oxford University Press - K. Chaudhuri, F. Pfenning, and G. Price.
*A Logical Characterization of Forward and Backward Chaining in the Inverse Method*. Journal of Automated Reasoning, 40(2–3), pp. 133–177. 2008. ©Springer

#### Conferences

- K. Chaudhuri, S. Marin, and L. Straßburger.
*Modular Focused Proof Systems for Intuitionistic Modal Logics*. Formal Structures for Computation and Deduction (FSCD-1), Porto, Porgugal. LIPIcs v.52. June 2016. - K. Chaudhuri, S. Marin, and L. Straßburger.
*Focused and Synthetic Nested Sequents*. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS-19), Eindhoven, Netherlands. LNCS 9634. April 2016. ©Springer.*The official proceedings version is full of mistakes introduced by Springer’s “copyeditors” and we strongly recommend reading the authors’ versions instead.*Technical report with full proofs. - K. Chaudhuri and G. Reis.
*An adequate compositional encoding of bigraph structure in linear logic with subexponentials*. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Suva, Fiji. LNCS 9450, pp. 146–161. November 2015. ©Springer -
T. Brock-Nannestad and K. Chaudhuri.
*Disproving Using the Inverse Method by Iterated Refinement of Finite Approximations*. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-24), Wrocław, Poland. LNCS 9323, pp. 153–168. September 2015. ©Springer. See the associated theorem prover, Mætning. -
Y. Wang and K. Chaudhuri.
*A Proof-Theoretic Characterization of Independence in Type Theory*. International Conference on Typed Lambda Calculi and Applications (TLCA-13), Warsaw, Poland. LIPIcs v.38, pp. 332–346. July 2015. This paper has a dedicated web-page. - K. Chaudhuri, M. Cimini, and D. Miller.
*A lightweight formalization of the meta-theory of bisimulation-up-to*. ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP-4), Mumbai, India. ACM Proceedings, pp. 157–166. January 2015. This paper has a dedicated web-page. -
M. Southern and K. Chaudhuri.
*A Two-Level Logic Approach to Reasoning about Typed Specification Languages*. International Conference on Foundation[*sic*] of Software Technology and Theoretical Computer Science (FSTTCS-34), New Delhi, India. LIPIcs, v.29, pp. 557–569. December 2014. This paper has a dedicated web-page. - K. Chaudhuri and N. Guenot.
*Equality and Fixpoints in the Calculus of Structures*. Joint meeting of the 23rd*Computer Science Logic*and the 29th*Logic in Computer Science*(CSL-LICS), Vienna, Austria (reviews). ACM Proceedings. July 2014. ©ACM -
J. Despeyroux and K. Chaudhuri.
*A Hybrid Linear Logic for Constrained Transition Systems*. International Conference on Types for Proofs and Programs (TYPES-19), Toulouse, France. LIPIcs v.26, pp. 150–168. 2014. -
Y. Wang, K. Chaudhuri, A. Gacek, and G. Nadathur.
*Reasoning about Higher-Order Relational Specifications*. Symposium on Principles and Practice of Declarative Programming (PPDP-15), Madrid, Spain. ACM Proceedings, pp. 157–168. September 2013. ©ACM - K. Chaudhuri.
*Subformula Linking as an Interaction Method*. Conference on Interactive Theorem Proving (ITP-04), Rennes, France. LNCS 7998, pp. 386–401. July 2013. ©Springer - K. Chaudhuri.
*Compact Proof Certificates for Linear Logic*. Certified Programs and Proofs (CPP-02), Kyoto, Japan. LNCS 7679, pp. 208–223. December 2012. ©Springer - K. Chaudhuri, S. Hetzl, and D. Miller.
*A Systematic Approach to Canonicity in the Classical Sequent Calculus*. Computer Science Logic (CSL-21), Fontainebleau, France. LIPICS v.16, pp. 183–197. September 2012. - K. Chaudhuri, N. Guenot, and L. Straßburger.
*The Focused Calculus of Structures*. Computer Science Logic (CSL-20), Bergen, Norway. LIPICS v.12, pp. 159–173. September 2011. - K. Chaudhuri.
*Magically Constraining the Inverse Method Using Dynamic Polarity Assignment*. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Yogyakarta, Indonesia. LNCS 6397, pp. 202–216. October 2010. ©Springer - K. Chaudhuri.
*Classical and Intuitionistic Subexponential Logics are Equally Expressive*. Computer Science Logic (CSL-19), Brno, Czech Republic. LNCS 6247, pp. 185–199. August 2010. ©Springer - K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz.
*Verifying Safety Properties with the TLA+ Proof System*. International Joint Conference on Automated Reasonign (IJCAR-5), Edinburgh, UK. LNCS 6173, pp. 142–148. July 2010. ©Springer - K. Chaudhuri.
*Focusing Strategies in the Sequent Calculus of Synthetic Connectives*. Logic for Programming, Artificial Intelligence and Reasoning (LPAR-15), Doha, Qatar. LNCS 5330, pp. 467–481. November 2008. ©Springer - K. Chaudhuri, D. Miller, and A. Saurin.
*Canonical Sequent Proofs via Multi-Focusing*. IFIP International Conference on Theoretical Computer Science (TCS-5), Milan, Italy. IFIP 273, pp. 383–396. September 2008. ©Springer - K. Chaudhuri, F. Pfenning, and G. Price.
*A Logical Characterization of Forward and Backward Chaining in the Inverse Method*. International Joint Conference on Automated Reasoning (IJCAR-3), Seattle, USA. LNCS 4130, pp. 97–111. August 2006. ©Springer - K. Chaudhuri and F. Pfenning.
*Focusing the Inverse Method for Linear Logic*. Computer Science Logic (CSL-14), Oxford, UK. LNCS 3634, pp. 200–215. August 2005. ©Springer - K. Chaudhuri and F. Pfenning.
*A Focusing Inverse Method Theorem Prover for First-Order Linear Logic*. Conference on Automated Deduction (CADE-20), Tallinn, Estonia. LNCS 3632, pp. 69–83. July 2005. ©Springer

#### Workshops

- K. Chaudhuri, L. Lima, and G. Reis.
*Formalized Meta-Theory of Sequent Calculi for Substructural Logics*. Workshop on Logical and Semantic Frameworks, with Applications (LSFA-11), Porto, Portugal. Draft of April 2016. June 2016. -
I. Cervesato and K. Chaudhuri.
*Proceedings of the 10th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)*. EPTCS v.185. August 2015. -
O. Savary-Bélanger and K. Chaudhuri.
*Automatically Deriving Schematic Theorems for Dynamic Contexts*. Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), Vienna, Austria. ACM Proceedings. July 2014. - K. Chaudhuri.
*Undecidability of Multiplicative Subexponential Logic*. 3rd International Workshop on Linearity, Vienna, Austria (reviews). EPTCS v.176, pp. 1–8. July 2014. - K. Chaudhuri and J. Despeyroux.
*A Hybrid Linear Logic for Constrained Transition Systems*. Types for Proofs and Programs (TYPES-19), Toulouse, France. April 2013. - K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz.
*A TLA+ Proof System*. Workshop on Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), Doha, Quatar. CEUR Workshop Proceedings 418, pp. 17–37. November 2008.

#### Invited

- K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz.
*The TLA+ Proof System: Building a Heterogeneous Verification Platform*. International Colloquium on Theoretical Aspects of Computing (ICTAC-7), Natal, Brazil. LNCS 6256, p. 44. September 2010. ©Springer

### By Evaluation

#### Refereed

- K. Chaudhuri, L. Lima, and G. Reis.
*Formalized Meta-Theory of Sequent Calculi for Substructural Logics*. Workshop on Logical and Semantic Frameworks, with Applications (LSFA-11), Porto, Portugal. Draft of April 2016. June 2016. - K. Chaudhuri, S. Marin, and L. Straßburger.
*Modular Focused Proof Systems for Intuitionistic Modal Logics*. Formal Structures for Computation and Deduction (FSCD-1), Porto, Porgugal. LIPIcs v.52. June 2016. - K. Chaudhuri, S. Marin, and L. Straßburger.
*Focused and Synthetic Nested Sequents*. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS-19), Eindhoven, Netherlands. LNCS 9634. April 2016. ©Springer.*The official proceedings version is full of mistakes introduced by Springer’s “copyeditors” and we strongly recommend reading the authors’ versions instead.*Technical report with full proofs. - K. Chaudhuri and G. Reis.
*An adequate compositional encoding of bigraph structure in linear logic with subexponentials*. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-20), Suva, Fiji. LNCS 9450, pp. 146–161. November 2015. ©Springer -
I. Cervesato and K. Chaudhuri.
*Proceedings of the 10th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)*. EPTCS v.185. August 2015. -
T. Brock-Nannestad and K. Chaudhuri.
*Disproving Using the Inverse Method by Iterated Refinement of Finite Approximations*. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX-24), Wrocław, Poland. LNCS 9323, pp. 153–168. September 2015. ©Springer. See the associated theorem prover, Mætning. -
Y. Wang and K. Chaudhuri.
*A Proof-Theoretic Characterization of Independence in Type Theory*. International Conference on Typed Lambda Calculi and Applications (TLCA-13), Warsaw, Poland. LIPIcs v.38, pp. 332–346. July 2015. This paper has a dedicated web-page. - K. Chaudhuri, M. Cimini, and D. Miller.
*A lightweight formalization of the meta-theory of bisimulation-up-to*. ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP-4), Mumbai, India. ACM Proceedings, pp. 157–166. January 2015. This paper has a dedicated web-page. -
M. Southern and K. Chaudhuri.
*A Two-Level Logic Approach to Reasoning about Typed Specification Languages*. International Conference on Foundation[*sic*] of Software Technology and Theoretical Computer Science (FSTTCS-34), New Delhi, India. LIPIcs, v.29, pp. 557–569. December 2014. This paper has a dedicated web-page. -
O. Savary-Bélanger and K. Chaudhuri.
*Automatically Deriving Schematic Theorems for Dynamic Contexts*. Logical Frameworks and Meta-languages: Theory and Practice (LFMTP), Vienna, Austria. ACM Proceedings. July 2014. - K. Chaudhuri.
*Undecidability of Multiplicative Subexponential Logic*. 3rd International Workshop on Linearity, Vienna, Austria (reviews). EPTCS v.176, pp. 1–8. July 2014. - K. Chaudhuri and N. Guenot.
*Equality and Fixpoints in the Calculus of Structures*. Joint meeting of the 23rd*Computer Science Logic*and the 29th*Logic in Computer Science*(CSL-LICS), Vienna, Austria (reviews). ACM Proceedings. July 2014. ©ACM - K. Chaudhuri, S. Hetzl, and D. Miller.
*A multi-focused proof system isomorphic to expansion proofs*. Journal of Logic and Computation. 26 (2), pp. 577–603. 2016. ©Oxford University Press -
J. Despeyroux and K. Chaudhuri.
*A Hybrid Linear Logic for Constrained Transition Systems*. International Conference on Types for Proofs and Programs (TYPES-19), Toulouse, France. LIPIcs v.26, pp. 150–168. 2014. -
Y. Wang, K. Chaudhuri, A. Gacek, and G. Nadathur.
*Reasoning about Higher-Order Relational Specifications*. Symposium on Principles and Practice of Declarative Programming (PPDP-15), Madrid, Spain. ACM Proceedings, pp. 157–168. September 2013. ©ACM - K. Chaudhuri.
*Subformula Linking as an Interaction Method*. Conference on Interactive Theorem Proving (ITP-04), Rennes, France. LNCS 7998, pp. 386–401. July 2013. ©Springer - K. Chaudhuri.
*Compact Proof Certificates for Linear Logic*. Certified Programs and Proofs (CPP-02), Kyoto, Japan. LNCS 7679, pp. 208–223. December 2012. ©Springer - K. Chaudhuri, S. Hetzl, and D. Miller.
*A Systematic Approach to Canonicity in the Classical Sequent Calculus*. Computer Science Logic (CSL-21), Fontainebleau, France. LIPICS v.16, pp. 183–197. September 2012. - K. Chaudhuri, N. Guenot, and L. Straßburger.
*The Focused Calculus of Structures*. Computer Science Logic (CSL-20), Bergen, Norway. LIPICS v.12, pp. 159–173. September 2011. - K. Chaudhuri.
*Magically Constraining the Inverse Method Using Dynamic Polarity Assignment*. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Yogyakarta, Indonesia. LNCS 6397, pp. 202–216. October 2010. ©Springer - K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz.
*The TLA+ Proof System: Building a Heterogeneous Verification Platform*. International Colloquium on Theoretical Aspects of Computing (ICTAC-7), Natal, Brazil. LNCS 6256, p. 44. September 2010. ©Springer - K. Chaudhuri.
*Classical and Intuitionistic Subexponential Logics are Equally Expressive*. Computer Science Logic (CSL-19), Brno, Czech Republic. LNCS 6247, pp. 185–199. August 2010. ©Springer - K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz.
*Verifying Safety Properties with the TLA+ Proof System*. International Joint Conference on Automated Reasonign (IJCAR-5), Edinburgh, UK. LNCS 6173, pp. 142–148. July 2010. ©Springer - K. Chaudhuri, D. Doligez, L. Lamport, and S. Merz.
*A TLA+ Proof System*. Workshop on Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), Doha, Quatar. CEUR Workshop Proceedings 418, pp. 17–37. November 2008. - K. Chaudhuri.
*Focusing Strategies in the Sequent Calculus of Synthetic Connectives*. Logic for Programming, Artificial Intelligence and Reasoning (LPAR-15), Doha, Qatar. LNCS 5330, pp. 467–481. November 2008. ©Springer - K. Chaudhuri, D. Miller, and A. Saurin.
*Canonical Sequent Proofs via Multi-Focusing*. IFIP International Conference on Theoretical Computer Science (TCS-5), Milan, Italy. IFIP 273, pp. 383–396. September 2008. ©Springer - K. Chaudhuri, F. Pfenning, and G. Price.
*A Logical Characterization of Forward and Backward Chaining in the Inverse Method*. Journal of Automated Reasoning, 40(2–3), pp. 133–177. 2008. ©Springer - K. Chaudhuri, F. Pfenning, and G. Price.
*A Logical Characterization of Forward and Backward Chaining in the Inverse Method*. International Joint Conference on Automated Reasoning (IJCAR-3), Seattle, USA. LNCS 4130, pp. 97–111. August 2006. ©Springer - K. Chaudhuri and F. Pfenning.
*Focusing the Inverse Method for Linear Logic*. Computer Science Logic (CSL-14), Oxford, UK. LNCS 3634, pp. 200–215. August 2005. ©Springer - K. Chaudhuri and F. Pfenning.
*A Focusing Inverse Method Theorem Prover for First-Order Linear Logic*. Conference on Automated Deduction (CADE-20), Tallinn, Estonia. LNCS 3632, pp. 69–83. July 2005. ©Springer

#### Not Refereed

- K. Chaudhuri.
*Encoding Additives Using Multiplicatives and Subexponentials*. To appear in*Mathematical Structures in Computer Science*. Draft of August 2015. 2016. -
D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, and Y. Wang.
*Abella: A System for Reasoning about Relational Specifications*. Journal of Formalized Reasoning. Volume 7(2). 2014. - K. Chaudhuri and J. Despeyroux.
*A Hybrid Linear Logic for Constrained Transition Systems*. Types for Proofs and Programs (TYPES-19), Toulouse, France. April 2013. - K. Chaudhuri and J. Despeyroux.
*A Logic for Constrained Process Calculi with Applications to Molecular Biology*. INRIA. Technical Report. May 2009. - K. Chaudhuri.
*The Focused Inverse Method for Linear Logic*. Carnegie Mellon University. Ph.D. thesis, available as technical report CMU-CS-06-162. December 2006. - K. Chaudhuri and F. Pfenning.
*Focusing the Inverse Method for Linear Logic*. Carnegie Mellon University. Technical Report CMU-CS-05-106. July 2005. - K. Chaudhuri.
*The Inverse Method for Intuitionistic Linear Logic (The Propositional Fragment)*. Carnegie Mellon University. Technical Report CMU-CS-03-140. November 2003. -
B.-Y. E. Chang, K. Chaudhuri, and F. Pfenning.
*A Judgemental Analysis of Linear Logic*. Carnegie Mellon University. Technical Report CMU-CS-03-131R. April 2003.

### Coauthors

D. Baelde | LSV, ENS Cachan, France |

T. Brock-Nannestad | Inria Saclay, France |

I. Cervesato | Carnegie Mellon University (Qatar), Doha, Qatar |

B.-Y. E. Chang | University of Colorado, USA |

M. Cimini | Indiana University, USA |

J. Despeyroux | Inria Sophia-Antipolis and I3S, France |

D. Doligez | INRIA Rocquencourt, France |

A. Gacek | Rockwell Collins, USA |

N. Guenot | DemTech @ IT University, Copenhagen, Denmark |

S. Hetzl | Viena University of Technology, Austria |

L. Lamport | Microsoft Research, USA |

L. Lima | Federal University of Paraíba, Brazil |

S. Marin | Inria Saclay & LIX/École polytechnique, France |

S. Merz | Inria Lorraine, France |

D. Miller | Inria Saclay & LIX/École Polytechnique, France |

G. Nadathur | University of Minnesota, USA |

F. Pfenning | Carnegie Mellon University, USA |

G. Price | |

G. Reis | INRIA |

A. Saurin | CNRS, France |

O. Savary-Bélanger | Princeton University, USA |

M. Southern | University of Minnesota, USA |

L. Straßburger | Inria Saclay & LIX/École polytechnique, France |

A. Tiu | Nanyang Technological University, Singapore |

Y. Wang | University of Minnesota, USA |