License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.WPTE.2015.47
URN: urn:nbn:de:0030-drops-51811
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5181/
Go to the corresponding OASIcs Volume Portal

Smetsers, Sjaak ; Madlener, Ken ; van Eekelen, Marko

Formalizing Bialgebraic Semantics in PVS 6.0

pdf-format:
7.pdf (0.5 MB)

Abstract

Both operational and denotational semantics are prominent approaches for reasoning about properties of programs and programming languages. In the categorical framework developed by Turi and Plotkin both styles of semantics are unified using a single, syntax independent format, known as GSOS, in which the operational rules of a language are specified. From this format, the operational and denotational semantics are derived. The approach of Turi and Plotkin is based on the categorical notion of bialgebras. In this paper we specify this work in the theorem prover PVS, and prove the adequacy theorem of this formalization. One of our goals is to investigate whether PVS is adequately suited for formalizing metatheory. Indeed, our experiments show that the original categorical framework can be formalized conveniently. Additionally, we present a GSOS specification for the simple imperative programming language While, and execute the derived semantics for a small example program.

BibTeX - Entry

@InProceedings{smetsers_et_al:OASIcs:2015:5181,
  author =	{Sjaak Smetsers and Ken Madlener and Marko van Eekelen},
  title =	{{Formalizing Bialgebraic Semantics in PVS 6.0}},
  booktitle =	{2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)},
  pages =	{47--61},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Yuki Chiba and Santiago Escobar and Naoki Nishida and David Sabel and Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5181},
  URN =		{urn:nbn:de:0030-drops-51811},
  doi =		{10.4230/OASIcs.WPTE.2015.47},
  annote =	{Keywords: operational semantics, denotational semantics, bialgebras, distributive laws, adequacy, theorem proving, PVS, WHILE}
}

Keywords: operational semantics, denotational semantics, bialgebras, distributive laws, adequacy, theorem proving, PVS, WHILE
Collection: 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)
Issue Date: 2015
Date of publication: 17.06.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI