ionathanch
Grad student in PL & former splabmate · MSc @ UBC ⇝ PhD @ UPenn
PLClub @ UPennVancouver, Canada
Pinned Repositories
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.
cwf-notes
Notes on categories with families, interpreting syntax into CwFs, and some semantic models.
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.
TTBFL
A logical relations model of a minimal type theory with bounded first-class universe levels mechanized in Lean.
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/TTBFL
A logical relations model of a minimal type theory with bounded first-class universe levels mechanized in Lean.
ionathanch/system-f-redex
Church-style System F with definitions in Redex.
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/cwf-notes
Notes on categories with families, interpreting syntax into CwFs, and some semantic models.
ionathanch/ttzoo
Notes on type theory.
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/github-scripts
A collection of Racket scripts for manipulating student repositories on GitHub as course staff.
ionathanch/HoTT-Idris
Some HoTT in Idris.
ionathanch/ECC
Various woefully incomplete mechanizations of Luo's Extended Calculus of Constructions.
ionathanch/ionathanch.github.io
ionathanch/agda
Agda is a dependently typed programming language / interactive theorem prover.
ionathanch/autoenv
A simple variable binding library based on well-scoped indices and environments
ionathanch/graphite
A data visualization library for Racket.
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/rouge
A pure Ruby code highlighter that is compatible with Pygments
ionathanch/rqual
research qualifier
ionathanch/SimPLambda
Mostly follows https://www.cs.cornell.edu/courses/cs3110/2019fa/textbook/interp/inference.html.