From 3b8e1a81a1208b112a174e7f2ecdd2752ebc3bcd Mon Sep 17 00:00:00 2001 From: Bas Spitters Date: Wed, 28 Apr 2021 07:48:52 +0200 Subject: [PATCH] Update README.md --- embedding/README.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/embedding/README.md b/embedding/README.md index 9014e7ec..9c04a802 100644 --- a/embedding/README.md +++ b/embedding/README.md @@ -12,16 +12,16 @@ language. * [theories/pcuic/](theories/pcuic/) contains translation from ``λsmart`` expression to PCUIC terms, proof of soundness and various auxiliary lemmas for that proof. -* [theories/examples/](theories/examples/) contains examples of smart contract +* [examples/](examples/) contains examples of smart contract verification: the crowdfunding contract, verification of ``Acorn`` list functions, integration with the execution framework. -* [theories/examples/Demo.v](theories/examples/Demo.v) contains a demonstration +* [examples/Demo.v](examples/Demo.v) contains a demonstration using our framework to write definitions using the deep embedding, convert them to Coq functions, compute with the interpreter and prove simple properties using the shallow embedding. -* [theories/examples/ExecFrameworkIntegration.v](theories/examples/ExecFrameworkIntegration.v) +* [examples/ExecFrameworkIntegration.v](examples/ExecFrameworkIntegration.v) is an "end-to-end" example of writing a contract in ``λsmart``, translating it to Gallina, and integrating it with the execution framework to prove safety properties about it.