Document Open Access Logo

Formalizing Bialgebraic Semantics in PVS 6.0

Authors Sjaak Smetsers, Ken Madlener, Marko van Eekelen

PDF
Thumbnail PDF

File

OASIcs.WPTE.2015.47.pdf
  • Filesize: 0.53 MB
  • 15 pages

Document Identifiers

Author Details

Sjaak Smetsers
Ken Madlener
Marko van Eekelen

Cite AsGet BibTex

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)
https://doi.org/10.4230/OASIcs.WPTE.2015.47

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.
Keywords
  • operational semantics
  • denotational semantics
  • bialgebras
  • distributive laws
  • adequacy
  • theorem proving
  • PVS
  • WHILE

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Michael Barr and Charles Wells. Category theory for computing science, volume 49. Prentice Hall New York, 1990. Google Scholar
  2. Falk Bartels. On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004. Google Scholar
  3. Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can't be traced. J. ACM, 42(1):232-268, January 1995. Google Scholar
  4. Marcello M Bonsangue, Helle Hvid Hansen, Alexander Kurz, and Jurriaan Rot. Presenting distributive laws. In Algebra and Coalgebra in Computer Science, LNCS, pages 95-109. Springer, 2013. Google Scholar
  5. Ben Delaware, Bruno C.d.S. Oliveira, and Tom Schrijvers. Meta-theory à la carte. In Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '13, New York, NY, USA, 2013. ACM. Google Scholar
  6. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99, pages 193-202, Washington, DC, USA, 1999. IEEE Computer Society. Google Scholar
  7. Marcelo Fiore and Sam Staton. A congruence rule format for name-passing process calculi from mathematical structural operational semantics. In Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, LICS '06, pages 49-58, Washington, DC, USA, 2006. IEEE Computer Society. Google Scholar
  8. Ulrich Hensel and Bart Jacobs. Coalgebraic theories of sequences in pvs. J. Log. Comput., 9(4):463-500, 1999. Google Scholar
  9. Ralf Hinze and Daniel W.H. James. Proving the unique fixed-point principle correct: an adventure with category theory. SIGPLAN Not., 46(9):359-371, September 2011. Google Scholar
  10. Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:62-222, 1997. Google Scholar
  11. Mauro Jaskelioff, Neil Ghani, and Graham Hutton. Modularity and implementation of mathematical operational semantics. Electron. Notes Theor. Comput. Sci., 229(5):75-95, March 2011. Google Scholar
  12. Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. CMCS Tenth Anniversary Meeting. Google Scholar
  13. Sheng Liang, Paul Hudak, and Mark Jones. Monad transformers and modular interpreters. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '95, pages 333-343, New York, NY, USA, 1995. ACM. Google Scholar
  14. Ken Madlener and Sjaak Smetsers. GSOS formalized in Coq. In The 7th International Symposium on Theoretical Aspects of Software Engineering (TASE2013), pages 199-206, 2013. Birmingham, UK, 2013. IEEE. Google Scholar
  15. Ken Madlener, Sjaak Smetsers, and Marko C. J. D. van Eekelen. Formal component-based semantics. In Michel A. Reniers and Pawel Sobocinski, editors, SOS, volume 62 of EPTCS, pages 17-29, 2011. Google Scholar
  16. Erik Meijer, Maarten M. Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, pages 124-144, London, UK, UK, 1991. Springer-Verlag. Google Scholar
  17. Hanne Riis Nielson and Flemming Nielson. Semantics with applications: a formal introduction. John Wiley &Sons, Inc., New York, NY, USA, 1992. Google Scholar
  18. Daniele Turi and Gordon Plotkin. Towards a mathematical operational semantics. In Proceedings of the 12th Annual IEEE Symposium on Logic in Computer Science, LICS '97, pages 280-291, Washington, DC, USA, 1997. IEEE Computer Society. Google Scholar
  19. Philip Wadler. Theorems for free! In Functional Programming Languages And Computer Architecture, pages 347-359. ACM Press, 1989. Google Scholar
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