h: A Plank for Higher-order Attribute Contraction Schemes

TL;DR

This paper introduces and formalizes 'h', a core calculus designed to underpin advanced compiler specification languages, ensuring well-defined rewriting with powerful variable and environment manipulation features.

Contribution

The paper's main contribution is the formalization of 'h', a foundational calculus enabling complex rewriting and variable handling in compiler specification languages.

Findings

Formalization of 'h' as a core calculus for compiler languages

Introduction of typing and formation rules for well-defined rewriting

Support for manipulating free variables and environments as first-class elements

Abstract

We present and formalize h, a core (or "plank") calculus that can serve as the foundation for several compiler specification languages, notably CRSX (Combinatory Reductions Systems with eXtensions), HACS (Higher-order Attribute Contraction Schemes), and TransScript. We discuss how the h typing and formation rules introduce the necessary restrictions to ensure that rewriting is well-defined, even in the presence of h's powerful extensions for manipulating free variables and environments as first class elements (including in pattern matching).