Number of documents

27

Kaustuv Chaudhuri


Research Interests


Journal articles2 documents

  • Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Multi-Focused Proof System Isomorphic to Expansion Proofs. Journal of Logic and Computation, Oxford University Press (OUP), 2014. <hal-00937056>
  • David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, et al.. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning, ASDD-AlmaDL, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. <10.6092/issn.1972-5787/4650>. <hal-01102709>

Conference papers20 documents

  • Kaustuv Chaudhuri, Matteo Cimini, Dale Miller. A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. Xavier Leroy and Alwen Tiu. 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), Jan 2015, Mumbai, India. ACM Proceedings, 2014, <http://cpp2015.inria.fr>. <10.1145/2676724.2693170>. <hal-01091524>
  • Kaustuv Chaudhuri, Giselle Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. Martin Davis; Ansgar Fehnker; Annabelle McIver; Andrei Voronkov. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. Springer-Verlag Berlin Heidelberg, 9450, pp.146--161, Lecture Notes in Computer Science. <10.1007/978-3-662-48899-7_11>. <hal-01208362>
  • Taus Brock-Nannestad, Kaustuv Chaudhuri. Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations. Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wrocław, Poland. <http://tableaux2015.ii.uni.wroc.pl/>. <10.1007/978-3-319-24312-2_11>. <hal-01222592>
  • Yuting Wang, Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. Thorsten Altenkirch. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Jul 2015, Warsaw, Poland. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 38, pp.332--346, Leibniz International Proceedings in Informatics (LIPIcs). <http://rdp15.mimuw.edu.pl/index.php?site=tlca>. <10.4230/LIPIcs.TLCA.2015.332>. <hal-01222743>
  • Kaustuv Chaudhuri. Undecidability of Multiplicative Subexponential Logic. Sandra Alves and Iliano Cervesato. Proceedings of the Third International Workshop on Linearity, Jul 2014, Vienna, Austria. 176, pp.1--8, 2014, Electronic Proceedings in Theoretical Computer Science. <10.4204/EPTCS.176.1>. <hal-00998753>
  • Mary Southern, Kaustuv Chaudhuri. A Two-Level Logic Approach to Reasoning about Typed Specification Languages. Venkatesh Raman and S. P. Suresh. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), Dec 2014, New Delhi, India. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 29, 2014, <http://www.fsttcs.org/>. <10.4230/LIPIcs.FSTTCS.2014.557>. <hal-01091544>
  • Kaustuv Chaudhuri, Nicolas Guenot. Equality and fixpoints in the calculus of structures. Thomas A. Henzinger and Dale Miller. JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC (CSL) AND the Twenty-Ninth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS), Jul 2014, Vienna, Austria. ACM-SIGPLAN, pp.1 - 10, 2014, <http://lics.rwth-aachen.de/csl-lics14/>. <10.1145/2603088.2603140>. <hal-01091570>
  • Olivier Savary Bélanger, Kaustuv Chaudhuri. Automatically Deriving Schematic Theorems for Dynamic Contexts. Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2014, Vienna, Austria. ACM-SIGPLAN, 2014, <http://complogic.cs.mcgill.ca/lfmtp14/>. <10.1145/2631172.2631181 >. <hal-01091555>
  • Joelle Despeyroux, Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. LIPIcs. TYPES'2013, Apr 2013, Toulouse, France. Post-proceedings of TYPES'2013, 19th Intl Conference on Types for Proofs and Programs, LIPIcs., 26, pp.150-168, 2014. <hal-01285039>
  • Kaustuv Chaudhuri. Subformula Linking as an Interaction Method. 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. Springer, 7998, pp.386-401, 2013, Lecture Notes in Computer Science; Interactive Theorem Proving : 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013 : Proceedings. <10.1007/978-3-642-39634-2_28>. <hal-00937009>
  • Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur. Reasoning About Higher-Order Relational Specifications. Tom Schrijvers. International Symposium on Principles and Practice of Declarative Programming, Sep 2013, Madrid, Spain. ACM, 2013, <10.1145/2505879.2505889>. <hal-00787126v2>
  • Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. Patrick Cégielski and Arnaud Durand. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. 16, pp.183-197, 2012, Leibniz International Proceedings in Informatics (LIPIcs). <10.4230/LIPIcs.CSL.2012.183>. <hal-00772396>
  • Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic. Chris Hawblitzel and Dale Miller. Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, 7679, pp.208--223, 2012, Lecture Notes in Computer Science (LNCS). <10.1007/978-3-642-35308-6_17>. <hal-00760118>
  • Kaustuv Chaudhuri, Nicolas Guenot, Lutz Straßburger. The Focused Calculus of Structures. Marc Bezem. 20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. 12, pp.159-173, 2011, Leibniz International Proceedings in Informatics (LIPIcs). <10.4230/LIPIcs.CSL.2011.159>. <hal-00772420>
  • Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. The TLA+ Proof System: Building a Heterogeneous Verification Platform. Ana Cavalcanti and David Déharbe and Marie-Claude Gaudel and Jim Woodcock. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. Springer, 6255, pp.44, 2010, Lecture Notes in Computer Science; Theoretical Aspects of Computing - ICTAC 2010. <10.1007/978-3-642-14808-8_3>. <inria-00521886>
  • Kaustuv Chaudhuri. Magically Constraining the Inverse Method Using Dynamic Polarity Assignment. Christian Fermueller and Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Oct 2010, Yogyakarta, Indonesia. Springer, 6397, pp.202--216, 2010, LNCS. <10.1007/978-3-642-16242-8_15>. <inria-00535948>
  • Kaustuv Chaudhuri. Classical and Intuitionistic Subexponential Logics are Equally Expressive. Anuj Dawar and Helmut Veith. Computer Science Logic, Aug 2010, Brno, Czech Republic. Springer, 6247, pp.185--199, 2010, LNCS. <10.1007/978-3-642-15205-4_17>. <inria-00534865>
  • Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. Verifying Safety Properties With the TLA+ Proof System. Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, 6173, pp.142--148, 2010, Lecture Notes in Artificial Intelligence; Automated Reasoning 5th International Joint Conference, IJCAR 2010 Edinburgh, UK, July 16-19, 2010 Proceedings. <10.1007/978-3-642-14203-1_12>. <inria-00534821>
  • Alexis Saurin, Kaustuv Chaudhuri, Dale Miller. Canonical Sequent Proofs via Multi-Focusing. Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, Sep 2008, Milano, Italy. pp.383-396, 2008, <10.1007/978-0-387-09680-3_26>. <hal-00527893>
  • Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. A TLA+ Proof System. Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA), 2008, Doha, Qatar. 2008. <inria-00338299>

Documents associated with scientific events1 document

  • Kaustuv Chaudhuri, Gopalan Nadathur. Reasoning about Computational Systems using Abella. Abella Tutorial, Aug 2015, Berlin, Germany. 2015. <hal-01222774>

Directions of work or proceedings1 document

Preprints, Working Papers, ...1 document

  • Kaustuv Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. 2015. <hal-01222767>

Reports2 documents

  • Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger. Focused and Synthetic Nested Sequents (Extended Technical Report). [Research Report] Inria. 2016. <hal-01251722v2>
  • Kaustuv Chaudhuri, Joelle Despeyroux. A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology. [Research Report] 2013, pp.30. <inria-00402942v5>