Computer-Aided Program Development Group

Reasoning about Cardinalities of Relations Supported by Proof Assistants

 

Here, you can find the proof scripts for the paper "Reasoning about Cardinalities of Relations Supported by Proof Assistants" submitted at RAMiCS 2017.

Coq proof scripts  (Compiles with Coq 8.5 and the libraries relation-algebra-1.6 and cardinal.)

Isabelle/HOL library  (Compiles with Isabelle2016 and the library Relation-Algebra.)

 

NEW: Isabelle/HOL library  (Compiles with Isabelle2016.1 and the library Relation-Algebra.)