Skip to content

mit-plv/certifying-derivation-of-state-machines-from-coroutines

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

86 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Coq version exactly v8.9.1 is needed to build this development. Once you have installed it, you can build the coq files by running make in the root directory and the haskell wrapper by running stack build in the directory hs. For more information on this codebase, please see the artifact description at https://zenodo.org/record/5553451

A tutorial on using our compiler: src/Example.v