Coq formalization of QRC1
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
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).
Worms in Coq
A Coq implementation of the Worm Calculus, the (closed fragment of the) Reflection Calculus, and the relationship between them.