rlepigre Goto Github PK

bare-metal-aarch64

Fiddling with aarch64 exception levels on a Raspberry Pi 3.

cerberus

Cerberus C semantics

coq

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

coq-elpi

Coq plugin embedding elpi

coq-equations

A function definition package for Coq

coq-lean-import

coq-library-undecidability

A library of mechanised undecidability proofs in the Coq proof assistant.

coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq

coq-opam

Archive for all Coq related OPAM packages organized in various repositories

coq-serapi

Coq Protocol Playground with Se(xp)rialization of Internal Structures.

coq-tactician

A Seamless, Interactive Tactic Learner and Prover for Coq

coq-waterproof

coqhammer

CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory

cwg

Crossword generator, text, LaTeX and HTML backend

dedukti

Implementation of the λΠ-calculus modulo rewriting

dklib

General purpose, hand-written, dedukti files

dune

A composable build system for OCaml.

elpi

Embeddable Lambda Prolog Interpreter

fmodulo

System F modulo

gameshell

"jeu" d'apprentissage du shell et des commandes standards

itauto

js-tt

Javascript Teaching Tools

lambdapi

Minimal implementation of the λΠ-calculus modulo

metacoq

Metaprogramming, verified meta-theory and implementation of Coq in Coq

mtac2

ocaml

The core OCaml system: compilers, runtime system, base libraries

ocaml-bash-wrap

A trivial bash wrapper script

ocaml-bindlib

Efficient binder representation in OCaml

ocaml-earley

Parsing library based on Earley Algorithm

ocaml-earley-ocaml

Extensible OCaml parser to be used with Earley