This repository contains a brief Coq development for the paper:
Constraint Logic Programming with a Relational Machine Emilio Jesús Gallego Arias, James Lipton, and Julio Mariño
This formalization is a work-in-progress and shouldn't be considered final by any means.
The code requires Coq v8.4 and MathComp v1.5
- nf_weak.v: results about the preliminary transition system.