Skip to content

Instantly share code, notes, and snippets.

Avatar

Brendan Zabarauskas brendanzab

View GitHub Profile
View weird-type-theory-diagrams.md

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!

Syntax

View porting-inference-rules.md

Inference Rules

Natural deduction

T ::=
  | Int
  | Bool

t1, t2 ::=
View quantifier-syntax.md

Quantifiers

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

Examples

{
  out id : {
@brendanzab
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
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].
[expcompile.v]: https://www.ps.uni-saarland.de/courses/sem-ws17/expcompile.v
[course material]: https://courses.ps.uni-saarland.de/sem_ws1718/3/Resources
-/
@brendanzab
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]: https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
-/
namespace Maps
@brendanzab
brendanzab / pikelet-update.md
Last active Oct 18, 2020
Updates on the Pikelet Programming Language
View pikelet-update.md
marp theme
true
uncover

Pikelet status update

Brendan Zabarauskas

31/08/2020

@brendanzab
brendanzab / weird-lang.md
Last active Aug 24, 2020
A weird dependent graph language thing?
View weird-lang.md
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
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
%
% http://www.apache.org/licenses/LICENSE-2.0
%
% Unless required by applicable law or agreed to in writing, software
% distributed under the License is distributed on an "AS IS" BASIS,
@brendanzab
brendanzab / combining-pi-and-simga.md
Last active Apr 20, 2020
Probably a terrible idea
View combining-pi-and-simga.md

Combining Pi and Sigma types?

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

id : type [
    in A : Type, 
    in a : A, 
    out a' : A,