Skip to content

Alpha v0.1

Pre-release
Pre-release
Compare
Choose a tag to compare
@CharlesAverill CharlesAverill released this 07 Feb 14:39
· 20 commits to main since this 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