Releases: CharlesAverill/volpic
Releases · CharlesAverill/volpic
Alpha v0.1
The first public release of VOLPIC, supporting the following:
Pascal to Coq Lifter
- Basic integer arithmetic
- Builtin FPC IO functions
- Loops
- Array accesses
Coq to OCaml Extraction
- All above features
- Basic IO
Theorem Library
- Basic theorems about store read/writes