Skip to main content

more options

I'm interested in building more trustworthy and easy to use Proof Assistants. Recently, for the Coq proof assistant, I developed a new parametricity theory and implementation that automatically produces Coq proofs needed to transport theorems across isomorphic instantiations of interfaces. I am also a contributor to the Certicoq project which is building a compiler for Coq that is written and proved correct in Coq. Less recently, to increase the trust in the Nuprl proof assistant, Vincent and I formalized a model of the Nuprl in the Coq proof assistant.

I'm also interested in using these Proof Assistants to make this world a safer place. Recently, I developed ROSCoq, a framework for developing certified robotic programs in Coq.

My past reseach also addresses problems in Machine Vision and Computer Systems.
My publications can be found below. For a more up-to-date list, visit my google scholar profile.

Publications and Technical Reports

    Proof Assistants

  1. Revisiting Parametricity: Inductives and Uniformity of Propositions (with Greg Morrisett), arXiv Technical Report, 2017 . [PDF, github, invited talk at the Coq Implementor's workshop 2017]
    Unsuccessful attempts to publish this work:
  2. Towards a Formally Verified Proof Assistant (with Vincent Rahli), ITP-2014 . [PDF, Tech. Report, website]
  3. A Generic Approach to Proofs about Substitution (with Vincent Rahli), LFMTP-2014 . [PDF, website ]
  4. Proof Assistants ∩ Robotics

  5. ROSCoq : Robots powered by Constructive Reals (with Ross Knepper) , ITP-2015 , also presented at the Coq Workshop 2015 [PDF, website, slides, github, more recent slides ]
  6. Robotics ∩ Machine Vision

  7. Contextually Guided Semantic Labeling and Search for 3D Point Clouds (with Hema Swetha Koppula, Thorsten Joachims, and Ashutosh Saxena) In International Journal of Robotics Research, 2012. [arXivPDF]
  8. Semantic Labeling of 3D Point Clouds for Indoor Scenes (with Hema Swetha Koppula, Thorsten Joachims and Ashutosh Saxena) In Neural Information Processing Systems, 2011. [PDF, website]
  9. 3D Scene Grammar for Parsing RGB-D Pointclouds (with Sherwin Li) arXiv Technical Report, 2012. [arXiv]
  10. Computer Systems

  11. Finding Almost-Invariants in Distributed Systems. (with Maysam Yabandeh, Marco Canini, and Dejan Kostic) In The 30th IEEE Symposium on Reliable Distributed Systems (SRDS), 2011. [PDF]
  12. An Energy Efficient Low Latency MAC Protocol for Query Based Wireless Sensor Networks. (with Shikhar Sachan, Kalpesh Kapoor, and Sukumar Nandi) In International conference on Distributed Computing and Networking, 2009. [PDF]