Research Scientist, Inria (French: chargé de recherche)
Lecturer (parttime), École polytechnique (French: chargé d’enseignement)
Project Parsifal, Inria Saclay  ÎledeFrance
Office #2059, Alan Turing Building
1 rue Honoré d’Estienne d’Orves
Campus de l’École Polytechnique
91120
Palaiseau,
France (map)
+33 1 74 85 42 24 (voice)
kaustuv@chaudhuri.info
(PGP key)
Recent events
 WoF 2015: International Workshop on Focusing (PC member)
 FICS 2015: International Workshop on Fixed Points in Computer Science (PC member)
 Abella Tutorial @ CADE 2015 (Coorganizer with G. Nadathur)

LFMTP 2015: Logical Frameworks and MetaLanguages: Theory and Practice (PC cochair with
I. Cervesato)
I. Cervesato and K. Chaudhuri. Proceedings of the 10th International Workshop on Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP). EPTCS v.185. .  CPP 2015: ACMSIGPLAN Conference on Certified Programs and Proofs (PC member)
 LFMTP 2014: Logical Frameworks and MetaLanguages: Theory and Practice (PC member)
 SD 2014: International Workshop on Structures and Deduction (PC cochair with L. Straßburger and W. Heijltjes)
 ICLP 2014: International Confernece on Logic Programming (PC member)
Recent papers and drafts
 K. Chaudhuri. Encoding Additives Using Multiplicatives and Subexponentials. To appear in Mathematical Structures in Computer Science. Draft of August 2015. .
 K. Chaudhuri, S. Marin, and L. Straßburger. Focused and Synthetic Nested Sequents. Submitted. Draft manuscript. .
 K. Chaudhuri and G. Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. Accepted to Logic for Programming, Artificial Intelligence, and Reasoning (LPAR20), Suva, Fiji. Draft from September. .
 T. BrockNannestad and K. Chaudhuri. Disproving Using the Inverse Method by Iterated Refinement of Finite Approximations. Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX24), Wrocław, Poland. LNCS 9323, pp. 153–168. . ©Springer. See the associated theorem prover, Mætning.
 Y. Wang and K. Chaudhuri. A ProofTheoretic Characterization of Independence in Type Theory. International Conference on Typed Lambda Calculi and Applications (TLCA13), Warsaw, Poland. LIPIcs v.38, pp. 332–346. . This paper has a dedicated webpage.
 K. Chaudhuri, M. Cimini, and D. Miller. A lightweight formalization of the metatheory of bisimulationupto. ACMSIGPLAN Conference on Certified Programs and Proofs (CPP4), Mumbai, India. ACM Proceedings, pp. 157–166. . This paper has a dedicated webpage.
 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). .
Recent courses
 INF 321: Les principes des langages de programmation (Principles of Programming Languages), TD, Spring 2015, École polytechnique
 INF 431: Programmation d’applications concurrentes et distribuées (Concurrent and Distributed Programming), TD, Spring 2015, École polytechnique
 INF 321: Les principes des langages de programmation (Principles of Programming Languages), TD, Spring 2014, École polytechnique