An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
Solange Coupet-Grimal · Journal of Logic and Computation · 2003
We present in this paper a shallow embedding of Linear Temporal Logic in the Calculus of Inductive Constructions. Our axiomatization is based on a co-inductive representation of program executions. Temporal operators are implemented as co-inductive (respectively inductive) types when they are greatest (respectively least) fixpoints, and several generic lemmas are proved to allow elegant and efficient reasoning in practical cases. This work results in several reusable libraries in the Coq proof-assistant.