@inbook{dc09c90e87cd40d3ad5a046628a343f2,
title = "A Coq Implementation of the Program Algebra in Jifeng He{\textquoteright}s New Roadmap for Linking Theories of Programming",
abstract = "Jifeng He has proposed a roadmap for linking theories of programming and presents an algebra of programs capable of generating both denotational and operational representations from the refinement relation. In this paper, we implement this algebra of programs and its refinement relation using the interactive theorem prover Coq. Encoding the algebra into CIC (Calculus of Inductive Constructions), the main formalism in Coq, facilitates machine-aided interactive proving for the properties of programs using predefined algebraic laws. The implementation of the algebra for finite programs enables us to prove that every finite program can be reduced to the normal form and to check the refinement between two finite programs. The implementation of the algebra for infinite programs supports formalizing recursive programs with one variable and checking the refinement between one finite and one infinite program. Then, we present examples of proving the refinement relationship between two finite programs and a finite program and an infinite program.",
keywords = "Coq, Program algebra, Refinement, Unifying theories of programming",
author = "Rundong Mu and Qin Li",
note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.",
year = "2023",
doi = "10.1007/978-3-031-40436-8\_15",
language = "英语",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Science and Business Media Deutschland GmbH",
pages = "395--412",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
address = "德国",
}