Skip to content

Instantly share code, notes, and snippets.


Brendan Zabarauskas brendanzab

View GitHub Profile
brendanzab / ArithExprs.lean
Last active May 10, 2021
A proof of the correctness of an arithmetic expression compiler and decompiler in Lean 4.
View ArithExprs.lean
A proof of the correctness of an arithmetic expression compiler in Lean 4.
Ported from [expcompile.v], which is part of Derek Dreyer and Gert Smolka's
[course material].
[course material]:

Weird type theory diagrams

I always get confused about terms, types, expressions, etc. in full spectrum dependent types… so toying around with these very informal Venn diagram thingies.

Note: Don't take this super seriously or authoritatively, it's more me trying to figure things out, and I'm very sloppy at this stuff!



Inference Rules

Natural deduction

T ::=
  | Int
  | Bool

t1, t2 ::=


Idea: create a surface syntax where all quantifiers behave more like records/modules with labelled entries.


  out id : {

C++'s Templates

C++'s templates could be seen as forming a duck typed, purely functional code generation program that is run at compile time. Types are not checked at the initial invocation stage, rather the template continues to expand until it is either successful, or runs into an operation that is not supported by that specific type – in that case the compiler spits out a 'stack trace' of the state of the template expansion.

To see this in action, lets look at a very simple example:

template <typename T>
T fact(T n) {
    return n == T(0) ? T(1) : fact(n - T(1)) * n;
brendanzab /
Last active Apr 10, 2021
A reading list that I'm collecting while building my Rust ES+CQRS framework:

Functional, Reactive, and Distributed Systems Bibliography


brendanzab / Monoids.lean
Last active Mar 5, 2021
Playing with monoids in Lean 4
View Monoids.lean
Playing with monoids in Lean 4
$ lean -v
Lean (version 4.0.0-nightly-2021-02-28, commit 6a6f68f6ccc8, Release)
namespace Monoids
brendanzab / maps.lean
Last active Feb 10, 2021
Total and partial maps in Lean 4 (inspired by Software Foundations)
View maps.lean
Total and partial maps
This is inspired by [the relevant chapter in Software Foundations]. Unlike
Software Foundations, these maps are also parameterised over a `Key`
type, which must supply an implementation of `DecidableEq`.
[Software Foundations]:
namespace Maps
brendanzab /
Last active Oct 18, 2020
Updates on the Pikelet Programming Language
marp theme

Pikelet status update

Brendan Zabarauskas