Title :
Programming Language Semantics with Isabelle/HOL
Author :
Martini, Antonio
Author_Institution :
Fac. of Inf., PUCRS, Porto Alegre, Brazil
Abstract :
Isabelle is a generic meta-logical framework for implementing logical formalisms, and Isabelle/HOL is the specialization of Isabelle for HOL, which stands for Higher Order Logic. In programming language theory, formal semantics is the field concerned with the rigorous mathematical study of the meaning of programming languages. In this paper we develop a relational denotational semantics for a small imperative programming language and implement it as a theory in Isabelle/HOL. We give special attention to the specification of monotonic fix point functional for loops and provide non-trivial proofs of interesting lemmas and properties with the structured proof language Isar.
Keywords :
formal logic; logic programming languages; programming language semantics; theorem proving; Isabelle specialization; Isabelle/HOL; Isar; formal semantics; generic meta-logical framework; higher order logic; imperative programming language; logical formalisms; loops; mathematical study; monotonic fix point functional; nontrivial proofs; programming language semantics; programming language theory; relational denotational semantics; structured proof language; Abstracts; Computer languages; Computers; Equations; Lattices; Semantics; Syntactics; Isabelle/HOL; formal semantics; higher-order logic; proof assistants;
Conference_Titel :
Theoretical Computer Science (WEIT), 2013 2nd Workshop-School on
Conference_Location :
Rio Grande
DOI :
10.1109/WEIT.2013.29
