proofs

Runnable code for solving Project Euler problems in Java, Python, Mathematica, Haskell.

KaRaMeL is a tool for extracting low-level F* programs to readable C code

Authenticated multi-version database: sparse binary merkle tree with compact partial-tree proofs

GAPT: General Architecture for Proof Theory

ZKProofs website

Like Keybase but distributed

Solutions to In-Class questions, Problem Sets and Exams of MIT Mathematics for Computer Science 2015 (same as 2019 Open Learning Library)

An example of how generate zero-knowledge proofs and verify using an Ethereum smart contract.

Type level algebraic "proofs" using lens combinators

Fully proved small C functions (examples for verification course).

Theorems, Definitions, Papers, Research

F-omega with interval kinds mechanized in Agda

Translate natural deduction proofs into natural language.

My portfolio contains a lexer generator, a parser generator, my own λProlog interpreter, and several meta-theorems for the propositional logic with their proofs written in Coq.

Formal proofs in mathematics/computer science/logic formalized in the Agda language. A hobby project I am working on in my free time.

Template-based proofs of concurrent search structures.

My master thesis on Whitebox cryptography & AES Whitebox schemes.

Idris proofs for extensional equalities

Just some of my CS Proofs, things like why `k << 1 == k * 2`