A dynamic logic to reason about Reo circuits implemented in Coq.
This repository contains an implementation of ReLo language in Coq
To execute it, please install Coq 8.13+ and compile file ''LogicMain.v'' to proceed. It comprises the following
- Core concepts of ReLo logic
- A Model constructor for a formula over a ReLo Program
- A tableau for ReLo
For more information on ReLo logic, please refer to the preproceeding of LSFA 2020: http://lsfa2020.ufba.br/lsfa2020-preproc.pdf#page=37