The While language
Cl\'audio Vasconcelos, Ant\'onio Ravara

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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems
