Discover c-cube/quip-book Open Source project

Stars
3
Rank 3,963,521 (Top 79 %)
Language SMT
Created over 3 years ago
Updated over 1 year ago

c-cube

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

Book for Quip, a proof format for first-order and higher-order theorem provers

ocaml-containers

A lightweight, modular standard library extension, string library, and interfaces to various libraries (unix, threads, etc.) BSD license.

OCaml

485

qcheck

QuickCheck inspired property-based testing for OCaml.

OCaml

343

datalog

An in-memory datalog implementation for OCaml.

Prolog

247

iter

Simple iterator abstract datatype, intended to iterate efficiently on collections while performing some transformations.

OCaml

104

tiny_httpd

Minimal HTTP server using good old threads + blocking IO, with a small request router.

OCaml

printbox

print nested boxes, lists, arrays, tables in several formats

OCaml

stimsym

[toy] A rewriting language similar to the core of Mathematica

OCaml

moonpool

Commodity thread pools and concurrency primitives for OCaml 5

OCaml

gen

Simple, efficient iterators for OCaml

OCaml

mc2

[research] A modular SMT solver in OCaml, based on mcSAT

SMT

oseq

Purely functional iterators compatible with standard `seq`.

OCaml

batsat

A (parametrized) Rust SAT solver originally based on MiniSat

Rust

lwt-pipe

[beta] A multi-consumer, multi-producers blocking queue and stream for Lwt

OCaml

calculon

Library for writing IRC bots in OCaml, a collection of plugins, and a dramatic robotic actor.

OCaml

ocaml-iostream

generic I/O streams of bytes

OCaml

cconv

[dead] combinators for type conversion (serialization/deserialization) to/from several formats. See this blog post (outdated): http://cedeela.fr/universal-serialization-and-deserialization.html

OCaml

linol

Wrapper around the OCaml `lsp` library to make it easier to write LSP servers

OCaml

ezcurl

A simple wrapper around OCurl.

OCaml

bare-ocaml

runtime library and code-generator for BARE (https://baremessages.org/)

OCaml

sidekick

A modular library for CDCL(T) SMT solvers, with [wip] proof generation.

SMT

smbc

Experimental model finder/SMT solver for functional programming.

OCaml

ocaml-trace

Common interface for tracing/instrumentation libraries in OCaml

OCaml

choice

Choice operator in OCaml, providing a backtracking monad

OCaml

spelll

fuzzy string searching, using Levenshtein automaton. Can be used for spell-checking.

OCaml

ocaml-avro

Runtime library and schema compiler for the Avro serialization format

OCaml

sqlite3_utils

[beta] High-level wrapper around ocaml-sqlite3

OCaml

olinq

LINQ-like combinators for manipulating collections of in-memory data

OCaml

maki

[beta] persistent memoization of computations, e.g. for repeatable tests and benchmarks

OCaml

ocaml-bigstring

Overlay over bigarrays of chars

OCaml

thread-local-storage

thread-local storage for OCaml

OCaml

fuseau

[alpha] lightweight fiber library for OCaml 5

OCaml

ocaml-minisat

OCaml bindings to Minisat

C++

ocaml-gnuplot

bindings to gnuplot (fork of https://bitbucket.org/ogu/gnuplot-ocaml/)

OCaml

seq

compatibility package for the standard OCaml iterator type

OCaml

quip

[wip] Proof format and checker for first-order and higher-order theorem provers

OCaml

batsat-ocaml

OCaml bindings for batsat (https://github.com/c-cube/batsat)

OCaml

trustee

[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.

OCaml

ocaml-qbf

OCaml bindings to QBF solver(s)

ocabot

IRC bot for #ocaml@freenode

OCaml

jsonrpc2

[unfinished] Jsonrpc2 for OCaml, parametrized by the underlying IO.

OCaml

IKSML

[toy] industrial-strength implementation of the SKI calculus, using XML

thrifty

[wip] Reimplementation of thrift in OCaml

Thrift

hashset_benchs

Reproducing https://www.reddit.com/r/rust/comments/4dd5yl/rust_vs_f_hashset_benchmark/

Clojure

funarith

[wip] functorial library with classic algorithms for arithmetic

OCaml

ocaml-atomic

Compatibility package for the Atomic module

OCaml

indexed-set

OCaml implementation of indexed sets (inspired from Haskell's ixSet library)

OCaml

[draft] dynamic representation of types

OCaml

zulip-log-viewer

Small website to serve zulip logs obtained from [zulip archive](https://github.com/zulip/zulip-archive)

OCaml

ocaml-twirp

OCaml implementation of Twirp using ocaml-protoc

OCaml

poc-modular-io

proof of concept for https://github.com/ocaml/RFCs/pull/19

OCaml

frog-utils

[frozen] Scheduling and running jobs on a shared computer, then analyse their output

OCaml

oasis-parser

Simple parser for _oasis files

OCaml

ocaml-chord

[unfinished] Chord DHT implementation in OCaml (not production-ready)

OCaml

rcontext

Per-request context, inspired from Go's

OCaml

space_camels

[toy] Tiny game built to try notty

OCaml

smtlib-utils

A parser and some utils for SMTLIB. For a fully compliant parser, see https://github.com/Gbury/dolmen/.

SMT

gemini-client

[toy] ocaml client for gemini

OCaml

containers-lwt

Utilities for Lwt

OCaml

bender

[toy] IRC bot in rust, for my private use

Rust

iterators_bench

[bench] benchmark of various iterator implementations

OCaml

playground

various little experiments

OCaml

ccbor

[WIP] CBOR codec for OCaml

OCaml

ocaml-ty

[clone] Fork of ocaml-ty by Grégoire Henry (original url https://gitorious.org/ocaml-ty/)

OCaml

containers-misc

[toy] Random stuff from containers, low quality, experimental

OCaml

neperien

[unfinished] structured, hierarchical log system for OCaml

OCaml

andes

[toy, wip] A chain with lots of lemmas. More specifically, a logic programming engine.

OCaml

logtk

[migrated to https://github.com/c-cube/zipperposition] Logic toolkit, designed primarily for first-order automated reasoning. It aims at providing basic types and algorithms (terms, unification, orderings, indexing, etc.) that can be factored out of several applications.

OCaml

vim-tptp

Vim syntax file for the TPTP logic format (http://www.cs.miami.edu/~tptp/)

Vim Script

paradox

[clone] model finder for first-order logic, from http://vlsicad.eecs.umich.edu/BK/Slots/cache/www.cs.chalmers.se/~koen/paradox/

Haskell

bencode_rpc

[toy] Remote Procedure Call with B-encode serialization and Lwt concurrency (probably not production ready).

OCaml

ldl

[TOY] loop-dee-loop, an event loop

OCaml

bender-ocaml

[dead] Write OCaml plugins for bender

OCaml

ocaml-aig

[toy] And-Inverter Graph in OCaml

OCaml

tiny-httpd-moonpool-bench

experiment with tiny_httpd using moonpool as a scheduler

Makefile

tomato-chan

[wip] IRC bot.

OCaml

unif-visitor

Playground for visitors on terms

OCaml

ocaml-polynomials

[toy] Toy implementation of multi-variable polynomials over Z

OCaml

microsat

experiments around microsat

Rust

playground-k8s

just playing with minikube

OCaml

ppx_deriving_cconv

[deprecated] ppx_deriving instance for CConv encoders/decoders

OCaml

tip-parser

[obsolete] parser for https://github.com/tip-org/

OCaml

irky

[wip] IRC client for OCaml

OCaml

ocaml-irclog

parsing IRC logs as produced by irssi

OCaml

strictly_tally

Implementation of relative placement tabulation for dance competitions

Rust

c-cube/quip-book

c-cube

Reviews

Repository Details

More Repositories