Arthur Azevedo de Amorim

poleiro. A blog about Coq

extructures. Finite sets and maps for Coq with extensional equality

deriving. Class instances for Coq inductive types with little boilerplate

agda-hoas-demo. Experiments with higher-order abstract syntax in Agda

memory-safe-language. A formalization of properties of a simple imperative, memory-safe language.

cryptis. Rocq Prover

coq-utils. Some basic libraries for Coq.

beaq. A Formalization of TeX in Coq

cufp-2015-tutorial. An introductory tutorial for the Coq proof assistant.

finprob. Finite probability theory in Coq

sf-grader. Auto grader for Software Foundations

cutelittlethings. C++

netter. Produce Prism models from a simple imperative language

cis670-project. Oh yeah

coq-cpo. A Coq library for CPOs

ll-cut-elim. Cut elimination for Intuitionistic Linear Logic in Coq

plink.

mc326-bplus. C

yaml-mode. The emacs major mode for editing files in the YAML data serialization format.

umamao. Free and open source Q&A software, open source stackoverflow style app written in ruby, rails, mongomapper and mongodb.

emacs-files. Personal configuration files for Emacs

el-get. Manage the external elisp bits and pieces upon which you depend!

mongomapper. A Ruby Object Mapper for Mongo

OpaChat. A simple scalable, real-time web chat application in Opa

opalang. OPA

forest-explanations. Jupyter Notebook

GIMME. XMMS2 client for GNU Emacs

ssr-intro. An introduction to Coq through the ssreflect library.

Projeto-mc823.

project. C

opam-coq-archive. Archive for all Coq related OPAM packages organized in various repositories