Working with Operational Semantics as a Programming Language
Authors
Hyberts, Sebastian Hjorth ; Frederiksen, Kári
Term
4. term
Education
Publication year
2022
Submitted on
2022-06-17
Pages
27
Abstract
Når vi beskriver, hvordan programmer kører, skriver vi ofte regelsæt kaldet specifikationer for Strukturel Operationel Semantik (SOS). Hvis vi behandler disse specifikationer som et egentligt programmeringssprog, kan vi bruge de samme automatiske analyseteknikker, som normalt anvendes i forskning i programmeringssprog. Denne afhandling præsenterer et typesystem, der ved hjælp af unifikation kontrollerer, at specifikationerne er veltypede. Derudover anvendes grafbaserede analyser til at sikre, at variabelbindinger og præmisser i reglerne er ordnet på en logisk og afhængighedsrespekterende måde. Tilsammen åbner dette for forskning i, hvilken rolle et kompiler-lignende værktøj kan spille i undervisning og arbejde med specifikationer af operationel semantik.
When we describe how programs run, we often write rule-based descriptions called specifications of Structural Operational Semantics (SOS). If we treat these specifications as a programming language in their own right, we can apply the same automated analysis techniques commonly used in programming language research. This paper presents a type system that uses unification to check that specifications are well-typed. It also applies graph-based analyses to ensure that variable bindings and rule premises are ordered in a logical, dependency-respecting way. Together, these ideas open up research into the role of compiler-like tools for learning and working with specifications of operational semantics.
[This abstract was generated with the help of AI]
Keywords
Documents