direkt zum Inhalt springen

direkt zum Hauptnavigationsmenü

Sie sind hier

TU Berlin

Inhalt des Dokuments


A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics
Zitatschlüssel glesner04a
Autor Sabine Glesner
Buchtitel Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004)
Seiten 73 - 93
Jahr 2004
Adresse Barcelona, Spain
Jahrgang Vol. 132 (2005)
Monat Apr
Verlag Elsevier, Electronic Notes in Theoretical Computer Science (ENTCS)
Zusammenfassung Formal semantics of programming languages needs to model the potentially infinite state transition behavior of programs as well as the computation of their final results simultaneously. This requirement is essential in correctness proofs for compilers. We show that a greatest fixed point interpretation of natural semantics is able to model both aspects equally well. Technically, we infer this interpretation of natural semantics based on an easily omprehensible introduction to the dual definition and proof principles of induction and coinduction. Furthermore, we develop a proof calculus based on it and demonstrate its application for two typical problems.
Typ der Publikation Conference Article
Download Bibtex Eintrag

Zusatzinformationen / Extras


Schnellnavigation zur Seite über Nummerneingabe