Skip to content

Instantly share code, notes, and snippets.

Avatar

Brendan Zabarauskas brendanzab

View GitHub Profile
View weird-field-param-language-2.md

Weird field/param language 2

AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.

This is a more succinct syntax than the previous gist, this time using in and out in place of param and record, and making introductions and eliminations more succinct.

Grammar

View weird-field-param-language.md

Weird field/param language

Further messing around on top of some ideas in the previous gist.

AUTOMATH/De Bruijn Notation-inspired, but extended with dependent records.

Grammar

term, type ::=\

View weird-binder-language.md

Weird binder language thingy

Playing around with a uniform notation for binders (eg. Π, Σ, λ, let). This is probably not the greatest language to program in directly, but I think it's fun to see if a more consistent syntax can help to expose some of the differences between dependent functions, dependent pairs, and let expressions...

Syntax

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