Kaustuv Chaudhuri

See also:

• This list sorted in other ways
• Draft manuscripts

2024

• F. Al Wardani, K. Chaudhuri, and D. Miller. About Trust and Proof: An experimental framework for heterogeneous verification. The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II. LNCS 14871, pp. 162–183. 2024. ©Springer

2023

• F. Al Wardani, K. Chaudhuri, and D. Miller. Formal Reasoning using Distributed Assertions. International Symposium on Frontiers of Combining Systems (FroCoS). LNCS 14279, pp. 176–194. 2023. ©Springer
• F. Al Wardani, K. Chaudhuri, and D. Miller. Distributing and trusting proof checking: a preliminary report. INRIA. Technical Report HAL-03909741. 2023.

2022

• K. Chaudhuri, P. Donato, L. Massacci, and B. Werner. Certifying Proof-By-Linking. INRIA. Technical Report HAL-04317972. 2022.

2021

• K. Chaudhuri. Subformula Linking for Intuitionistic Logic with Application to Type Theory. International Confernce on Automated Deduction (CADE). LNCS 12699, pp. 200–216. 2021. ©Springer

2019

• K. Chaudhuri, J. Despeyroux, C. Olarte, and E. Pimentel. Hybrid linear logic, revisited. Mathematical Structures in Computer Science. 29(8), pp. 1151–1176. 2019.
• K. Chaudhuri, L. Lima, and G. Reis. Formalized Meta-Theory of Sequent Calculi for Substructural Logics. Theoretical Computer Science. 781, pp. 651–666. 2019.
• K. Chaudhuri, M. Manighetti, and D. Miller. A proof-theoretic approach to certifying skolemization. ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP). ACM Digital Library. April 2019. Supplementary code

2018

• K. Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. Mathematical Structures in Computer Science. 28(5). 2018.
• K. Chaudhuri. A Two-Level Logic Perspective on (Simultaneous) Substitutions. ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP-07), Los Angeles, USA. ACM Digital Library. January 2018.

2016

• 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, 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

2015

• 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.

2014

• 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.
• 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
• 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.

2013

• 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 and J. Despeyroux. A Hybrid Linear Logic for Constrained Transition Systems. Types for Proofs and Programs (TYPES-19), Toulouse, France. April 2013.

2012

• 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.

2011

• 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.

2010

• 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

2009

• K. Chaudhuri and J. Despeyroux. A Logic for Constrained Process Calculi with Applications to Molecular Biology. INRIA. Technical Report. May 2009.

2008

• 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

2006

• 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, 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

2005

• 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
• K. Chaudhuri and F. Pfenning. Focusing the Inverse Method for Linear Logic. Carnegie Mellon University. Technical Report CMU-CS-05-106. July 2005.

2003

• 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.