1 Search Results for "Smetsers, Sjaak"

Document
DOI: 10.4230/OASIcs.WPTE.2015.47
Formalizing Bialgebraic Semantics in PVS 6.0

Authors: Sjaak Smetsers, Ken Madlener, and Marko van Eekelen

Published in: OASIcs, Volume 46, 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)

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.
Cite as

Sjaak Smetsers, Ken Madlener, and Marko van Eekelen. Formalizing Bialgebraic Semantics in PVS 6.0. In 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015). Open Access Series in Informatics (OASIcs), Volume 46, pp. 47-61, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{smetsers_et_al:OASIcs.WPTE.2015.47,
  author =	{Smetsers, Sjaak and Madlener, Ken and van Eekelen, Marko},
  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 =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-94-1},
  ISSN =	{2190-6807},
  year =	{2015},
  volume =	{46},
  editor =	{Chiba, Yuki and Escobar, Santiago and Nishida, Naoki and Sabel, David and Schmidt-Schau{\ss}, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/OASIcs.WPTE.2015.47},
  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}
}
  • Refine by Author
  • 1 Madlener, Ken
  • 1 Smetsers, Sjaak
  • 1 van Eekelen, Marko

  • Refine by Classification

  • Refine by Keyword
  • 1 PVS
  • 1 WHILE
  • 1 adequacy
  • 1 bialgebras
  • 1 denotational semantics
  • Show More...

  • Refine by Type
  • 1 document

  • Refine by Publication Year
  • 1 2015

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact