Trebor Huang

history. History of type theory (Chinese).

combinator-nbe. Normalization by evaluation of simply typed combinators.

model. Models of dependent type theory

vscode-forester. VSCode support for Forester

HomotopyHistory. Typst

vscode-btex. VSCode extension for bTeX.

ice1000. 🧊 A Elbereth Gilthoniel / silivren penna míriel! 🌟

ZFC. An embedding of ZFC into Agda

elab-reloaded. A modern, principled toy implementation of dependent type theory

agda-linear. An implementation of a Zeilberger-style linear type theory.

forester-theme. XSLT

forest. My forest.

clock. The clock from Rain World as an OS X desktop widget

aperiodic. An incremental generator for arbitrarily large patches of aperiodic tilings

elementary. Elementary functions in Lean

at. Effective Algebraic Topology in Haskell

Thonk. An untyped programming language based on polarized type theory.

hexo-banana-forest. A hexo plugin for foresting.

pure-type-system. A python implementation of Barendregt's pure type system.

qq-bot. A bot on Tencent QQ.

CFG-Challenge. A challenge for proof assistants about a particular context-free language.

tetrhs. A Haskell tetris bot

first-order-logic-solver. A simple first order logic solver

hereditary. Setfuck, an esolang based on the hereditarily finite sets.

elab. A simple elaborator for dependent type theory

ASKL. A simple HTML player for 4K Malody charts.

Numerical-Analysis-Homework. Homework repository for Numerical Analysis course.

stiff-second-order-bvp. A robust adaptive algorithm for stiff second order boundary value problems

Mathieu. A puzzle related to the M24 sporadic simple group

coq-logic. Formalization of first order logic in Coq.

PyGR. Implements symbolic calculation in General Relativity.