Research Scientist (French: chargé de recherche)
1 rue Honoré d’Estienne d’Orves
Campus de l’École Polytechnique
91120 Palaiseau, France (map)
- Abella 2.0.0 has been released! This version adds support for arbitrary higher-order hereditary Harrop specifications. Check out this neat example of reasoning on higher-order specs: a structural characterization of λ-terms in terms of a simple inductive notion of λ-paths. Some specific technical details can be found in the PPDP paper below.
Recent papers and drafts
- K. Chaudhuri, M. Cimini, and D. Miller. Formalization of the Bisimulation-Up-To Technique and its Meta Theory. Draft manuscript. Submitted. .
- K. Chaudhuri, S. Hetzl, and D. Miller. The Isomorphism Between Expansion Proofs and Multi-Focused Sequent Proofs. To appear in the Journal of Logic and Computation. Draft manuscript. .
- 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. . ©ACM
- K. Chaudhuri. Subformula Linking as an Interaction Method. Conference on Interactive Theorem Proving (ITP-04), Rennes, France. LNCS 7998, pp. 386–401. . ©Springer
See also the associated tool: Profound (available from github).
- K. Chaudhuri, and J. Despeyroux. A Hybrid Linear Logic for Constrained Transition Systems. Types for Proofs and Programs (TYPES-19), Toulouse, France. .
- K. Chaudhuri. Equality and Fixpoints in the Calculus of Structures. Draft manuscript. .