About

My name is Arthur Azevedo de Amorim. I’m a post-doctoral researcher at CMU.

This is a blog about the Coq proof assistant and programming language. With Coq, it is possible to develop programs, write a specification capturing their intended behavior, and prove that the specification is satisfied. That proof is then checked by Coq to ensure that is logically valid. One can also use Coq to formalize much of Mathematics. Great examples of its use in the real world include CompCert, a verified C compiler, and the formalization of the Feit-Thompson theorem.

This blog is generated using Hakyll, Sass and Compass. All source files, including posts and Coq developments, are available on GitHub.