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:

• Reactors: A Deterministic Model of Concurrent Computation for Reactive Systems (Lohstroh 2020)
• Reactors: A Deterministic Model for Composable Reactive Systems (Lohstroh et al. 2019)
• List of related publications by the Lingua Franca community