Explore projects

Ocsigen based web-server for interaction with Arborator

command line interface to the Grew library

Separation Logic with Characteristic Formulae Entirely within Coq

implementation and metatheory of time credits and time receipts in Iris / Coq

An LR(1) parser generator for OCaml.

Why3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.

Coccinelle is a program matching and transformation engine which provides the language SmPL (Semantic Patch Language) for specifying desired matches and transformations in C code.

ProVerif symbolic protocol verifier

A generator of debugger for the Skel language for semantics description

This platform gives tools to manipulate Sanskrit data

Server side of the Grew-web tool

Mirror of the git repository of Coq now hosted at https://github.com/coq/coq (synchronized every 15min)

Python Semantics in Skel