-
latexrun Public
Forked from aclements/latexrunA 21st century LaTeX wrapper
Python MIT License UpdatedDec 11, 2025 -
CBPV Public
Lean 4 mechanization of assorted CBPV metatheory.
-
MutualInduction Public
An experimental mutual induction tactic for Lean 4.
-
-
ssh-keygen-ed25519-vanity Public
Generate a vanity EdDSA SSH key for fun.
-
-
newbot Public
Forked from iliana/newbota silly fediverse emoji bot
Rust GNU General Public License v3.0 UpdatedAug 8, 2025 -
Idris2 Public
Forked from idris-lang/Idris2A purely functional programming language with first class types
Idris Other UpdatedAug 8, 2025 -
-
TTBFL Public
A logical relations model of a minimal type theory with bounded first-class universe levels mechanized in Lean.
-
mltt-consistency Public
Forked from yiyunliu/mltt-consistencyLogical relation for predicative CC omega with booleans and an intensional identity type
TeX MIT License UpdatedFeb 23, 2025 -
parapoly Public
A LaTeX-typeset reproduction of Reynolds' "Types, Abstraction and Parametric Polymorphism"
-
coq Public
Forked from rocq-prover/rocqCoq 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 develo…
-
msc-thesis Public
Forked from briandealwis/ubcdissLaTeX source for Sized Dependent Types via Extensional Type Theory
-
ECC Public
Various woefully incomplete mechanizations of Luo's Extended Calculus of Constructions.
-
github-scripts Public
A collection of Racket scripts for manipulating student repositories on GitHub as course staff.
-
rouge Public
Forked from ayberkt/rougeA pure Ruby code highlighter that is compatible with Pygments
Ruby Other UpdatedJun 1, 2022 -
impressions Public
The Impressions File-System Image Generator from "Generating Realistic Impressions for File-System Benchmarking" (Agrawal 2009), now with bugs fixed.
-
system-f-redex Public
Church-style System F with definitions in Redex.
{{ message }}