Skip to content

stelleg/cem_coq

BranchesTags

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

47 Commits
.gitignore
.gitignore
 
 
CpdtTactics.v
CpdtTactics.v
 
 
JRWTactics.v
JRWTactics.v
 
 
README.md
README.md
 
 
assembly.v
assembly.v
 
 
build.hs
build.hs
 
 
cbn.v
cbn.v
 
 
cbn_cem.v
cbn_cem.v
 
 
cem.v
cem.v
 
 
cem_cesm.v
cem_cesm.v
 
 
cem_name.v
cem_name.v
 
 
cesm.v
cesm.v
 
 
cesm_im.v
cesm_im.v
 
 
compiler.v
compiler.v
 
 
curien.v
curien.v
 
 
curien_cem_name.v
curien_cem_name.v
 
 
db.v
db.v
 
 
db_assembly.v
db_assembly.v
 
 
expr.v
expr.v
 
 
expr_db.v
expr_db.v
 
 
im.v
im.v
 
 
machine.v
machine.v
 
 
relations.v
relations.v
 
 
set.v
set.v
 
 
util.v
util.v
 
 

Repository files navigation

% Verifiably Lazy : A Verified Compiler for Call-By-Need.

Building / Proof Checking

Requirements:

  • coqc and coqdep (tested with 8.4)
  • runhaskell and Shake

To Build: ./build.hs (requires runhaskell and Shake, the Haskell build system)

Notes: We use the convention that filenames correspond to that datatype and theorems , supporting datatypes, transitions for those datatypes, while filenames with underscores, e.g. c1_c2.v represents the connections between c1 and c2.

About

Coq implemenation of CEM with proof of correctness

Resources

Readme
Activity

Stars

3 stars

Watchers

3 watching

Forks

0 forks
Report repository

Releases

1 tags

Packages

No packages published

Languages