Skip to content

Instantly share code, notes, and snippets.

Avatar

Brendan Zabarauskas brendanzab

View GitHub Profile
@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
-/
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 : {
View cpp-templates-vs-rust-generics.md

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
brendanzab / reactive_systems_bibliography.md
Last active Apr 10, 2021
A reading list that I'm collecting while building my Rust ES+CQRS framework: https://github.com/brendanzab/chronicle
View reactive_systems_bibliography.md

Functional, Reactive, and Distributed Systems Bibliography

Books

@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 / 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