Programming Language Semantics with Isabelle/HOL

Author

Martini, Antonio

Author_Institution

Fac. of Inf., PUCRS, Porto Alegre, Brazil

fYear

2013

Firstpage

14

Lastpage

21

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Theoretical Computer Science (WEIT), 2013 2nd Workshop-School on

Conference_Location

Rio Grande

Type

conf

DOI

10.1109/WEIT.2013.29

Filename

6778559