Coq formalization of QRC1
2020-now
A Coq implementation of the Quantified Reflection Calculus with one modality.

The FormalV Library
Joint work with Quim Casals Buñuel, Juan Conejero Rodriguez, Mireia González Bedmar and Eduardo Hermo Reyes
2019-2022
The FormalV Library is the Coq/MathComp library developed in a public source-code setting by Formal Vindications S.L. Currently it includes three packages:

  • FV Prim63 to MathComp provides conversions from the Coq primitive integers Uint63 and Sint63 to the MathComp natural and integer numbers nat and int, and vice versa, as well as lemmas to rewrite between their respective operations.
  • FV Check Range provides tactics to automatically prove Boolean goals involving 1, 2 or 3 Uint63.int/Sint63.int bounded variables through brute-force computation.
  • FV Time is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds (which are part of the UTC standard but usually not implemented in commercial libraries).

templates
2021
Templates for configuration and other boilerplate files for Coq projects hosted on Gitlab, adapted from coq-community’s templates project.

Formalization of Basic Concepts from Tree Automata Theory in Coq
2020

Worms in Coq
2018
A Coq implementation of the Worm Calculus, the (closed fragment of the) Reflection Calculus, and the relationship between them.