Commit 506bd180 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Add `cl_logic` folder to README.

parent ad435a84
......@@ -100,6 +100,9 @@ followed by `make build-dep`.
modules; they may change or disappear without any notice.
* The folder [si_logic](theories/si_logic) defines a "plain" step-indexed logic
and shows that it is an instance of the BI interface.
* The folder [cl_logic](theories/cl_logic) embeds classical logic in Coq,
following essentially the Gödel-Gentzen translation, and shows that it is an
instance of the BI interface.
## Case Studies
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment