Abstract
A common belief is that formalizing semantics of programming languages requires the use of a proof assistant providing (1) a specification language with advanced features such as higher-order logic, inductive definitions, type polymorphism, and (2) a corresponding proof environment where higher-order and inductive reasoning can be performed, typically with user interaction. In this paper we show that such a formalization is nowadays possible inside a mostly-automatic program verification environment. We substantiate this claim by formalizing several semantics for a simple language, and proving their equivalence, inside the Why3 environment.
Cite
CITATION STYLE
Clochard, M., Filliâtre, J. C., Marché, C., & Paskevich, A. (2014). Formalizing semantics with an automatic program verifier. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8471, pp. 37–51). Springer Verlag. https://doi.org/10.1007/978-3-319-12154-3_3
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
