Kaustuv Chaudhuri

Publications (alternate views)

By type

Journals

  1. K. Chaudhuri. Encoding Additives Using Multiplicatives and Subexponentials. To appear in Mathematical Structures in Computer Science. Draft of August 2015. 2016.
  2. 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.
  3. 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
  4. 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. K. Chaudhuri, M. Manighetti, and D. Miller. A proof-theoretic approach to certifying skolemization. Draft manuscript. Submitted. April 2018. Supplementary code
  2. 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.
  3. 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.
  4. 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.
  5. 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
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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
  11. 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.
  12. 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
  13. 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
  14. K. Chaudhuri. Compact Proof Certificates for Linear Logic. Certified Programs and Proofs (CPP-02), Kyoto, Japan. LNCS 7679, pp. 208–223. December 2012. ©Springer
  15. 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.
  16. 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.
  17. 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
  18. 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
  19. 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
  20. 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
  21. 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
  22. 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
  23. 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
  24. 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. 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.
  2. 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.
  3. 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.
  4. 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.
  5. 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
  6. 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.
  7. 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.
  8. 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.
  9. 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.
  10. 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.
  11. 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.
  12. K. Chaudhuri. Undecidability of Multiplicative Subexponential Logic. 3rd International Workshop on Linearity, Vienna, Austria (reviews). EPTCS v.176, pp. 1–8. July 2014.
  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. 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
  15. 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.
  16. 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
  17. 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
  18. K. Chaudhuri. Compact Proof Certificates for Linear Logic. Certified Programs and Proofs (CPP-02), Kyoto, Japan. LNCS 7679, pp. 208–223. December 2012. ©Springer
  19. 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.
  20. 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.
  21. 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
  22. 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
  23. 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
  24. 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
  25. 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.
  26. 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
  27. 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
  28. 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
  29. 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
  30. 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
  31. 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. K. Chaudhuri, M. Manighetti, and D. Miller. A proof-theoretic approach to certifying skolemization. Draft manuscript. Submitted. April 2018. Supplementary code
  2. K. Chaudhuri. Encoding Additives Using Multiplicatives and Subexponentials. To appear in Mathematical Structures in Computer Science. Draft of August 2015. 2016.
  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

Kaustuv Chaudhuri
LSV, ENS Cachan, France
Inria Saclay, France
Carnegie Mellon University (Qatar), Doha, Qatar
University of Colorado, USA
Indiana University, USA
Inria Sophia-Antipolis and I3S, France
INRIA Rocquencourt, France
Rockwell Collins, USA
DemTech @ IT University, Copenhagen, Denmark
Viena University of Technology, Austria
Microsoft Research, USA
L. Lima Federal University of Paraíba, Brazil
M. Manighetti Inria & LIX/École polytechnique, France
Inria Saclay & LIX/École polytechnique, France
Inria Lorraine, France
Inria Saclay & LIX/École Polytechnique, France
University of Minnesota, USA
Carnegie Mellon University, USA
G. Price
INRIA
CNRS, France
Princeton University, USA
University of Minnesota, USA
Inria Saclay & LIX/École polytechnique, France
Nanyang Technological University, Singapore
University of Minnesota, USA