A logical relations model of a minimal type theory with bounded first-class universe levels mechanized in Lean.
-
Updated
Aug 17, 2026 - TeX
#
mechanization
Here are 4 public repositories matching this topic...
A Rocq Mechanization of ECMAScript 2023 Regexes
-
Updated
Jul 8, 2026 - OCaml
Lean 4 mechanization of assorted CBPV metatheory.
-
Updated
Sep 3, 2026 - Lean
Paper and Lean 4 mechanization for Graph Surgery and the Do-Operator
formal-verificationcausal-inferencelean4mechanizationgraph-surgerystructural-causal-modelsdo-operator
-
Updated
Aug 19, 2026 - TeX
Add this topic to your repo
To associate your repository with the mechanization topic, visit your repo's landing page and select "manage topics."