tchajed/coq-tla
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
No description
228 commits 2 branches 0 tags 418 KiB
  • Rocq Prover 99%
  • Makefile 0.6%
  • Shell 0.4%
Find a file
Exact
Tej Chajed 887bb3719b
 Update dependencies
2024-03-04 16:40:07 -06:00
.github/workflows Update build workflow 2023-11-02 11:14:42 -05:00
etc Generalize depgraph.sh to take a library name 2022-11-07 16:03:18 -08:00
external Update dependencies 2024-03-04 16:40:07 -06:00
src Add the same restatement for strong fairness 2023-12-05 08:28:58 -06:00
.gitignore Ignore .coq-native directories 2023-03-16 10:09:39 -07:00
.gitmodules Start writing a simple controller-like example 2022-09-28 15:38:59 -07:00
_CoqProject Start writing a simple controller-like example 2022-09-28 15:38:59 -07:00
Makefile Use alectryon caching 2022-10-01 11:24:39 -07:00
README.md Expand documentation in hello_liveness 2022-10-01 11:18:47 -07:00

README.md

TLA in Coq

CI

Embedding TLA in Coq. The goal is to better understand how TLA can be used for liveness reasoning, by playing around with the proof system and trying out small examples. Automation is just adequate here to get work done, but not suitable for large systems or complex temporal reasoning with many hypotheses.

Documentation compiled with Alectryon is automatically generated. Some good places to start are the basic definitions and a simple example of liveness for a toy transition system.

The TLA definitions and rules owe a lot to the classic paper "The Temporal Logic of Actions".