Education

• M.Sc., Artificial Intelligence, 2001
  The University of Edinburgh, Edinburgh, United Kingdom.

• B.E., Industrial Engineering, 1998
  Indian Institute of Technology, Roorkee, India.

Publications

• S. Kothari and J. Caldwell. Towards a Formalized Completeness Proof of Wand's Type Inference Algorithm: Some Issues of Freshness
  [ps | pdf ]. Coq proof scripts [ Coq script |HTML ].

• S. Kothari and J. Caldwell. A Machine Checked Model of Idempotent MGU Axioms For a List of Equational Constraints [ps | pdf | slides].
  Presented at the 24th International Workshop on Unification (UNIF'10), July 14, 2010, Edinburgh, United Kingdom.
  Coq proofs of Idempotent MGU axioms [ Coq script |HTML ]. Also needed this file.

• S. Kothari and J. Caldwell. Toward a machine-certified correctness proof of Wand's type reconstruction algorithm [ps | pdf | slides].
  Extended abstract. 4th Informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM'09), Edinburgh, United Kingdom.

• S. Kothari, J. Caldwell. A Machine Checked Model of MGU Axioms: Applications of Finite Maps and Functional Induction [ps | pdf | slides ].
  Presented at the 23rd International Workshop on Unification (UNIF'09), Montreal, Canada.
  Coq proofs of MGU axioms [Coq script | HTML ]. Also needed (for reasoning about unique lists) [ Coq script | HTML ].

• S. Kothari and J. Caldwell. On Extending Wand's Type Reconstruction Algorithm to Handle Polymorphic Let [ps | pdf ].
  Presented at the Fourth Conference on Computability in Europe (CiE'08), Athens, Greece. June 15-20, 2008.
  OCaml source code: Extended Wand's Algorithm

• S. Kothari and J. Caldwell. Wand's Algorithm extended for the Polymorphic ML-Let [ps | pdf ].
  Technical Report, University of Wyoming, 2007.
  OCaml source code: Extended Wand's Algorithm, OCaml source code representing proof idea is available here.

• S. Kothari. Type Reconstruction Algorithms - A Survey [Updated version coming soon].
  Technical Report, University of Wyoming, 2007.
  OCaml source code: Algorithm W, Algorithm J, Algorithm M, Wand's Algorithm.

• S. Kothari and M. Sulzmann. C++ templates/traits versus haskell type classes [ bib | pdf | ps ].
  Technical Report TRB2/05, The National University of Singapore, 2005.

• S.Kothari. A declarative approach towards ensuring auto-completion and auto-update of HTML form fields [ps | pdf | HTML].
  Unpublished paper.
  The examples mentioned in the paper are available here. The binary .jar file is available here.

Work Experience

•  Aug'04 - Jul'05  Senior Software Engineer 

•  Mar'00 - Jul'00  Consultant

•  Jul'98 - Mar'00  Software Engineer 

Future Events

• None

Past Events

• Attended Oregon Programming Languages Summer School, University of Oregon, Eugene, Oregon, June 15-25, 2010.

• Attended 23rd International Workshop on Unification (UNIF'09),
  McGill University, Montreal, Canada, August 2, 2009.

• Attended Summer School on Logic and Theorem Proving in Programming Languages,
  University of Oregon, Eugene, Oregon, July 22-30, 2008.

• Attended Fourth International Conference on Computability in Europe, Athens, Greece, June 15-20, 2008.

• Attended International Summer School on Generative Programming, Tampere, Finland, June 4-7, 2002.

Teaching Duties

Courses Taken

• Research Writing
• Theory of Computation
• Constructive Logic and Mathematics in Computer Science
• Analysis of Algorithms
• Automatic Programming
• Software Validation and Verification
• Operating Systems
• Machine Learning
• Languages and Automata
• Graduate Seminar on Emergent Behavior
• Graduate Seminar on Type Reconstruction Algorithms
• Graduate Seminar on Names and Bindings in Programming Languages
• Graduate Seminar on Detecting and Eliminating Software Bugs

Knowledge Sharing

• Machine Learning notes based on Tom Mitchell's book [ ps | pdf]

• A useful trick for inclusion and exclusion of commented code