@conference{,
  author={Sabine Glesner},
  title=\{A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics},
  booktitle=\{Proceedings of the COCV-Workshop (Compiler Optimization meets Compiler Verification), 7th European Conferences on Theory and Practice of Software (ETAPS 2004)},
  year=\{2004},
  month=\{April},
  publisher=\{Elsevier, Electronic Notes in Theoretical Computer Science (ENTCS)},
  abstract=\{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.},
}