Towards Rewriting in Coq

Autor:	Daria Walukiewicz-Chrząszcz, Jacek Chrząszcz
Rok vydání:	2007
Předmět:	Critical pair TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Programming language Computer science TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Confluence Proof assistant Rewriting Inductive type Research process computer.software_genre computer
Zdroj:	Rewriting, Computation and Proof ISBN: 9783540731467 Rewriting, Computation and Proof
DOI:	10.1007/978-3-540-73147-4_6
Popis:	Equational reasoning in Coq is not straightforward. For a few years now there has been an ongoing research process towards adding rewriting to Coq. However, there are many research problems on this way. In this paper we give a coherent view of rewriting in Coq, we describe what is already done and what remains to be done. We discuss such issues as strong normalization, confluence, logical consistency, completeness, modularity and extraction.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::95d6cc5c58059d384ce08e944522b81d https://doi.org/10.1007/978-3-540-73147-4_6 Zobrazit plný text záznamu