Number of documents

33

Kaustuv Chaudhuri


Research Interests


Journal articles4 documents

  • Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux. Hybrid Linear Logic, revisited. Mathematical Structures in Computer Science, Cambridge University Press (CUP), In press, ⟨10.1017/S0960129518000439⟩. ⟨hal-01968154⟩
  • Kaustuv Chaudhuri. Expressing Additives Using Multiplicatives and Subexponentials. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (5), pp.651-666. ⟨hal-01222767⟩
  • 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⟩
  • 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⟩

Conference papers25 documents

  • Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller. A Proof-Theoretic Approach to Certifying Skolemization. CPP 2019 - 8th ACM SIGPLAN International Conference, Jan 2019, Cascais, Portugal. pp.78-90, ⟨10.1145/3293880.3294094⟩. ⟨hal-02368946⟩
  • Kaustuv Chaudhuri, Ulysse Gérard, Dale Miller. Computation-as-deduction in Abella: work in progress. 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom. ⟨hal-01806154⟩
  • Kaustuv Chaudhuri. A Two-Level Logic Perspective on (Simultaneous) Substitutions. CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States. ⟨hal-01968139⟩
  • Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger. Focused and Synthetic Nested Sequents. FOSSACS 2016 - 19th International Conference Foundations of Software Science and Computation Structures, Apr 2016, Eindhoven, Netherlands. ⟨10.1007/978-3-662-49630-5_23⟩. ⟨hal-01417618⟩
  • Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger. Modular Focused Proof Systems for Intuitionistic Modal Logics. FSCD 2016 - 1st International Conference on Formal Structures for Computation and Deduction, Jun 2016, Porto, Portugal. ⟨10.4230/LIPIcs.FSCD.2016.16⟩. ⟨hal-01417603⟩
  • Kaustuv Chaudhuri, Giselle Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. pp.146--161, ⟨10.1007/978-3-662-48899-7_11⟩. ⟨hal-01208362⟩
  • Yuting Wang, Kaustuv Chaudhuri. A Proof-theoretic Characterization of Independence in Type Theory. 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Jul 2015, Warsaw, Poland. pp.332--346, ⟨10.4230/LIPIcs.TLCA.2015.332⟩. ⟨hal-01222743⟩
  • 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. ⟨10.1007/978-3-319-24312-2_11⟩. ⟨hal-01222592⟩
  • Kaustuv Chaudhuri, Matteo Cimini, Dale Miller. A Lightweight Formalization of the Metatheory of Bisimulation-Up-To. 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), ACM-SIGPLAN, Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693170⟩. ⟨hal-01091524⟩
  • Kaustuv Chaudhuri, Nicolas Guenot. Equality and fixpoints in the calculus of structures. 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. pp.1 - 10, ⟨10.1145/2603088.2603140⟩. ⟨hal-01091570⟩
  • Mary Southern, Kaustuv Chaudhuri. A Two-Level Logic Approach to Reasoning about Typed Specification Languages. 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), Dec 2014, New Delhi, India. ⟨10.4230/LIPIcs.FSTTCS.2014.557⟩. ⟨hal-01091544⟩
  • 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. ⟨10.1145/2631172.2631181 ⟩. ⟨hal-01091555⟩
  • Kaustuv Chaudhuri. Undecidability of Multiplicative Subexponential Logic. Proceedings of the Third International Workshop on Linearity, Jul 2014, Vienna, Austria. pp.1--8, ⟨10.4204/EPTCS.176.1⟩. ⟨hal-00998753⟩
  • Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur. Reasoning About Higher-Order Relational Specifications. International Symposium on Principles and Practice of Declarative Programming, ACM SIGPLAN, Sep 2013, Madrid, Spain. ⟨10.1145/2505879.2505889⟩. ⟨hal-00787126v2⟩
  • Kaustuv Chaudhuri. Subformula Linking as an Interaction Method. 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.386-401, ⟨10.1007/978-3-642-39634-2_28⟩. ⟨hal-00937009⟩
  • Joelle Despeyroux, Kaustuv Chaudhuri. A Hybrid Linear Logic for Constrained Transition Systems. TYPES 2013 - 19th International Conference on Types for Proofs and Programs, Apr 2013, Toulouse, France. pp.150-168. ⟨hal-01285039⟩
  • Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller. A Systematic Approach to Canonicity in the Classical Sequent Calculus. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. pp.183-197, ⟨10.4230/LIPIcs.CSL.2012.183⟩. ⟨hal-00772396⟩
  • Kaustuv Chaudhuri. Compact Proof Certificates for Linear Logic. Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.208--223, ⟨10.1007/978-3-642-35308-6_17⟩. ⟨hal-00760118⟩
  • Kaustuv Chaudhuri, Nicolas Guenot, Lutz Straßburger. The Focused Calculus of Structures. 20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. pp.159-173, ⟨10.4230/LIPIcs.CSL.2011.159⟩. ⟨hal-00772420⟩
  • Kaustuv Chaudhuri. Classical and Intuitionistic Subexponential Logics are Equally Expressive. Computer Science Logic, Aug 2010, Brno, Czech Republic. pp.185--199, ⟨10.1007/978-3-642-15205-4_17⟩. ⟨inria-00534865⟩
  • Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. The TLA+ Proof System: Building a Heterogeneous Verification Platform. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩. ⟨inria-00521886⟩
  • Kaustuv Chaudhuri. Magically Constraining the Inverse Method Using Dynamic Polarity Assignment. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Oct 2010, Yogyakarta, Indonesia. pp.202--216, ⟨10.1007/978-3-642-16242-8_15⟩. ⟨inria-00535948⟩
  • Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz. Verifying Safety Properties With the TLA+ Proof System. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. pp.142--148, ⟨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, ⟨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. ⟨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

  • Iliano Cervesato, Kaustuv Chaudhuri. Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice. Iliano Cervesato; Kaustuv Chaudhuri. Aug 2015, Berlin, Germany. 2015, ⟨10.4204/EPTCS.185⟩. ⟨hal-01222747⟩

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⟩