Liang-Ting Chen

MtacAR. Mtac in Agda

Type-Theory. Lecture note on Lambda Calculus and Types for FLOLAC

auto-dark-mode.vim. A MacVim plugin for switching between dark and light modes automatically.

BiSig. Bidirectional Binding Signature and Bidirectional Type Synthesis, Generically

ModalTypeTheory. Agda

FiniteSets. Fintie Sets in Cubical Agda

TTasQIIRT. Type theories as quotient inductive-inductive-recursive types

FLOLAC-semantics. Lecture notes on semantics for FLOLAC'14

provability. Agda

FindUnion. An imperative implementation of disjoint-set data structure in Haskell

PCF-Nominal. A formalisation of PCF in Agda using naive nominal binding

nstc-proposal. 國科會專題研究計畫中文 CM03/CM302 的 LaTeX 文件格式

STLC. Simply typed lambda calculus in Agda

docker-agda. Dockerfile

L-TChen.github.io. Haskell

agda-mode-vscode. agda-mode on VS Code

proof-relevant-lp. Agda

vim-dark-mode-switcher. Just a vimscript which sets the Vim background to dark or light depending on system-wide setup