All Projects → robbertkrebbers → Ch2o

robbertkrebbers / Ch2o

Licence: other

Labels

Projects that are alternatives of or similar to Ch2o

Nuprlincoq
Implementation of Nuprl's type theory in Coq
Stars: ✭ 31 (-58.67%)
Mutual labels:  coq
Metalib
The Penn Locally Nameless Metatheory Library
Stars: ✭ 47 (-37.33%)
Mutual labels:  coq
Riscv Coq
RISC-V Specification in Coq
Stars: ✭ 63 (-16%)
Mutual labels:  coq
Compcert
The CompCert formally-verified C compiler
Stars: ✭ 984 (+1212%)
Mutual labels:  coq
Pornview
Porn browser formally-verified in Coq
Stars: ✭ 42 (-44%)
Mutual labels:  coq
Verlang
Stars: ✭ 52 (-30.67%)
Mutual labels:  coq
Hott
Homotopy type theory
Stars: ✭ 946 (+1161.33%)
Mutual labels:  coq
Certicoq
A Verified Compiler for Gallina, Written in Gallina
Stars: ✭ 66 (-12%)
Mutual labels:  coq
Poleiro
A blog about Coq
Stars: ✭ 42 (-44%)
Mutual labels:  coq
Collapsing Towers
Collapsing Towers of Interpreters
Stars: ✭ 61 (-18.67%)
Mutual labels:  coq
Parseque
Total Parser Combinators in Coq
Stars: ✭ 37 (-50.67%)
Mutual labels:  coq
Freespec
A framework for implementing and certifying impure computations in Coq
Stars: ✭ 41 (-45.33%)
Mutual labels:  coq
Perennial
Verifying concurrent crash-safe systems
Stars: ✭ 57 (-24%)
Mutual labels:  coq
Paramcoq
Coq plugin for parametricity [[email protected]]
Stars: ✭ 32 (-57.33%)
Mutual labels:  coq
Scallina
A Coq-based synthesis of Scala programs which are correct-by-construction
Stars: ✭ 65 (-13.33%)
Mutual labels:  coq
Profunctor Monad
Bidirectional programming in Haskell with monadic profunctors
Stars: ✭ 30 (-60%)
Mutual labels:  coq
Silveroak
Formal specification and verification of hardware, especially for security and privacy.
Stars: ✭ 51 (-32%)
Mutual labels:  coq
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-1.33%)
Mutual labels:  coq
Sfja
SoftwareFoundations(Ja)
Stars: ✭ 65 (-13.33%)
Mutual labels:  coq
Scala Escape
A compiler plug-in to control object lifetimes in Scala
Stars: ✭ 60 (-20%)
Mutual labels:  coq

PREREQUISITES

This version is known to compile with:

  • Coq 8.5pl2
  • SCons 2.5
  • Ocaml 4.02.3
  • GNU C preprocessor 6.1.1

BUILDING INSTRUCTIONS

Say "scons" to build the full library, or "scons some_module.vo" to just build some_module.vo (and its dependencies).

In addition to common Make options like -j N and -k, SCons supports some useful options of its own, such as --debug=time, which displays the time spent executing individual build commands.

scons -c replaces Make clean

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