Coq provides two ways to finish definitions
Defined. The former is meant for “proofs” and makes the definition opaque while the later is meant for “definitions” and leaves the definition transparent. While the “proof” and “definition” dicotomy initially makes a lot of sense to users, but as users start to use dependent types more and more, they realize that the distinction is quite arbitrary, in which case, should we abandon
Qed? In this post, I argue that yes abandoning
Qedis a perfectly sensible thing to do.
You can now watch my thesis defense on computational reflection in intensional type theory. Some minor hicups during the talk but otherwise gives a very high-level overview of MirrorCore and Rtac at the time (2014).
During my post-doc at UCSD I’ve been working on verifying cyber-physical systems in the VeriDrone project. Cyber-physical systems are just systems that interact with the real world (think quadcopters, cars, planes, hydro-electric dams, and robots). The interesting thing about verifying cyber-physical systems in Coq is that they require a lot of reasoning about continuous mathematics, real numbers, differential equations, and all that. Coq does a great job at all of the discrete reasoning that we do (see my previous blog post on embedding logics in Coq) but at the end of all the nice theory, problems often boil down to mundane reasoning about real arithmetic. In this post I’m going to discuss a plugin that I wrote to call SMT solvers from Coq.
gmalecha at gmail
Mullings on computer science and math: programming languages, compilers, and program analysis.