An implementation of the IMP toy language in Coq with two proofs. The code is documented (in italian), you can generate the documentation with coqdoc.
-
Notifications
You must be signed in to change notification settings - Fork 1
zagoli/ImpCoq
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
An implementation of the IMP language in Coq with two proofs.