GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → mit-plv → Fiat

mit-plv / Fiat

Licence: other
Mostly Automated Synthesis of Correct-by-Construction Programs

Labels

coq

Projects that are alternatives of or similar to Fiat

Certicoq
A Verified Compiler for Gallina, Written in Gallina
Stars: ✭ 66 (-44.54%)
Mutual labels:  coq
Ttlite
A SuperCompiler for Martin-Löf's Type Theory
Stars: ✭ 94 (-21.01%)
Mutual labels:  coq
Ergo
The Language for Smart Legal Contracts
Stars: ✭ 108 (-9.24%)
Mutual labels:  coq
Ch2o
Stars: ✭ 75 (-36.97%)
Mutual labels:  coq
Fourcolor
Formal proof of the Four Color Theorem
Stars: ✭ 87 (-26.89%)
Mutual labels:  coq
Coq Pipes
Stars: ✭ 101 (-15.13%)
Mutual labels:  coq
Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Stars: ✭ 65 (-45.38%)
Mutual labels:  coq
Iron
Coq formalizations of functional languages.
Stars: ✭ 114 (-4.2%)
Mutual labels:  coq
Coq Serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Stars: ✭ 87 (-26.89%)
Mutual labels:  coq
Ceramist
Verified hash-based AMQ structures in Coq
Stars: ✭ 107 (-10.08%)
Mutual labels:  coq
Disel
Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations in Coq
Stars: ✭ 85 (-28.57%)
Mutual labels:  coq
Vscoq
Coq Support for Visual Studio Code
Stars: ✭ 85 (-28.57%)
Mutual labels:  coq
Coq Ext Lib
A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
Stars: ✭ 102 (-14.29%)
Mutual labels:  coq
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-37.82%)
Mutual labels:  coq
Coqtail
Interactive Coq Proofs in Vim
Stars: ✭ 109 (-8.4%)
Mutual labels:  coq
Sfja
SoftwareFoundations(Ja)
Stars: ✭ 65 (-45.38%)
Mutual labels:  coq
Peacoq
PeaCoq is a pretty Coq, isn't it?
Stars: ✭ 99 (-16.81%)
Mutual labels:  coq
Coq Of Ocaml
Import OCaml programs to Coq 🐓 🐫
Stars: ✭ 117 (-1.68%)
Mutual labels:  coq
Awesome Provable
A curated set of links to formal methods involving provable code.
Stars: ✭ 111 (-6.72%)
Mutual labels:  coq
Mindless Coding
Mindless, verified (erasably) coding using dependent types
Stars: ✭ 104 (-12.61%)
Mutual labels:  coq
View All Similar Projects ➔

Fiat − Deductive Synthesis of Abstract Data Types in a Proof Assistant

This repository holds the source code of Fiat, a Coq ADT synthesis library.

Dependencies:

  • To build the library: Coq 8.4pl6
  • To step through the examples: GNU Emacs 24.3+, Proof General 4.4+
  • To extract and run OCaml code: OCaml 4.02.0+

Compiling and running the code

  • To build the core library: make fiat-core
  • To build the SQL-like libary: make querystructures
  • To build the parsers libary: make parsers
Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].