The Operational Semantics and Implementation of a Core Dart language

In this report we present the specification of the operational semantics of Dart Kernel and a reference implementation of Dart Kernel in Dart. We design a CESK-like machine to specify the operational semantics of Dart Kernel and we implement an interpreter that follows closely the small-step semantics of the language. This approach allows us to define the behaviour of the rich features of Dart Kernel, such as exception handling and asynchronous execution. Since Dart Kernel is an evolving language, the specification is expected to evolve with it and the semantics for new features needs to be defined further. The work done for this project sets the grounds for further formalization of the behaviour of the language with a formal proof management system, as Coq.