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.
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
- Towards Certified Meta-Programming with Typed Template-Coq (with Simon Boulier, Cyril Cohen, Matthieu Sozeau and Nicolas Tabareau), Interactive Theorem Proving, 2018 .
- 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 :
- ICFP 2017: reviews. how we addressed the reviews
- POPL 2018: reviews.
- 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 .
- Towards a Formally Verified Proof Assistant (with Vincent Rahli), ITP-2014 . [PDF, Tech. Report, website]
- A Generic Approach to Proofs about Substitution (with Vincent Rahli), LFMTP-2014 . [PDF, website ]
- 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 ]
- 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]
- 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]
- 3D Scene Grammar for Parsing RGB-D Pointclouds (with Sherwin Li) arXiv Technical Report, 2012. [arXiv]
- 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]
- 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]