An Axiomatization of Linear Temporal Logic in the Calculus of Inductive Constructions
- 1 December 2003
- journal article
- Published by Oxford University Press (OUP) in Journal of Logic and Computation
- Vol. 13 (6) , 801-813
- https://doi.org/10.1093/logcom/13.6.801
Abstract
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.Keywords
This publication has 0 references indexed in Scilit: