Stars
A profiler which samples the RTS callstack
Extensions to cubical for categorical logic/type theory
An LSP client for Emacs implemented in Rust.
An editing environment for LaTeX mathematical documents
Transient interface for managing and interacting with projects
Demo for dependent types + runtime code generation
Formalizing the fact that countable choice implies postnikov effectiveness in HoTT
Lecture notes and exercises for the advanced course on Categorical Realizability at the Midlands Graduate School (MGS) 2024 and the European Summer School on Logic, Language and Information (ESSLLI…
Python scripts that build optimal routes for node collection
An experimental proof assistant based on a type theory for synthetic ∞-categories.
Latex documentation of our understanding of the synthetic /internal theory of the Zariski-Topos
A work-in-progress core language for Agda, in Agda
Yet another modal editing on Emacs / 猫态编辑
Experiment with synthetic domain theory in cubical agda
drom is a wrapper over opam/dune in an attempt to provide a cargo-like user experience. It can be used to create full OCaml projects with sphinx and odoc documentation. It has specific knowledge of…
A garden of small programming language implementations 🪴
A proof search and construction framework (based on refinery)