×

Formalizing bialgebraic semantics in PVS 6.0. (English) Zbl 1428.68179

Chiba, Yuki (ed.) et al., Second international workshop on rewriting techniques for program transformations and evaluation, WPTE’15, Warsaw, Poland, July 2, 2015. Proceedings. Wadern: Schloss Dagstuhl – Leibniz Zentrum für Informatik. OASIcs – OpenAccess Ser. Inform. 46, 47-61 (2015).
Summary: 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.
For the entire collection see [Zbl 1329.68023].

MSC:

68Q55 Semantics in the theory of computing
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68V20 Formalization of mathematics in connection with theorem provers

Software:

PVS
PDFBibTeX XMLCite
Full Text: DOI

References:

[2] Falk Bartels. On generalised coinduction and probabilistic specification formats. PhD thesis, CWI, Amsterdam, April 2004.
[3] Bard Bloom, Sorin Istrail, and Albert R. Meyer. Bisimulation can’t be traced. J. ACM, 42(1):232-268, January 1995. · Zbl 0886.68027
[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. · Zbl 1394.68238
[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 pro- gramming languages, POPL ’13, New York, NY, USA, 2013. ACM. · Zbl 1301.68218
[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.
[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. · Zbl 1101.68697
[8] Ulrich Hensel and Bart Jacobs. Coalgebraic theories of sequences in pvs. J. Log. Comput., 9(4):463-500, 1999. · Zbl 0940.68084
[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. · Zbl 1323.68211
[10] Bart Jacobs and Jan Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:62-222, 1997. · Zbl 0880.68070
[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. · Zbl 1291.68123
[12] Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theoretical Computer Science, 412(38):5043-5069, 2011. CMCS Tenth Anniversary Meeting. · Zbl 1246.68150
[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.
[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.
[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. · Zbl 1405.68175
[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.
[17] Hanne Riis Nielson and Flemming Nielson. Semantics with applications: a formal intro- duction. John Wiley & Sons, Inc., New York, NY, USA, 1992. · Zbl 0875.68626
[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.
[19] Philip Wadler. Theorems for free! In Functional Programming Languages And Computer Architecture, pages 347-359. ACM Press, 1989.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.