Replication package with proofs for the paper "Operations on Fixpoint Equation Systems"

This archive contains mechanized proofs for the theorems and lemmas that appear in the paper Thomas Neele, Jaco van de Pol - Operations on Fixpoint Equation Systems. lmcs:11199 - Logical Methods in Computer Science, July 10, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:5)2024 This package contains proofs in both Coq (now known as Rocq) and PVS. See the included README file for details on how to execute the proofs.

Related Organizations

Aarhus University
Denmark
Eindhoven University of Technology
Netherlands

Keywords

PVS, proof assistant, fixpoint equation system, Coq

Impact byBIP!

	selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	0
	popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.	Average
	influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).	Average
	impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.	Average