Skip to content

Instantly share code, notes, and snippets.


Brendan Zabarauskas brendanzab

View GitHub Profile
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 / ArithExprs.lean
Last active Mar 2, 2021
A proof of the correctness of an arithmetic expression compiler 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]:
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


brendanzab /
Last active Aug 24, 2020
A weird dependent graph language thing?
Notation Meaning
l ? T abstract node in T
l : T concrete node in T
l = t node equal to t
default = t reduce to this node if all nodes are concrete
{ ... } graph term
t1.{ l = t2 } updates node l in t1 to be t2
t.l gets the value of node l in t
t.{ l1 -> l2 } renames l1 to l2 in t
brendanzab / ddl-experiment.makam
Last active May 11, 2020
A dependently typed binary data description language, prototyped in Makam!
View ddl-experiment.makam
% Copyright 2020 YesLogic Pty. Ltd.
% Licensed under the Apache License, Version 2.0 (the "License");
% you may not use this file except in compliance with the License.
% You may obtain a copy of the License at
% Unless required by applicable law or agreed to in writing, software
% distributed under the License is distributed on an "AS IS" BASIS,
brendanzab /
Last active Apr 20, 2020
Probably a terrible idea

Combining Pi and Sigma types?

-- id : forall a. a -> a
-- id x = x

id : type [
    in A : Type, 
    in a : A, 
    out a' : A,
brendanzab / dependent.makam
Last active Dec 3, 2019
Messing with dependent type systems in makam (
View dependent.makam
(* terms *)
term : type.
universe : term.
annotate : term -> term -> term.
unitType : term.
unitTerm : term.
pairType : term -> (term -> term) -> term.
pairTerm : term -> term -> term.
brendanzab /
Last active Nov 29, 2019
Pull-based tree processing for lambda calculi.
//! See [this twitter thread](
//! Traditional syntax trees suffer from lots of pointer indirections and poor data locality!
//! Could we stream things instead, using [pull-based events](
//! as opposed to trees? This should be equivalent to our tree based approaches, but might
//! require us to think carefully about what our core calculus looks like in order to make
//! this kind of thing easier.
use std::sync::Arc;
brendanzab /
Last active Aug 12, 2020
🚧 A graph-based core for a dependently typed language. 🚧

A graph-based core for a dependently typed language


An overly-ambitious attempt to re-think the core calculus of dependent type theory by basing it on graphs as opposed to lambdas, Π-types, Σ-types, etc. The hope is that this might allow us to investigate dependency more closely, and allow us to refine programs to target different environments in an easier way than with traditional programming representations.