The While language

TL;DR

This paper formalizes a simple imperative programming language called 'The While language,' including its syntax, semantics, and type system, with an implementation in Racket for practical experimentation.

Contribution

It provides a comprehensive formal specification and an executable implementation of the language's semantics and type system, facilitating hands-on study and validation.

Findings

Formal syntax and semantics defined

Executable implementation in Racket created

Supports studying language properties and behaviors

Abstract

This article presents a formalisation of a simple imperative programming language. The objective is to study and develop "hands-on" a formal specifcation of a programming language, namely its syntax, operational semantics and type system. To have an executable version of the language, we implemented in Racket its operational semantics and type system.