My solutions to C++ Primer(5th edition) exercises.

A few Mathematics Revision Cheat Sheets I've made on LaTeX.

The compiler and interpreter for the high-level quantum programming language Qunity, based on compositional quantum control flow.

Agda lecture notes for the Functional Programming course at TU Delft

A work-in-progress core language for Agda, in Agda

Development of homotopy type theory in Agda

Categories parametrized by morphism equality, in Agda

Clowns to the left of me, jokers to the right

A slow-paced introduction to reflection in Agda. ---Tactics!

What I wish I knew when learning HoTT

Porting of software foundations book to Agda

Papers on aspects of Generalised Algebraic Theories, Contextual Categories and Mathematical Theory Of Data

Abstract binding trees (abstract syntax trees plus binders), as a library in Agda

Minimal implementations for dependent type checking and elaboration

OTT in Agda

Quasi-quoting library for agda

Course on Metaprogramming

An Agda formalization of System F and the Brown-Palsberg self-interpreter

Categories with families in HoTT

The category theory by example book

Theory and Applications of Lenses and Optics

A digital archive of category theory papers.

multi-stage relational programming for staged relational interpreters: running with holes, faster

A LaTeX-typeset reproduction of Reynolds' "Types, Abstraction and Parametric Polymorphism"

A proof assistant for higher-dimensional type theory

Improved Lecture Notes in Computer Science (LNCS) template

Resources for ACT study group

A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.

A proof checker meant for education. Primarily for teaching proofs of correctness of functional programs.

A mini-book on category theory. Superseded by https://github.com/jonsterling/forest