A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics | Zendy

Sabine Glesner | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

A Proof Calculus for Natural Semantics Based on Greatest Fixed Point Semantics

Author(s) -

Sabine Glesner

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2005.02.011

Subject(s) - denotational semantics , semantics (computer science) , correctness , computer science , mathematical proof , programming language , operational semantics , action semantics , interpretation (philosophy) , compiler , formal semantics (linguistics) , fixed point , well founded semantics , axiomatic semantics , calculus (dental) , theoretical computer science , mathematics , medicine , mathematical analysis , geometry , dentistry

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research