gmalecha at gmail dot com
Experimenting with Mtac
on Apr 18, 2016
PhD Defense: Extensible Proof Engineering in Intensional Type Theory
on Mar 22, 2016
Using SMT Solvers in Coq 8.5
on Mar 16, 2016
Rtac: Reflective Tactics in Coq
on Feb 20, 2016
Approximating Inductive Types in Coq
on Jan 14, 2016
Embedding Logics in Coq
on Dec 18, 2015
The Core of Computational Reflection
on Oct 3, 2015
MirrorCore is a framework for easing the burden of building reflective automation in Coq proof assistant.
ExtLib is an extension to Coq's standard library which embraces new features such as universe polymorphism, primitive projections, and type classes.
Template-Coq is a bare-bones quoting library for Coq. Its syntax is designed to be as close as possible to Coq's internal representation.
VeriDrone is exploring foundational verification of cyber-physical systems such as quadcopters. Check us out!
Modular Deductive Verification of Sampled-Data Systems
on Oct 14, 2016
Towards Foundational Verification of Cyber-physical Systems
on Apr 11, 2016
Formal Verification of Stability Properties in Cyber-physical Systems
on Jan 23, 2016
Extensible and Efficient Automation through Reflective Tactics
on Jan 1, 2016
Towards Verification of Hybrid Systems in a Foundational Proof Assistant
on Sep 23, 2015