1 rue Honoré d’Estienne d’Orves
Campus de l’École Polytechnique
91120 Palaiseau, France (map)
NEW! IJCAR 2020: International Joint Conference on Automated Deduction (Conference chair)
Stay tuned for more information about IJCAR-FSCD 2020 in Paris!
- NEW! LICS 2019: ACM/IEEE Symposium on Logic in Computer Science (PC member)
- SD 2017: Structures and Deduction (PC co-chair with A. Das and W. Heijltjes)
- LFMTP 2017 : Logical Frameworks and Meta-Languages: Theory and Practice (PC member)
- LSFA 2017: Workshop on Logical and Semantic Frameworks, with Applications (PC member)
- LSFA 2016: Workshop on Logical and Semantic Frameworks, with Applications (invited speaker)
- WoF 2015: International Workshop on Focusing (PC member)
- FICS 2015: International Workshop on Fixed Points in Computer Science (PC member)
- Abella Tutorial @ CADE 2015 (Co-organizer with G. Nadathur)
LFMTP 2015: Logical Frameworks and Meta-Languages: Theory and Practice (PC co-chair with I. Cervesato)
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.
- CPP 2015: ACM-SIGPLAN Conference on Certified Programs and Proofs (PC member)
- LFMTP 2014: Logical Frameworks and Meta-Languages: Theory and Practice (PC member)
- LINEARITY 2014: International Workshop on Linearity (PC member)
- SD 2014: International Workshop on Structures and Deduction (PC co-chair with L. Straßburger and W. Heijltjes)
- ICLP 2014: International Confernece on Logic Programming (PC member)
Recent papers and drafts
- K. Chaudhuri, M. Manighetti, and D. Miller. A proof-theoretic approach to certifying skolemization. Draft manuscript. Submitted. April 2018. Supplementary code
- 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.
- 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 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
- 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.
- CSE 102: Computer Programming, Instructor, Spring 2018, part of the new Bachelor Program @ École polytechnique
- INF 441: Programmation avancée (Advanced Programming), TD, Spring 2017-2018, École polytechnique
- INF 321: Les principes des langages de programmation (Principles of Programming Languages), TD, Spring 2014-2015, École polytechnique
- INF 431: Programmation d’applications concurrentes et distribuées (Concurrent and Distributed Programming), TD, Spring 2015, École polytechnique