Computer Science – Logic in Computer Science
Scientific paper
2012-02-29
Mathematical Structures in Computer Science 21, 4 (2011) 827-859
Computer Science
Logic in Computer Science
Scientific paper
10.1017/S0960129511000120
Termination is an important property of programs; notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting systems, where many methods and tools have been developed over the years to address this problem. Ensuring reliability of those tools is therefore an important issue. In this paper we present a library formalizing important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.
Blanqui Frédéric
Koprowski Adam
No associations
LandOfFree
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-523837