Reactor Model
This repository contains a Lean-based formalization of the Reactor model - a model of computation underlying the Lingua Franca language.
Resources
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
Project Structure
ReactorModel/Objects contains definitions and proofs about reactor objects.
ReactorModel/Execution contains definitions and proofs for the execution model. Notably Execution/Theorems/Execution.lean contains the theorem of determinism and Execution/Theorems/Progress.lean the progress theorem.