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. Towards Certified Meta-Programming with Typed Template-Coq (with Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau), Interactive Theorem Proving, 2018 .
  2. 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, talk at CoqPL 2018]
    Reviews :
  3. CertiCoq: A verified compiler for Coq (with Andrew W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier Savary Belanger, Matthieu Sozeau and Matthew Weaver), CoqPL 2017 .
  4. Towards a Formally Verified Proof Assistant (with Vincent Rahli), ITP-2014 . [PDF, Tech. Report, website]
  5. A Generic Approach to Proofs about Substitution (with Vincent Rahli), LFMTP-2014 . [PDF, website ]
  6. Proof Assistants ∩ Robotics

  7. 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 ]
  8. Robotics ∩ Machine Vision

  9. 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]
  10. 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]
  11. 3D Scene Grammar for Parsing RGB-D Pointclouds (with Sherwin Li) arXiv Technical Report, 2012. [arXiv]
  12. Computer Systems

  13. 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]
  14. 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]