Abstract
We present a simple and effective methodology for equational reasoning in proof checkers. The method is based on a two-level approach distinguishing between syntax and semantics of mathematical theories. The method is very general and can be carried out in any type system with inductive and oracle types. The potential of our two-level approach is illustrated by some examples developed in Lego.
Cite
CITATION STYLE
Barthe, G., Ruys, M., & Barendregt, H. (1996). A two-level approach towards lean proof-checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1158 LNCS, pp. 16–35). https://doi.org/10.1007/3-540-61780-9_59
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
