diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-08-30 17:57:09 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-05 13:52:54 +0200 |
| commit | e8dc5a7222dbb81306883e4f19eb5b0c33b0d5e0 (patch) | |
| tree | a8ceae36fc63fa5b9eea76c36022143d41bb6650 /backend/Selectionproof.v | |
| parent | 91f21889423c41bb46b8b25b510c71987cf6006b (diff) | |
| download | compcert-e8dc5a7222dbb81306883e4f19eb5b0c33b0d5e0.tar.gz compcert-e8dc5a7222dbb81306883e4f19eb5b0c33b0d5e0.zip | |
Introducing the "eventually" closure and new simulation diagrams using it
These diagrams enable the source program to make a number of finite
transitions before eventually reaching a state that restores the
simulation relation.
Diffstat (limited to 'backend/Selectionproof.v')
0 files changed, 0 insertions, 0 deletions