package coq-ltl
Linear Temporal Logic
Install
Dune Dependency
Authors
Maintainers
Sources
v8.10.0.tar.gz
md5=8a4b130957215e97768d37fb747f2c18
Description
This contribution contains a shallow embedding of Linear Temporal Logic (LTL) based on a co-inductive representation of program executions. Temporal operators are implemented as inductive (respectively co-inductive) types when they are least (respectively greatest) fixpoints. Several general lemmas, that correspond to LTL rules, are proved.
On This Page