Skip to content

Releases: CharlesAverill/volpic

Alpha v0.1

07 Feb 14:39
Compare
Choose a tag to compare
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