I build small programming languages, theorem provers, and other systems related to PLT concepts.
I sometimes write about the things I learn ✏️ in my digital notepad 📘
The latest published post was a report on Propositions as Types ⭐
Detour 🍀 🌷
Detour is a small proof-checker for a mix of Second-order Propositional Logic and First-order Predicate Logic Natural Deduction proofs in Fitch-style notation.
It is a first step into the area of proof-checkers and (interactive) proof assistants. I picked the Fitch-style notation because I find it nice to look at. The goal is to have a very simple proof-checker that supports user-defined inductive data types/syntactic constructs, proof by induction, case analysis and maybe more.
An example proof—a proof of totality of the addition on natural numbers.