Skip to content

Latest commit

 

History

History
 
 

embedding

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 
 
 
 
 
 
 
 
 
 
 
 
 

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.