@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.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} }