We are setting out to build a prototype formally verified database system. Formal verification is a technique of mathematically proving certain functionality and algorithms. Essentially pre and post conditions are represented as mathematical theorems and proven with a mechanical proof solving system. The core system would be built in Coq and compiled down to OCaml. I/O and command parsing will be written in OCaml.
-
Notifications
You must be signed in to change notification settings - Fork 0
CornellDataScience/FormalDB
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
About
FormalDB is a prototype database management system built in Gallina, verified in Coq. This repo has an expanded OCaml layer and a further expanded Node.js layer for GUI use
Resources
Stars
Watchers
Forks
Releases
No releases published
Packages 0
No packages published