Reactor Model

This repository contains a Lean-based formalization of the Reactor model - a model of computation underlying the Lingua Franca language.


While this formalization differs quite significantly from previous work, the following list contains relevant literature covering the Reactor model.

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.