I think type systems, type theory, formal logic, proof theory and formal reasoning are really interesting topics. 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 β
Glask πΌ π΅
Glask is my current, long-term project. It is a small programming language inspired by Haskell. It has type classes, higher-rank polymorphism, row polymorphism and other interesting features.
I have already built a pretty large part of that as a part of my master's thesis. At this point, I am reworking it from the ground up, formalizing the type system, and learning more things. I am hoping to make the project public one day.
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 and it seems to fit the constraints of the text file better. 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.
π« Lambdulus π²
Lambdulus is a tool for learning Ξ»-calculus interactively. It runs locally in any modern browser and enables you to experience Ξ»-calculus as a programming language.
I have a strong appreciation for teaching tools. This one is the first one I developed. It's being used at FIT CTU in Prague for teaching Ξ»-calculus in a course on programming paradigms.
Resin πΊ π·
Resin is a small automated theorem prover for First Order Classical Logic built on resolution.
It's another step on my journey through the topic of formal reasoning and implementing theorem provers and proof assistants. It is not my goal to make it real-world applicable at all. I just want to explore the concepts related to the resolution and learn more about logic.
constants: zero .
aliases : 0 = zero
, 1 = suc(0) .
axioms: β n Plus(0, n, n)
, β n m r Plus(n, m, r) ==> Plus(suc(n), m, suc(r))
, β n Times(0, n, 0)
, β n m r a [Times(n, m, r) β§ Plus(r, m, a) ==> Times(suc(n), m, a)]
, Fact(0, 1)
, β n pr r [Fact(n, pr) β§ Times(suc(n), pr, r) ==> Fact(suc(n), r)]
.
theorem fact-0-is-1: Fact(0, 1) .
theorem fact-1-is-1 : Fact(1, 1) .
theorem exists-fact-for-1 : β n Fact(n, 1) .
Plover πΉ
Plover is a small automated theorem prover based on a logic language like Prolog. The main idea is to replace Minilog's depth-first search strategy with a complete one.
It serves as the first step on my journey to study the topic of formal reasoning and automated and interactive theorem provers and assistants. It's as small as Minilog.
The main difference the complete search strategy makes is that the language can productively answer queries like nat(A).
for a knowledge base like the following:
nat(s(N)) :- nat(N).
nat(z).
Minilog πΈ
Minilog is an implementation of a small logic programming language. The primary purpose of it is to present a simple abstract machine that can be easily implemented in any language and can serve as an aid when making the intuition about how such a language works.
I have designed the abstract machine and written a description of it for (not only) my students to learn about how such a language works. It is meant to inspire and offer a starting point to them should they decide to implement a small subset of Prolog as their course project.
Minilog is not the first project in a line of logic languages. In the past, I've implemented a small logic language Monolog. But back then, I didn't know how to implement the unification in a sensible way. So, while the Minilog implements unification according to Martelli and Montanari, the first project keeps around sort of a unification context making it very impractical and inefficient.
plus(z, N, N).
plus(s(N), M, s(R)) :- plus(N, M, R).
times(z, _, z).
times(s(N), M, A) :- times(N, M, R), plus(R, M, A).
fact(z, s(z)).
fact(s(N), R) :- fact(N, PR), times(s(N), PR, R).
Frea π°
Small programming language with HM type inference, higher-kinded types, and lazy evaluation. Implemented as an AST interpreter in Haskell.
It's one of my first larger projects. I wanted to learn about Hindley-Milner type inference and how to implement parametric polymorphism both for functions and data types. Additionally, I learned a bit about laziness.
Originally, the language used to treat recursion on terms very explicitly. There was a fix
language construct.
Eventually, I replaced the fix
with an implicit recursion. The type-checker first splits the definitions into groups of mutually recursive definitions and finds a topological ordering on them. This makes it possible to infer the types as polymorphic as possible.
module Main where
{ data Result a
= None
| Some a
; let
{ zero n = (n == 0)
; dec n = (n - 1)
; rec fact n = if (zero n)
then 1
else (n * (fact (dec n)))
} in (Some (fact 5))
}
Lambda-pie π΄
Three better simple REPLs for Ξ»->
, Ξ»2
, and Ξ»Ξ
.
Ξ»-> >> assume (id :: T -> T) (T :: *) (a :: T) (b :: T)
Ξ»-> >> id a
(id a) :: T
Ξ»-> >> id b
(id b) :: T
Lambdas πΎ
Three simple REPLs for Ξ»
, Ξ»->
, and Ξ»2
.
A couple of small lambda evaluators as a reference for my students:
All of the following, except the last one, were done as a semestral project or coursework during my master's. The last one was a little thing I did while talking about JavaScript on a voice call with a friend.
Monolog π
Small logic programming language inspired by Prolog. Implemented as an AST interpreter in Ruby.
plus(z, N, N).
plus(s(N), M, s(R)) :- plus(N, M, R).
times(z, _, z).
times(s(N), M, A) :- times(N, M, R), plus(R, M, A).
fact(z, s(z)).
fact(s(N), R) :- fact(N, PR), times(s(N), PR, R).
:check
fact(s(s(s(s(s(z))))), F)
SJS π
A simple toy compiler from a Lisp-inspired programming language targetting JS. Implemented as a parser and a trivial code-gen in Scala.
(define fact (n)
(if (or (= n 0) (= n 1))
1
(* n (fact (- n 1)))
)
)
(fact 5)
FeenyML π
Interpreter and (incomplete) VM for a small programming language inspired by Feeny and ML.
function fact (num) ->
if num == 0
then 1
else num * fact(num - 1);
fact(5)
Call-by-Name ISWIM π
Call-by-name operational semantics of ISWIM in PLT REDEX.
(((Ξ» unused (Ξ» x (* (+ 1 x) (+ 2 x))))
((Ξ» x (x x)) (Ξ» x (x x))))
(+ 3 4))
:-->>n 72
Transaction ISWIM π
ISWIM with transactional memory in PLT REDEX.
(let ([a 80])
(let ([b 20])
(let ([adjust ;; Invariant: a + b = 100
(Ξ» f1
(Ξ» f2
(transaction
(begin (set a (f1 a))
(set b (f2 b))
(if0 (+ (+ a b) -100) (Ξ» x x) 1)))))])
(begin ((adjust (Ξ» a (* a 2))) (Ξ» b (+ b -50))) ;; abort
((adjust (Ξ» a (+ a -20))) (Ξ» b (* b 2))) ;; commit
a))))
evaluates to 60
$wau ISWIM π
A little experiment with non-strict semantics of ISWIM in PLT REDEX.
DFSM-DSL π
JS DSL for implementing Deterministic Finite State Machines using string template literal.
const dfsm = require('./dsl').dfsm
let factorial = null
factorial = dfsm`
state default INIT
call
INIT -> ${(state, num) => num === 0 ? '1' : `${num}`}
${(state, num) => num === 0 ? undefined : factorial.call(num - 1)} .
call
${state => state === 'INIT' ? 'NO' : state} -> ${(state, num) => num === 0 ? state : `${Number(state) * num}`}
${(state, num) => num === 0 ? state : factorial.call(num - 1)} .
`
factorial.call(5)
console.log(factorial.state) // 120