Alpha v0.1
Pre-release
Pre-release
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