Track dependencies between theorems.

A programming language that runs in Haskell's type system. - seliopou/typo

How do you design good abstractions? By using abstractions that already exist.

I initially thought that symbol ⨋ is some sort of joke, but apparently it is used, and it made it's way to Unicode in 2002.
The only reference to its meaning or usage I found is its site on wiktion...

In this paper we present a new "external checker" for the Lean theorem prover, written in Lean itself. This is the first complete typechecker for Lean 4 other than the reference implementation in...

Could anyone explain the difference between the above mentioned terms "unique", "unique up to isomorphism" and "unique up to unique isomorphism", preferably with an example? Are there other

Implementing an equivalent to the NixOS module system in Nickel

Continuing my unending train of thoughts on static analysis ofeffects, in this post I’m going to talk about using Applicative tosort any collection. The Trav...

Deriving mode switch. GitHub Gist: instantly share code, notes, and snippets.

I thought I would write a quick reference to help people understand some contractions which I have found to be incredibly common in popular media and casual speech, but which most textbooks tend to gloss over or ignore. My hope is that I can save some of…

Logical Verification course

I was setting a big proof like this one: Adding one more layer causes Typst to complain. Is this expected?

An in-depth description of GHC's type checker, including its overall structure, key datatypes, the context that led to important design decisions, and the constraint solver. Additionally, pervasive ideas such as level numbers, zonking, the structure of the…