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…

Purpose This issue documents the progress of development on HTML export. It's not for discussion of specific features, which should occur in other issues or on Discord. For design discussions, ...

in Haskell we can define both of these in this way:
data Free (f :: Type -> Type) (a :: Type) = Pure a | Free (f (Free f a))
data Cofree (f :: Type -> Type) (a :: Type) = Cofree a (f (Cofree ...