codyroux Goto Github PK

autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

bap

Binary Analysis Platform

broad-coq-tutorial

Some unstructured notes concerning the Broad tutorial to take place in March 2020

catnapp

the Categorical Nearly Automatic Property Prover

compact-php

A proof of a finitary pigeon hole principle via compactness and the infinitary version, in Lean.

fracture

an architecture-independent decompiler to LLVM IR

frontc

An OCaml library providing a C parser and lexer

hoare-toy

A tiny toy formalization of Hoare logic for IMP with a proof of soundness

knuckledragger

lean

Lean Theorem Prover

lean0.1

Snapshot of Lean 0.1, before major kernel changes in Lean 0.2. It contains a working binary, examples, and documentation.

look-and-say

master_theorem

An attempt to prove the master theorem in coq

name-the-biggest-number

nbe-experiments

ny-haskell

The source files for the NY Haskell Lean talk

polya

A heuristic procedure for proving inequalities

stupidsat

A python interface for minisat

tinymatch

A teeny language with nats, lists and pattern matching, static and dynamic semantics and a proof of progress and preservation.

toy-reflect

A tiny example of reflection in lean, using quote4

traat-lean

Lean formalization of selected lemmas from "Term Rewriting and All That"