An Executable Structural Operational Formal Semantics for Python
Maximilian A. K\"ohl

TL;DR
This paper develops an executable formal semantics for Python using structural operational semantics, enabling sound static analysis and automated interpreter derivation for the language.
Contribution
It introduces a meta-theoretic framework for formalizing structural operational semantics and applies it to Python, facilitating static analysis and interpreter automation.
Findings
Created a formal semantics for Python
Developed a tool-supported framework for semantics formalization
Validated the approach for modern programming languages
Abstract
Python is a popular high-level general-purpose programming language also heavily used by the scientific community. It supports a variety of different programming paradigms and is preferred by many for its ease of use. With the vision of harvesting static analysis techniques like abstract interpretation for Python, we develop a formal semantics for Python. A formal semantics is an important cornerstone for any sound static analysis technique. We base our efforts on the general framework of structural operational semantics yielding a small-step semantics in principle allowing for concurrency and interaction with an environment. The main contributions of this thesis are twofold: first, we develop a meta-theoretic framework for the formalization of structural operational semantics in tandem with the necessary tool support for the automated derivation of interpreters from such formal…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputational Physics and Python Applications · Scientific Computing and Data Management · Parallel Computing and Optimization Techniques
