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

• UpdatedMay 26, 2024
• Java

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

• UpdatedDec 14, 2025
• OCaml

A verification toolchain for Rust programs

• UpdatedDec 17, 2025
• OCaml

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

• UpdatedFeb 9, 2023
• C++

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

• UpdatedSep 2, 2024
• TeX

Solutions to Susanna Epp's Discrete Mathematics book, 5th Edition

• UpdatedAug 29, 2025
• TeX

GAPT: General Architecture for Proof Theory

• UpdatedDec 5, 2025
• Scala

ZKProofs website

• UpdatedOct 25, 2023

Like Keybase but distributed

• UpdatedAug 29, 2023
• JavaScript

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

• UpdatedOct 17, 2019

[Informatica - Basi di Dati 1] Forum di scambio e confronto di soluzioni a esercizi e prove d'esame passate

• UpdatedDec 10, 2025

Type level algebraic "proofs" using lens combinators

• UpdatedJul 26, 2019
• Haskell

Theorems, Definitions, Papers, Research

• UpdatedJul 3, 2019
• TeX

Easy-to-use Sigma proofs in C using libsodium.

• UpdatedOct 13, 2025
• C

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

• UpdatedJun 26, 2017
• C

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.

• UpdatedAug 23, 2025
• TeX

F-omega with interval kinds mechanized in Agda

• UpdatedAug 1, 2024
• Agda

Agda Library to Study the Expressive Power of Languages for Static Variability

• UpdatedDec 13, 2025
• Agda

Distributed algorithms in Lean 4

• UpdatedSep 10, 2025
• Lean

• UpdatedFeb 9, 2022
• Zig