Reactive Semantics for User Interface Description Languages

TL;DR

This paper introduces a formal denotational semantics model for a core reactive User Interface Description Language, aiming to enhance the formalization and verification of safety-critical GUIs.

Contribution

It proposes a denotational semantic model for a reactive UIDL, facilitating formal verification and potential development of verified compilers.

Findings

Model is expressive enough for realistic languages

Provides a foundation for formal verification of UIDLs

Enables future verified compiler development

Abstract

User Interface Description Languages (UIDLs) are high-level languages that facilitate the development of Human-Machine Interfaces, such as Graphical User Interface (GUI) applications. They usually provide first-class primitives to specify how the program reacts to an external event (user input, network message), and how data flows through the program. Although these domain-specific languages are now widely used to implement safety-critical GUIs, little work has been invested in their formalization and verification. In this paper, we propose a denotational semantic model for a core reactive UIDL, Smalite, which we argue is expressive enough to encode constructs from more realistic languages. This preliminary work may be used as a stepping stone to produce a formally verified compiler for UIDLs.