Skip to Main content Skip to Navigation
Reports

Recursive Operator Definitions

Abstract : TLA+ originally allowed recursive function definitions, but not recursive operator definitions, because it was not known how how to define their semantics. They were added to the language in 2006 after we discovered a semantics for them. We describe that semantics here.
Complete list of metadata

Cited literature [2 references]  Display  Hide  Download

https://hal.inria.fr/hal-02598330
Contributor : Georges Gonthier <>
Submitted on : Friday, May 15, 2020 - 11:36:30 PM
Last modification on : Saturday, May 1, 2021 - 3:36:20 AM

File

RR-9341.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-02598330, version 1

Citation

Georges Gonthier, Leslie Lamport. Recursive Operator Definitions. [Research Report] RR-9341, Inria Saclay Ile de France. 2020, pp.17. ⟨hal-02598330⟩

Share

Metrics

Record views

53

Files downloads

348