Skip to content

Latest commit

 

History

History
27 lines (22 loc) · 1.17 KB

README.md

File metadata and controls

27 lines (22 loc) · 1.17 KB
Raw

ConCert embedding

This subfolder contains the development of an embedding of the functional programming language λsmart into Coq.

Some highlights

  • theories/Ast.v contains the definition of the λsmart language.

  • theories/EvalE.v contains an interpreter for λsmart language.

  • theories/pcuic/ contains translation from λsmart expression to PCUIC terms, proof of soundness and various auxiliary lemmas for that proof.

  • examples/ contains examples of smart contract verification: verification of Acorn list functions, and integration with the blockchain execution framework.

  • 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.

  • examples/ExecFrameworkIntegration.v is an "end-to-end" example of writing a smart contract in λsmart, translating it to Gallina, and integrating it with the execution framework and proving safety properties about it.