## 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.