Kaustuv Chaudhuri

By type

Journals

1. K. Chaudhuri, J. Despeyroux, C. Olarte, and E. Pimentel. Hybrid linear logic, revisited. Mathematical Structures in Computer Science. 29(8), pp. 1151–1176. 2019.
2. K. Chaudhuri, L. Lima, and G. Reis. Formalized Meta-Theory of Sequent Calculi for Substructural Logics. Theoretical Computer Science. 781, pp. 651–666. 2019.
3. K. Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. Mathematical Structures in Computer Science. 28(5). 2018.
4. 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.
5. 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
6. 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

1. 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
2. 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
3. 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
4. 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
5. 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.
6. 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.
7. 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.
8. 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
9. 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.
10. 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.
11. 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.
12. 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.
13. 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
14. 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.
15. 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
16. 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
17. K. Chaudhuri. Compact Proof Certificates for Linear Logic. Certified Programs and Proofs (CPP-02), Kyoto, Japan. LNCS 7679, pp. 208–223. December 2012. ©Springer
18. 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.
19. 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.
20. 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
21. 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
22. 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
23. 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
24. 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
25. 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
26. 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
27. 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

1. 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.
2. 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.
3. 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.
4. K. Chaudhuri. Undecidability of Multiplicative Subexponential Logic. 3rd International Workshop on Linearity, Vienna, Austria (reviews). EPTCS v.176, pp. 1–8. July 2014.
5. K. Chaudhuri and J. Despeyroux. A Hybrid Linear Logic for Constrained Transition Systems. Types for Proofs and Programs (TYPES-19), Toulouse, France. April 2013.
6. 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

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

1. 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
2. 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
3. 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
4. K. Chaudhuri, J. Despeyroux, C. Olarte, and E. Pimentel. Hybrid linear logic, revisited. Mathematical Structures in Computer Science. 29(8), pp. 1151–1176. 2019.
5. K. Chaudhuri, L. Lima, and G. Reis. Formalized Meta-Theory of Sequent Calculi for Substructural Logics. Theoretical Computer Science. 781, pp. 651–666. 2019.
6. 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
7. K. Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. Mathematical Structures in Computer Science. 28(5). 2018.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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
13. 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.
14. 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.
15. 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.
16. 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.
17. 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.
18. 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.
19. K. Chaudhuri. Undecidability of Multiplicative Subexponential Logic. 3rd International Workshop on Linearity, Vienna, Austria (reviews). EPTCS v.176, pp. 1–8. July 2014.
20. 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
21. 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
22. 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.
23. 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
24. 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
25. K. Chaudhuri. Compact Proof Certificates for Linear Logic. Certified Programs and Proofs (CPP-02), Kyoto, Japan. LNCS 7679, pp. 208–223. December 2012. ©Springer
26. 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.
27. 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.
28. 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
29. 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
30. 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
31. 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
32. 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.
33. 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
34. 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
35. 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
36. 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
37. 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
38. 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

1. F. Al Wardani, K. Chaudhuri, and D. Miller. Distributing and trusting proof checking: a preliminary report. INRIA. Technical Report HAL-03909741. 2023.
2. K. Chaudhuri, P. Donato, L. Massacci, and B. Werner. Certifying Proof-By-Linking. INRIA. Technical Report HAL-04317972. 2022.
3. 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.
4. K. Chaudhuri and J. Despeyroux. A Hybrid Linear Logic for Constrained Transition Systems. Types for Proofs and Programs (TYPES-19), Toulouse, France. April 2013.
5. K. Chaudhuri and J. Despeyroux. A Logic for Constrained Process Calculi with Applications to Molecular Biology. INRIA. Technical Report. May 2009.
6. 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.
7. K. Chaudhuri and F. Pfenning. Focusing the Inverse Method for Linear Logic. Carnegie Mellon University. Technical Report CMU-CS-05-106. July 2005.
8. K. Chaudhuri. The Inverse Method for Intuitionistic Linear Logic (The Propositional Fragment). Carnegie Mellon University. Technical Report CMU-CS-03-140. November 2003.
9. 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