TY - GEN
T1 - Fundamental Constructs in Programming Languages
AU - Mosses, Peter D.
PY - 2021
Y1 - 2021
N2 - When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons), compositionally. In contrast to the informal explanations commonly found in reference manuals, such formal specifications of translations to funcons can be precise and complete. They are also easy to write and read, and to update when the language evolves. The PLanCompS project has developed a large collection of funcons. Each funcon is defined independently, using a modular variant of structural operational semantics. The definitions are available online, along with tools for generating funcon interpreters from them. This paper introduces and motivates funcons. It illustrates translation of language constructs to funcons, and funcon definition. It also relates funcons to the notation used in some previous language specification frameworks, including monadic semantics and action semantics.
AB - When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons), compositionally. In contrast to the informal explanations commonly found in reference manuals, such formal specifications of translations to funcons can be precise and complete. They are also easy to write and read, and to update when the language evolves. The PLanCompS project has developed a large collection of funcons. Each funcon is defined independently, using a modular variant of structural operational semantics. The definitions are available online, along with tools for generating funcon interpreters from them. This paper introduces and motivates funcons. It illustrates translation of language constructs to funcons, and funcon definition. It also relates funcons to the notation used in some previous language specification frameworks, including monadic semantics and action semantics.
KW - Formal specification
KW - Funcons
KW - Programming constructs
UR - http://www.scopus.com/inward/record.url?scp=85118183596&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-89159-6_19
DO - 10.1007/978-3-030-89159-6_19
M3 - Conference contribution
AN - SCOPUS:85118183596
SN - 9783030891589
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 296
EP - 321
BT - Leveraging Applications of Formal Methods, Verification and Validation - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021, Proceedings
A2 - Margaria, Tiziana
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Science+Business Media
T2 - 10th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2021
Y2 - 17 October 2021 through 29 October 2021
ER -