π: Towards a Simple Formal Semantic Framework for Compiler Construction

2018/05/12 by Christiano Braga, Braga, Christiano
Computer Science · #Logic, programming, and type systems #Formal Methods in Verification #Parallel Computing and Optimization Techniques

paper · pdf · doi:10.48550/arxiv.1805.04650

Abstract

This paper proposes π, a formal semantic framework for compiler construction together with program validation. π is comprised by π Lib, a set of programming languages constructs inspired by Peter Mosses' Component-Based Semantics and π Automata, an automata-based formalism to describe the operational semantics of programming languages, that generalizes Gordon Plotkin's Interpreting Automata.

Related

• Operational methods in semantics
• Pyrosome: Verified Compilation for Modular Metatheory
• A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs
• A DENOTATIONAL ENGINEERING OF PROGRAMMING LANGUAGES to make software systems reliable and user manuals clear, complete and unambiguous. A book in statu nascendi
• Formal certification of a compiler back-end or