Commit 2cfc4c73 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' into new_heap_lang

parents 274250ae 769903ca
...@@ -92,6 +92,8 @@ Important modules are highlighted. ...@@ -92,6 +92,8 @@ Important modules are highlighted.
time credits, that does not rely on the unsafe behavior of `tick`__ time credits, that does not rely on the unsafe behavior of `tick`__
* __`TimeReceipts`: interface, implementation, and proof of soundness for time * __`TimeReceipts`: interface, implementation, and proof of soundness for time
receipts (both exclusive and persistent)__ receipts (both exclusive and persistent)__
* __`Combined`: logical system providing both time credits and time receipts
at the same time__
* `Examples`: a very simple example illustrating the use of time credits to * `Examples`: a very simple example illustrating the use of time credits to
specify a program with lists specify a program with lists
* __`Thunks`: implementation of timed thunks using time credits__ * __`Thunks`: implementation of timed thunks using time credits__
......
...@@ -21,6 +21,7 @@ theories/Thunks.v ...@@ -21,6 +21,7 @@ theories/Thunks.v
theories/TimeCredits.v theories/TimeCredits.v
theories/TimeCreditsAltProofs.v theories/TimeCreditsAltProofs.v
theories/TimeReceipts.v theories/TimeReceipts.v
theories/Combined.v
theories/Translation.v theories/Translation.v
theories/union_find/math/Ackermann.v theories/union_find/math/Ackermann.v
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment