See also:
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. Encoding Additives Using Multiplicatives and Subexponentials. To appear in Mathematical Structures in Computer Science. Draft of August 2015. 2016.
- 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.