  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.
