Reactor Model
This repository contains a Lean-based formalization of the Reactor model - a model of computation underlying the Lingua Franca language.
Resources
The paper Provable Determinism for Software in Cyber-Physical Systems explains the formalization at a high level. While this formalization differs quite significantly from previous work, the following list contains relevant literature covering the Reactor model: