Skip to content

Instantly share code, notes, and snippets.

@TOTBWF
TOTBWF / MicroTT.ml
Last active September 2, 2025 23:59
A simple single-file elaborator for MLTT
(** Core Types *)
module Syntax =
struct
type t =
| Local of int
| Hole of string
| Let of string * t * t
| Lam of string * t
| Ap of t * t
| Pair of t * t
@pdarragh
pdarragh / papers.md
Last active February 23, 2025 02:04
Approachable PL Papers for Undergrads

Approachable PL Papers for Undergrads

On September 28, 2021, I asked on Twitter:

PL Twitter:

you get to recommend one published PL paper for an undergrad to read with oversight by someone experienced. the paper should be interesting, approachable, and (mostly) self-contained.

what paper do you recommend?

@vivshaw
vivshaw / README.md
Last active October 12, 2025 02:53
πŸ™ˆπŸ™‰πŸ™Š Three Wise Monkeys πŸ™ˆπŸ™‰πŸ™Š

Inference Rules

Natural deduction

T ::=
  | Int
  | Bool

t1, t2 ::=
@AndrasKovacs
AndrasKovacs / GluedEval.hs
Last active January 20, 2025 21:55
Non-deterministic normalization-by-evaluation in Olle Fredriksson's flavor.
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
https://github.com/ollef/sixty
The main idea is that during elaboration, we need different evaluation