---
title: "The Synchronous Data Flow Programming Language LUSTRE"
authors:
  - "Nicolas Halbwachs"
  - "Paul Caspi"
  - "Pascal Raymond"
  - "Daniel Pilaud"
year: 1991
venue: "Proceedings of the IEEE 79(9):1305-1320"
arxiv: null
doi: "10.1109/5.97300"
source: "https://homepage.cs.uiowa.edu/~tinelli/classes/181/Spring08/Papers/Halb91.pdf"
topics:
  - synchronous-languages
  - dataflow
  - clock-calculus
  - reactive-systems
  - standing-rules
seed_rank: 2399
seed_batch: "archive-2026-10-24"
reviewed: "2026-10-24"
pool: "languages"
relevance_score: 8
lineage: programming-language-foundations
see:
  - 1853-commit-window-observation-contracts-for-reactive-ecs
  - 016-deterministic-lockstep
  - 1489-dbsp-automatic-incremental-view-maintenance-for-rich-query-languages
  - 2356-teleo-reactive-programs-for-agent-control
cites:
  - title: "The Synchronous Data Flow Programming Language LUSTRE"
    url: "https://doi.org/10.1109/5.97300"
    year: 1991
    arxiv: null
    doi: "10.1109/5.97300"
---

# The Synchronous Data Flow Programming Language LUSTRE

## One-sentence takeaway

Lustre makes every variable a flow (a sequence of values on a clock), defines each one by exactly one equation built from pointwise operators plus `pre` (previous value), `->` (initial value, then), `when` (sample onto a slower clock) and `current` (hold onto the faster clock), rejects any cycle without a `pre` and any mixing of clocks, and compiles the whole node into one bounded-memory loop body (or a finite automaton) — with safety properties written in the same language as observer flows that must stay true.

## Why it matters here

ano's standing rules (する/なる) are tick-indexed equations over columns: "this value is defined from last tick's values and this tick's inputs." Lustre is the canonical design for exactly that: single definition per variable, order-independent equations, `pre` as the only way to reach back in time, a static check that every dependency cycle passes through a `pre`, and a clock calculus that refuses programs whose memory would grow without bound. Those are the rules ano needs so that a set of standing rules compiles to one deterministic per-tick schedule — which is also what GRID COMMAND's lockstep simulation requires.

## Key ideas

- **Flows and the basic clock.** Every variable and expression is a sequence of values with a clock; the program's cycle defines the basic clock, and slower clocks are defined by boolean flows.
- **Equations, not assignments.** Each local and output variable has one and only one definition; by the substitution principle equations can be written in any order and subexpressions can be named without changing meaning.
- **Four temporal operators.** `pre(E)` is the previous value of E (nil at the first instant); `E -> F` is E at the first instant and F afterwards; `E when B` samples E onto the clock defined by B; `current E` interpolates back to the faster clock, holding the last sampled value.
- **Static checks.** Definition checking, no recursive node calls (static networks only), clock consistency, no uninitialised values reaching clocks, outputs or assertions, and no cyclic definitions — every cycle must contain a `pre`. Structurally cyclic but semantically safe programs are also rejected because the general analysis is undecidable.
- **Clock calculus.** `y = x + (x when b)` is rejected: it would combine values from instants n and 2n and need unbounded memory. Clocks are equal only if they unify syntactically.
- **Compilation.** Called nodes are expanded recursively before compilation (the paper notes some separate compilation is possible), then compiled either to a single loop body ordered by dependencies or to a finite automaton whose states are the boolean memories, with transitions labelled by straight-line code; output in the OC format shared with Esterel.
- **Verification.** A safety property is a Lustre node whose boolean output must always be true (e.g. `onceBfromAtoC` built from `never` and `since`); to prove B invariant, compile a program whose only output is B and check that no state of its control automaton assigns false — the compiler only keeps the part of the program B depends on, and assertions express environment assumptions. Most critical properties of a nuclear plant monitoring program were expressed this way.

## Caveats

1991 language: static networks only (no recursion or dynamic process creation), automata generated by the compiler are often far from minimal and can blow up, and the "same clock" rule is purely syntactic. Arrays are not covered. Verification works on the boolean control automaton, an abstraction that ignores most numeric state unless assertions supply it. Synchronous semantics assume each cycle finishes before the next input; ano still needs its own story for cost bounds per tick.

## Links

- Paper (course mirror PDF): https://homepage.cs.uiowa.edu/~tinelli/classes/181/Spring08/Papers/Halb91.pdf
- Paper (HAL open archive): https://hal.science/hal-05028988v1
- Paper (DOI, Proceedings of the IEEE): https://doi.org/10.1109/5.97300