4093 Engineering Hall University of Wyoming Laramie, WY-82071, USA Phone: 001-307-766-5147 (W) Email: skothari at uwyo.edu

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. Toward a machine-certified correctness proof of Wand's type reconstruction algorithm [ps | pdf ].
  Extended abstract. 4th Informal ACM SIGPLAN Workshop on Mechanizing Metatheory (WMM'09), Edinburgh, Scotland.

• 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 proof scripts of MGU axioms: here. Also needed this file.

• 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 [ps | pdf ].
  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 

Past Events

• 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