Publications

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. DOI HAL

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. DOI HAL
F. Al Wardani, K. Chaudhuri and D. Miller. Distributing and trusting proof checking a preliminary report. Technical Report. 2023. HAL

2022

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

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. DOI HAL

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. DOI HAL
K. Chaudhuri, L. Lima and G. Reis. Formalized Meta-Theory of Sequent Calculi for Substructural Logics. Theoretical Computer Science. 781, pp. 651–666. 2019. DOI HAL
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, pp. 78–90. April 2019. DOI HAL

2018

K. Chaudhuri, U. Gérard and D. Miller. Computation-as-Deduction in Abella: work in progress. International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP-13). Technical Report. 2018. HAL
K. Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. Mathematical Structures in Computer Science. 28(5), pp. 651–666. 2018. DOI HAL
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. DOI

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

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

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. DOI
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. DOI
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. DOI
K. Chaudhuri. Undecidability of Multiplicative Subexponential Logic. 3rd International Workshop on Linearity, Vienna, Austria. EPTCS v.176, pp. 1–8. July 2014. DOI
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. ACM Proceedings. July 2014. DOI
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. DOI

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. DOI
K. Chaudhuri. Subformula Linking as an Interaction Method. Conference on Interactive Theorem Proving (ITP-04), Rennes, France. LNCS 7998, pp. 386–401. July 2013. DOI
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. DOI
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. DOI

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

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

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

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

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