Jonathan Chan's Projects
Solutions for https://adventofcode.com/2017/.
Solutions for https://adventofcode.com/2018/.
Solutions for https://adventofcode.com/2019/.
Solutions for https://adventofcode.com/2020/.
Solutions for https://adventofcode.com/2021/.
Solutions for https://adventofcode.com/2022/.
Agda is a dependently typed programming language / interactive theorem prover.
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
Notes on categories with families, interpreting syntax into CwFs, and some semantic models.
Docker Compose files for Thulium
Various woefully incomplete mechanizations of Luo's Extended Calculus of Constructions.
A collection of Racket scripts for manipulating student repositories on GitHub as course staff.
A data visualization library for Racket.
Migration scripts from Mercurial to Git (last worked in 2017)
Some HoTT in Idris.
A purely functional programming language with first class types
The Impressions File-System Image Generator from "Generating Realistic Impressions for File-System Benchmarking" (Agrawal 2009), now with bugs fixed.
README.md for GitHub profile.
Logical relation for predicative CC omega with booleans and an intensional identity type
LaTeX source for Sized Dependent Types via Extensional Type Theory
a silly fediverse emoji bot
A LaTeX-typeset reproduction of Reynolds' "Types, Abstraction and Parametric Polymorphism"
Files used for PHYS 319, WT2 2018
Solutions to Project Euler problems.
Android app for generating random pastel colours. Also it's pronounced like "kwots".
A pure Ruby code highlighter that is compatible with Pygments
Various mechanized proof files for fun.
Mostly follows https://www.cs.cornell.edu/courses/cs3110/2019fa/textbook/interp/inference.html.
NGINX configs for Thulium