jonsterling
Associate Professor in Logical Foundations and Formal Methods
University of CambridgeCambridge, Cambridgeshire, UK
Pinned Repositories
agda-calf
A cost-aware logical framework, embedded in Agda.
AquaUI
A library for producing HIG-compliant user interfaces for the Macintosh with Aqua styling
dreamtt
A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.
forest
My mathematical Zettelkasten, created using forester.
Githood
A minimal Github client for iOS. No longer actively developed.
JonPRL
An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
math
A mini-book on category theory. Superseded by https://github.com/jonsterling/forest
ocaml-forester
Mirror of ocaml-forester
cooltt
😎TT
redtt
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
jonsterling's Repositories
jonsterling/AquaUI
A library for producing HIG-compliant user interfaces for the Macintosh with Aqua styling
jonsterling/forest
My mathematical Zettelkasten, created using forester.
jonsterling/agda-calf
A cost-aware logical framework, embedded in Agda.
jonsterling/math
A mini-book on category theory. Superseded by https://github.com/jonsterling/forest
jonsterling/ocaml-forester
Mirror of ocaml-forester
jonsterling/coq-domains
jonsterling/agda-synthetic-domain-theory
jonsterling/math-translations
Hypertext translations of some classic mathematical papers into English
jonsterling/coq-algebra
jonsterling/coq-sgdt
jonsterling/bibtex-references
jonsterling/.TeXmacs-progs
My TeXmacs configuration files
jonsterling/datalog
An in-memory datalog implementation for OCaml.
jonsterling/Second-Brain
A curated list of awesome Public Zettelkastens 🗄️ / Second Brains 🧠 / Digital Gardens 🌱
jonsterling/bravo
Castle Bravo: Experimental HoTT Implementation
jonsterling/constrain
Responsive, animated figures in JavaScript/HTML canvases
jonsterling/cubical-1
jonsterling/dream-html
Render HTML, SVG, MathML, htmx markup from your OCaml app
jonsterling/ebproofx
ebproof extended
jonsterling/extructures
Finite sets and maps for Coq with extensional equality
jonsterling/golden-forest
jonsterling/HoTT
Homotopy type theory
jonsterling/HoTTEST-Summer-School
HoTTEST Summer School materials
jonsterling/htmx
</> htmx - high power tools for HTML
jonsterling/obsidian-influx
An alternative backlinks plugin, which displays relevant and formatted excerpts from notes with linked mentions, based on the position of mentions in the notes' hierarchical structure (bullet level indentation).
jonsterling/opam-repository
Main public package repository for opam, the source package manager of OCaml.
jonsterling/TaskPaper
TaskPaper parser written in Swift
jonsterling/topiary
jonsterling/tree-sitter-langs
Language bundle for Emacs's tree-sitter package
jonsterling/TypeTopology
Logical manifestations of topological concepts, and other things. This version adopts the univalent point of view.