Submitted: September 2024
Abstract
PseuCo is an imperative programming language, used in the lecture concurrent programming as an educational tool to teach concurrency to students. As of writing this, pseuCo has three implementations that all differ in some subtle ways. To clear up ambiguities and even find problems in the language, we provide a formal basis for pseuCo using inference rules. Two sets of rules, one for typechecking and one for execution, are created to define pseuCo’s semantics in a formal way. With those, it shall be possible to derive a program on paper. By doing so, all unclear or undefined parts of the language that disappear behind an implementation, are formally defined, and can be reasoned about. The goal is not to make THE semantics for pseuCo but to provide a first iteration and framework for the language.