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 → ANSSI-FR → Freespec

ANSSI-FR / Freespec

Licence: gpl-3.0
A framework for implementing and certifying impure computations in Coq

Labels

coq

Projects that are alternatives of or similar to Freespec

Cufp 2015 Tutorial
An introductory tutorial for the Coq proof assistant.
Stars: ✭ 9 (-78.05%)
Mutual labels:  coq
Jt89
sn76489an compatible Verilog core, with emphasis on FPGA implementation and Megadrive/Master System compatibility
Stars: ✭ 14 (-65.85%)
Mutual labels:  coq
Nuprlincoq
Implementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-24.39%)
Mutual labels:  coq
Monads
Coq code accompanying several articles on semantics of functional programming languages
Stars: ✭ 9 (-78.05%)
Mutual labels:  coq
Stalin Sort
Add a stalin sort algorithm in any language you like ❣️ if you like give us a ⭐️
Stars: ✭ 868 (+2017.07%)
Mutual labels:  coq
Vvclocks
Verified vector clocks, with Coq!
Stars: ✭ 14 (-65.85%)
Mutual labels:  coq
Cpp2v
Formalization of C++ for verification purposes.
Stars: ✭ 24 (-41.46%)
Mutual labels:  coq
Parseque
Total Parser Combinators in Coq
Stars: ✭ 37 (-9.76%)
Mutual labels:  coq
Ledgertheory
Stars: ✭ 12 (-70.73%)
Mutual labels:  coq
Profunctor Monad
Bidirectional programming in Haskell with monadic profunctors
Stars: ✭ 30 (-26.83%)
Mutual labels:  coq
Software Foundations
Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al.
Stars: ✭ 9 (-78.05%)
Mutual labels:  coq
Coqjvm
Coq executable semantics and resource verifier
Stars: ✭ 10 (-75.61%)
Mutual labels:  coq
Coq Printf
Implementation of sprintf for Coq
Stars: ✭ 15 (-63.41%)
Mutual labels:  coq
Hott Species
Combinatorial species in HoTT
Stars: ✭ 9 (-78.05%)
Mutual labels:  coq
Paramcoq
Coq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-21.95%)
Mutual labels:  coq
Coqpie
CoqPIE (an IDE for the Coq theorem prover + PEDANTIC)
Stars: ✭ 8 (-80.49%)
Mutual labels:  coq
Hello World
A Hello World program in Coq.
Stars: ✭ 14 (-65.85%)
Mutual labels:  coq
Certint
A Certified Interpreter for ML with Structural Polymorphism
Stars: ✭ 39 (-4.88%)
Mutual labels:  coq
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+2300%)
Mutual labels:  coq
Hott
Homotopy type theory
Stars: ✭ 946 (+2207.32%)
Mutual labels:  coq
View All Similar Projects ➔

FreeSpec

FreeSpec is a framework for implementing, certifying, and executing impure computations in Coq.

Overview

This repository contains three Coq packages:

  • coq-freespec-core provides the foundation of the FreeSpec formalism.
  • coq-freespec-exec provides the means to execute impure computations implemented with the help of coq-freespec-core.
  • coq-freespec-stdlib provides a small “impure effects” library to write impure computations more easily.

The codebase is organized as follows:

  • The Coq definitions of the three theories live in the theories/ directory.
  • The OCaml source of the Coq plugins live in the plugins/ directory.
  • There are examples for the three plugins in the examples/ directory.

Getting Started

The only external dependency of FreeSpec is coq-prelude. Once this package has been built and installed, building the FreeSpec packages is as simple as

dune build

Besides, we provide two helper scripts:

  • run-tests.sh executes each Coq file living in tests/ and reports any error
  • build-docs.sh builds the OCaml and Coq source documentation

Said documentations are published here.

In addition, FreeSpec has been the subject of two academic publications.

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].