Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329288 | Electronic Notes in Theoretical Computer Science | 2005 | 21 Pages |
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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Sabine Glesner,