Programming Language Theory λΠ

List of resources about foundational knowledge for programmers (supposed to last a few decades)

Proof theory seminar

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

An adventure on formalizing logics using the Agda programming language

Convert logical formulas and generate their syntax trees as vector images in SVG format. Structuralize pure C-N formulas, pure D-proofs, and index-based summaries of pure D-proofs into a universal representation that is based on the Standard Galactic Alphabet and digits of the Alteran language of the Stargate franchise.

Interactive proof tree editing

My contributions to Metamath's mmsolitaire project.

Absurdly sophisticated proofs of simple mathematical facts in Lean 4

Assignment from CSED433: Computational Logic, 2025 Fall, POSTECH

The Open Deduction Proof Editor allows proof theorists (or anyone) to deconstruction proofs step by step. It currently supports deep inference formalisms, namely Open Deduction and naturally the Calculus of Structures. The front end of the application is written in Java, while the back end is written in Maude. There is also an implementation of …

A high-throughput combinatory logic engine mapping topological friction to execute non-well-founded algorithms on bare-metal hardware.

MCTS-guided theorem proving agent — decomposes math problems into a proof tree and explores it with LLMs. Runs on Anthropic/OpenAI APIs or fully offline on Apple Silicon.

Fitch proof constructor (using rules from my version of the forall x textbook) — Mirror of mrieppel.github.io/FitchFX/

My master thesis (and related code) in Logic at the University of Bergen.

Parser for lambda terms, written in Haskell, that is also able to execute a list of operations on the terms

A webapp for creating sequent proof of propositional formulas

An exhaustive condensed detachment formal proof generator for Hilbert systems in proof theory.

Equivalence of natural deduction and sequent calculus in HOL4

A Rust crate for type-checked propositional logic proofs.