Matemática Discreta - Facultad de Informática de A Coruña

Coq in a Hurry - Exercises

🔪 OPG (Operator Precedence Grammar) Parser, in Coq.

Mastering the Art of Coq Programming

Final project for master's degree in Semantics of programming languages course.

Coq proof of an equivalence relation that is not congruent on the Imp language from Software Foundations

Updated version of the code found on Xavier Leroy's Compil course

My work and solutions for Coq In a Hurry by Yves Bertot.

Strong non-interference for fine-grained concurrent programs

Calvin Talks Types

Configuring Proof General for use with Coq is hard and the defaults suck. This is a simple baseline configuration for Emacs.

Certified regular expression matcher in Coq

A proof of the Pigeonhole principle. The Pigeonhole principle is a fundamental theorem that is used widely in Computer Science and Combinatorics, it asserts that if you put n things into m containers, and n > m, then at least one of the containers contains more than one thing.

Run `coqc` and print out colorized Coq error location information

Proof that the FFT implements the DFT, written in Coq.

Formalizing PEGs and a well-formedness algorithm in Coq

My master thesis (and related code) in Logic at the University of Bergen.

Proofs for the implementation of a power index via BDDs

Software Foundations book and exercises taken from https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

Dockerized Coq Image