Curriculum Vitae

PDF | TXT

Address

Centre de Recherche Commun
INRIA-Microsoft Research
28 rue Jean Rostand,
91893 Orsay Cedex, France

Contact

Telephone: +33 1 69 35 69 65
Fax: +33 1 69 35 69 69
E-mail: kaustuv.chaudhuri@gmail.com

Education

Carnegie Mellon University, August 2000 – December 2006
Ph.D. in Computer Science (Pure & Applied Logic)

Carnegie Mellon University, August 1996 – May 2000
B.S. in Computer Science (university honours)
B.S. in Mathematics (university honours)

Research Experience

  • See also: research statement

  • Interests: automated theorem proving; proof theory; substructural, temporal, hybrid, and non-classical logics; specification of stateful, concurrent and distributed systems; logic programming; logical frameworks; stochastic and probabilistic process calculi; systems biology.

Microsoft Research - INRIA Joint Centre, Orsay, France
Post-doctoral fellow, November 2007 – Present
Member of the Tools for Proofs project
Supervisors: Damien Doligez, Leslie Lamport, Stephan Merz

INRIA and LIX@École Polytechnique, Palaiseau, France
Post-doctoral fellow, November 2006 – October 2007
Member of the Parsifal project
Supervisor: Dale Miller

Carnegie Mellon University, Computer Science Dept., Pittsburgh, USA
Doctoral research, August 2000 – October 2006
Thesis: The Focused Inverse Method for Linear Logic
Advisor: Frank Pfenning
Committee: Frank Pfenning, Stephen Brookes, Jeremy Avigad, Tanel Tammet

Microsoft Research, Redmond, USA
Research internship, June 2004 – September 2004
Member of the Farsite project
Mentors: John Douceur, Jon Howell

Carnegie Mellon University, Pittsburgh, USA
Undergraduate research on bidirectional theorem proving
Advisor: Frank Pfenning

Publications

See also:

Refereed Journals

[CPP08] K. Chaudhuri, F. Pfenning and G. Price, A Logical Characterization of Forward and Backward Chaining in the Inverse Method. Journal of Automated Reasoning, 40(2–3), pp. 133–177. 2008.

Refereed Conferences

[Cha08] K. Chaudhuri, Focusing Strategies in the Sequent Calculus of Synthetic Connectives. Logic for Programming, Artificial Intelligence and Reasoning (LPAR-15), Doha, Qatar. Springer-Verlag LNCS 5330, pp. 467–481. November 2008.
[CMS08] K. Chaudhuri, D. Miller and A. Saurin, Canonical Sequent Proofs via Multi-Focusing. IFIP International Conference on Theoretical Computer Science (TCS-5), Milan, Italy. IFIP 273, pp. 383–396. September 2008.
[CPP06] K. Chaudhuri, F. Pfenning and G. Price, A Logical Characterization of Forward and Backward Chaining in the Inverse Method. International Joint Conference on Automated Reasoning (IJCAR-3), Seattle, Washinton. Springer-Verlag LNCS 4130, pp. 97–111. August 2006.
[CP05b] K. Chaudhuri and F. Pfenning, Focusing the Inverse Method for Linear Logic. Computer Science Logic (CSL-19), Oxford, UK. Springer-Verlag LNCS 3634, pp. 200–215. August 2005.
[CP05a] K. Chaudhuri and F. Pfenning, A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. Conference on Automated Deduction (CADE-20), Tallinn, Estonia. Springer-Verlag LNCS 3632, pp. 69–83. July 2005.

Refereed Workshops

[CDLM08] K. Chaudhuri, D. Doligez, L. Lamport and S. Merz, A TLA+ Proof System. Workshop on Knowledge Exchange: Automated Provers and Proof Assistants (KEAPPA). CEUR Workshop Proceedings 418, pp. 17–37. November 2008.

Technical Reports

[CD09] K. Chaudhuri and J. Despeyroux, A Logic for Constrained Process Calculi with Applications to Molecular Biology. INRIA. Technical Report. May 2009.
[Cha06] K. Chaudhuri, The Focused Inverse Method for Linear Logic. Carnegie Mellon University. Ph.D. thesis, available as technical report CMU-CS-06-162. December 2006.
[CP05t] K. Chaudhuri and F. Pfenning, Focusing the Inverse Method for Linear Logic. Carnegie Mellon University. Technical Report CMU-CS-05-106. July 2005.
[Cha03] K. Chaudhuri, The Inverse Method for Intuitionistic Linear Logic (The Propositional Fragment). Carnegie Mellon University. Technical Report CMU-CS-03-140. November 2003.
[CCP03] B.-Y. E. Chang, K. Chaudhuri and F. Pfenning, A Judgemental Analysis of Linear Logic. Carnegie Mellon University. Technical Report CMU-CS-03-131R. April 2003.

Teaching Experience

Professional

Member

Refereeing

References

Available on request