🎓 Path to a free self-taught education in Computer Science!

This book will be a textbook written in the univalent style, taking advantage of the presence of symmetry in the logic at an early stage.

Mirror of Software Foundations in PDF

Benchmarks for capture-avoiding substitution

PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization

λλλλ Lennart Augustsson's λ-calculus cooked four ways

A reimplementation of `Data.IntMap` that uses minimum and maximum bounds on subtrees instread of bit prefixes.