SLE 2023 paper:
An Executable Semantics for Faster Development of Optimizing Python Compilers

Olivier Melançon, Marc Feeley, Manuel Serrano

DOI: 10.1145/3623476.3623529
T1C: Behavioural Semantics
- The main contribution is an executable (formal) semantics for Python that serves as a reference for understanding and implementing the language.
T4C: Vertical Transformation
- The semantics is used to speed up development of optimizing compilers, i.e., downstream compilation and refinement pipelines.
T5D: Formal Methods
- The work is grounded in semantic specification/validation techniques typical of formal methods for programming languages.

The page is maintained by Dr. Vadim Zaytsev a.k.a. @grammarware. Last updated: June 2026.