{\pi}: Towards a Simple Formal Semantic Framework for Compiler Construction

TL;DR

This paper introduces { extpi}, a formal semantic framework for compiler construction and program validation, combining component-based semantics and automata-based formalism to improve language description and correctness proofs.

Contribution

It presents { extpi}, a novel framework integrating component-based semantics with automata, enhancing formal language description and compiler validation methods.

Findings

{ extpi} simplifies semantic descriptions of programming languages.

It generalizes existing automata-based semantics for better expressiveness.

The framework supports rigorous compiler correctness proofs.

Abstract

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