Simon Cruanes

Login: c-cube

Company: @AestheticIntegration

Location: Austin, TX

Bio: Computer scientist in computational logic, automated theorem proving, and formal methods. Seasoned OCaml programmer.

Blog: http://cedeela.fr/~simon/

Blog: http://cedeela.fr/~simon/

Member of

1. null
2. null

Repositories

abrasatcuda

Truly horrible old student project: a naive SAT-solver that runs on the GPU

awesome-ocaml

A curated collection of awesome OCaml tools, frameworks, libraries and articles.

batteries-included

Batteries Included project

benchmarks

Tons of Inductive Problems: The Benchmarks

bencode

Bencode (.torrent file format) reader/writer in OCaml

bencode_rpc

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

bender

Irc bot in rust, for my private use

bender-ocaml

Write OCaml plugins for bender

bibtex

repository for sharing bibtex files

calculon

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

cconv

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

c-cube.github.io

Personal page https://c-cube.github.io

choice

Choice operator in OCaml, providing a backtracking monad

containers-lwt

Utilities for Lwt

containers-misc

Random stuff from containers, low quality, experimental

coquille

Interactive theorem proving with Coq in vim.

datalog

An in-memory datalog implementation for OCaml.

dolmen

A library providing parser for languages such as dimacs, tptp, smtlib

dolog

A dumb OCaml logger

frog-utils

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

funarith

functorial library with classic algorithms for arithmetic

gen

Simple, efficient iterators for OCaml

hashset_benchs

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

hbmc

Haskell Bounded Model Checker

IKSML

industrial-strength implementation of the SKI calculus, using XML

indexed-set

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

iterators_bench

[bench] benchmark of various iterator implementations

jsonm

Mirrors http://erratique.ch/repos/jsonm/ no pull requests, please send patches by email.

lean

Lean Theorem Prover

lelelemanifesto

null

lfsc-ml

Small type-checker for lambda-pi calculus (maybe, later, with side-conditions)

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.

lwt

A cooperative threads library for OCaml.

lwt-pipe

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

lwt_scheduler

Utils to schedule tasks in the future, using Lwt

maki

[wip] persistent incremental computations, for repeatable tests and benchmarks

manual-ocamlbuild

A new reference manual for the ocamlbuild tool

mc2

A modular SMT solver in OCaml, based on mcSAT

mini-smt

[wip] small SMT solver in OCaml

mixtbl

Statically-typed heterogenous hash table

neperien

structured, hierarchical log system for OCaml

oasis

Cabal like system for OCaml

oasis-parser

Simple parser for _oasis files

ocabot

IRC bot for #ocaml@freenode

ocaml

Read-only mirror of INRIA SVN

ocaml-aig

And-Inverter Graph in OCaml

ocaml-benchmark

Benchmarking module for OCaml

ocaml-bigstring

Overlay over bigarrays of chars

ocamlbuild

OCamlbuild

ocaml-chord

Chord DHT implementation in OCaml (not production-ready)

ocaml-containers

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

ocaml-git

Pure OCaml low-level git bindings

ocamlgraph

OCaml graph library

ocaml-hamt

Mirror of: http://gitorious.org/ocaml-hamt/ocaml-hamt

ocaml-irc-client

OCaml IRC client library

ocaml-irclog

parsing IRC logs as produced by irssi

ocaml-junit

OCaml package to produce JUnit xml reports

ocaml-minisat

Simple bindings to Minisat-C

ocaml.org

Implementation of the ocaml.org website.

ocaml-polynomials

Toy implementation of multi-variable polynomials over Z

ocaml-qbf

OCaml bindings to QBF solver(s)

ocaml-re

Pure OCaml regular expressions, with support for Perl and POSIX-style strings

Ocaml-simplex

An ocaml implementation of variants of the simplex and branch&bound algorithms for satisfiability.

ocaml-sqlexpr

Minimalistic syntax extension for type-safe, convenient execution of SQL statements.

ocaml-tls

TLS in pure OCaml

ocaml-ty

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

ocp-indent-vim

Integration of ocp-indent to vim.

ocp-index

Easy access to the interface information of installed OCaml libraries for editors like Emacs and Vim.

oetb

OCaml implementation of the Datalog engine of ETB

olinq

LINQ-like combinators for manipulations collections of data

onanomsg

nanomsg bindings for ocaml

opam

OPAM is a source-based package manager for OCaml. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.

opam-repository

Main public package repository for OPAM, the source package manager of OCaml.

operf-micro

A set of micro-benchmarks for OCaml compiler

opium

Sinatra like web toolkit for OCaml

oseq

Purely functional iterators.

paradox

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

ppx_deriving

Type-driven code generation for OCaml >=4.02

ppx_deriving_cconv

ppx_deriving instance for CConv encoders/decoders

ppx_deriving_yojson

A Yojson codec generator for OCaml >= 4.02.

printbox

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

qcheck

QuickCheck inspired property-based testing for OCaml.

qc-ptrees

A model-based QuickCheck test of ptrees (Patricia trees)

random-generator

A small OCaml library to randomly generate values

sacrebleu

Prototype of an obscure and undecipherable language.

sat

[useless, see msat](gbury/msat) sat-solver in OCaml, extracted from [0install](https://github.com/0install/0install/)

sat-bench

A small repo to test and benchmark different sat solvers

sat_playground

[toy] playground for encodings to SAT

seq

compatibility package for the standard OCaml iterator type

sequence

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

sidekick

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

smbc

Experimental model finder/SMT solver for functional programming.

space_camels

Tiny game built to try notty

spelll

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

stimsym

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

tip-parser

parser for https://github.com/tip-org/

tomato-chan

[wip] IRC bot.

To.ml

Implementation in OCaml of the Toml minimal langage (https://github.com/mojombo/toml)

tstp-proof-checker

a simple OCaml proof-checker for TSTP cnf/fof derivations. It calls external provers to check every proof step.

ty

[draft] dynamic representation of types

unif-visitor

Playground for visitors on terms

vim-tptp

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

vim-zf

Vim syntax coloring for my very own format of logic problems. Because why not.

yojson

JSON parsing and pretty-printing library for OCaml

yolopam-repository

Personal opam repository to put foobar-like packages.

z3

The Z3 Theorem Prover

zipperposition

An automatic theorem prover in OCaml for typed logic with equality, datatypes and arithmetic, based on superposition+rewriting; supporting libraries for manipulating terms, formulas, clauses, etc. (including Logtk).

Commits To