ionathanch
Grad student in PL & former splabmate · MSc @ UBC ⇝ PhD @ UPenn
PLClub @ UPennVancouver, Canada
Pinned Repositories
cwf-notes
Notes on categories with families, interpreting syntax into CwFs, and some semantic models.
github-scripts
A collection of Racket scripts for manipulating student repositories on GitHub as course staff.
impressions
The Impressions File-System Image Generator from "Generating Realistic Impressions for File-System Benchmarking" (Agrawal 2009), now with bugs fixed.
msc-thesis
LaTeX source for Sized Dependent Types via Extensional Type Theory
parapoly
A LaTeX-typeset reproduction of Reynolds' "Types, Abstraction and Parametric Polymorphism"
scraps
Various mechanized proof files for fun.
ssh-keygen-ed25519-vanity
Generate a vanity EdDSA SSH key for fun.
system-f-redex
Church-style System F with definitions in Redex.
TT-model
A logical relations model of a minimal type theory with universes mechanized in Agda.
ttzoo
Notes on type theory.
ionathanch's Repositories
ionathanch/parapoly
A LaTeX-typeset reproduction of Reynolds' "Types, Abstraction and Parametric Polymorphism"
ionathanch/msc-thesis
LaTeX source for Sized Dependent Types via Extensional Type Theory
ionathanch/scraps
Various mechanized proof files for fun.
ionathanch/system-f-redex
Church-style System F with definitions in Redex.
ionathanch/TT-model
A logical relations model of a minimal type theory with universes mechanized in Agda.
ionathanch/cwf-notes
Notes on categories with families, interpreting syntax into CwFs, and some semantic models.
ionathanch/impressions
The Impressions File-System Image Generator from "Generating Realistic Impressions for File-System Benchmarking" (Agrawal 2009), now with bugs fixed.
ionathanch/ssh-keygen-ed25519-vanity
Generate a vanity EdDSA SSH key for fun.
ionathanch/ttzoo
Notes on type theory.
ionathanch/github-scripts
A collection of Racket scripts for manipulating student repositories on GitHub as course staff.
ionathanch/HoTT-Idris
Some HoTT in Idris.
ionathanch/adventofcode-2020
Solutions for https://adventofcode.com/2020/.
ionathanch/adventofcode-2021
Solutions for https://adventofcode.com/2021/.
ionathanch/coq
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.
ionathanch/ECC
Various woefully incomplete mechanizations of Luo's Extended Calculus of Constructions.
ionathanch/ionathanch.github.io
ionathanch/adventofcode-2018
Solutions for https://adventofcode.com/2018/.
ionathanch/adventofcode-2019
Solutions for https://adventofcode.com/2019/.
ionathanch/adventofcode-2022
Solutions for https://adventofcode.com/2022/.
ionathanch/agda
Agda is a dependently typed programming language / interactive theorem prover.
ionathanch/docker-compose
Docker Compose files for Thulium
ionathanch/graphite
A data visualization library for Racket.
ionathanch/hg2git
Migration scripts from Mercurial to Git (last worked in 2017)
ionathanch/Idris2
A purely functional programming language with first class types
ionathanch/ionathanch
README.md for GitHub profile.
ionathanch/mltt-consistency
Logical relation for predicative CC omega with booleans and an intensional identity type
ionathanch/newbot
a silly fediverse emoji bot
ionathanch/rouge
A pure Ruby code highlighter that is compatible with Pygments
ionathanch/SimPLambda
Mostly follows https://www.cs.cornell.edu/courses/cs3110/2019fa/textbook/interp/inference.html.
ionathanch/sites-available
NGINX configs for Thulium