Jon Sterling

AquaUI. Superseded by AquaKit https://tangled.org/jonmsterling.com/AquaKit

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]

Githood. A minimal Github client for iOS. No longer actively developed.

forest. My mathematical Zettelkasten, created using forester. Moved to sourcehut.

dreamtt. A pedagogic implementation of abstract bidirectional elaboration for dependent type theory.

math. A mini-book on category theory. Superseded by https://github.com/jonsterling/forest

ocaml-forester. Mirror of ocaml-forester

project-pterosaur. Lean

Tasky. A Taskwarrior client. This was created to fill my own need: feel free to modify it! If it looks really ugly, you probably have your terminal configured wrong.

coq-guarded-computational-type-theory. Coq

Lens.hpp. Functional Lenses in C++

agda-stc. Hacking synthetic Tait computability into Agda. Example: canonicity for MLTT.

latex-dieudonne. A LaTeX package to reproduce (an enhanced version of) the numbered paragraph style from classic French mathematics books.

lcf-sequent-calculus-example. A self-contained implementation of forward and backward inference for intuitionistic propositional logic

coq-domains. Coq

constructive-sheaf-semantics. I'm putting Palmgren's Constructive Sheaf Semantics into Agda. Defines sheaves via Grothendieck pretopologies.

RAFExamples. An example of ReactiveFormlets use in the MVVM style

tt. secret project

agda-synthetic-domain-theory. Agda

hs-abt. Type safe abstract binding trees for Haskell, using Vinyl

sml-modernized-algol. Harper's Modernized ALGOL in SML using multi-sorted nominal abstract binding trees

agda-effectful-forcing. Agda formalization of the paper, "Higher-Order Functions and Brouwer's Thesis". Deduces a Brouwer ordinal from a function ((nat -> nat) -> nat) in System T.

sml-logical-framework. Jason Reed's Tiny LF, and some experiments in higher-order proof refinement logics using Jon Sterling Thought

agda-zipper-machine. An abstract machine using indexed containers and their zippers

TT-Reflection. An experimental type theory with scoped equality reflection, and non-arbitrary proof search. This is basically a pared down version of Andromeda/Brazil, but with untyped reduction and a more Nuprl-like feel. Computational content of proofs is got via a realizability-based extraction. (Note: substitution is unsafe here, not because of a problem with the theory, but because I didn't understand how Bound works sadly.)

TaskWarriorWeb. A quick & dirty Yesod-based local web interface to TaskWarrior

topos-theory-notes. TeX

math-translations. Hypertext translations of some classic mathematical papers into English

itt-bidirectional. A bidirectional type checker for intensional constructive type theory (with thanks to Stephanie Weirich).

lean4-sgdt. Experiments with synthetic guarded domain theory in Lean 4.

agda-brouwerian-mathematics. some "modernized" brouwerian mathematics, inspired by Hancock, Ghani & Pattinson

lecture-notes. TeX

effectful-typesetting. A case-study in effects-and-handlers for bubbling out configurations from the interior of programs that typeset text.

brouwer-translations. translations of brouwer's writings; corrections from native speakers welcome!

coq-meaning-explanation. Coq

agda-bar-induction. Agda

sml-pronominal-ml. An experiment with nominal features in a programming language

agda-nominal-sets. Agda