Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Explore a 16-minute conference presentation introducing Pyrosome, a groundbreaking generic framework for modular language metatheory that revolutionizes extensible semantics and compilation through implementation in Coq. Discover how this novel approach addresses fundamental limitations in semantic reasoning by moving beyond techniques tied to specific language structures, overcoming challenges with contextual equivalence and fixed global effect notions that restrict semantic extension and composition. Learn about Pyrosome's fully extensible verified compilers that enable language extension through simple definition and verification of new feature compilation while reusing existing correctness theorems for all other cases. Understand the innovative inductive formulation of equivalence preservation that supports adding new rules to source languages, target languages, and compilers simultaneously. Examine how Pyrosome defines programming languages through dependently sorted equational theories, reducing all compiler-correctness proofs to type-checking and equational reasoning while supporting vertical composition of framework-expressed compilers and feature extension. Investigate the framework's support for open programs and linking guarantees with appropriately typed target code. Follow a comprehensive case study demonstrating a multipass compiler from System F with simple references through CPS translation and closure conversion, showcasing incremental compiler construction starting from simply typed lambda-calculus and progressively adding natural numbers, unit types, recursive functions, global heap, type environments, and type abstraction. Witness practical applications including a linear version of the simply typed CPS pass and compilation of imperative languages to simply typed targets, illustrating Pyrosome's handling of substructural typing and imperative features.
