Discover @jonsterling Open Source projects

Jon Sterling (@jonsterling)

jonsterling

Stars
1,036
Global Rank 28,470 (Top 2 %)
Followers 677
Following 301
Registered about 15 years ago
Most used languages

Agda 21.1 %

TeX
17.9 %

Standard ML 16.8 %

Haskell
12.6 %

Coq 9.5 %

OCaml
6.3 %

Lean 2.1 %

Makefile 2.1 %

PureScript 2.1 %

Objective-C
2.1 %

LilyPond 1.1 %

C++
1.1 %

Shell
1.1 %

Scheme
1.1 %

HTML
1.1 %

Racket
1.1 %

Python
1.1 %
Location 🇩🇰 Denmark
Country Total Rank 155
Country Ranking

Agda 1

LilyPond 1

Lean 2

PureScript 2

Coq 3

Standard ML 4

TeX
4

Racket
7

Haskell
8

OCaml
8

Scheme
8

Objective-C
20

Makefile 32

Shell
42

C++
131

Python
303

HTML
940

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.

dreamtt

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

forest

My mathematical Zettelkasten, created using forester.

agda-calf

A cost-aware logical framework, embedded in Agda.

math

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

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.

ocaml-forester

Mirror of ocaml-forester

Lens.hpp

Functional Lenses in C++

coq-guarded-computational-type-theory

lcf-sequent-calculus-example

A self-contained implementation of forward and backward inference for intuitionistic propositional logic

RAFExamples

An example of ReactiveFormlets use in the MVVM style

coq-domains

agda-synthetic-domain-theory

tt

latex-dieudonne

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

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-zipper-machine

An abstract machine using indexed containers and their zippers

agda-stc

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

sml-logical-framework

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

constructive-sheaf-semantics

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

TaskWarriorWeb

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

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.

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.)

topos-theory-notes

lean4-sgdt

Experiments with synthetic guarded domain theory in Lean 4.

itt-bidirectional

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

math-translations

Hypertext translations of some classic mathematical papers into English

agda-brouwerian-mathematics

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

agda-abt

Abstract binding trees in Agda

lecture-notes

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!

mathematical-notebook

Read at your own risk! Not everything in here is guaranteed to be correct.

agda-bar-induction

coq-algebra

hs-monad-open

Open-ended computation for when you need it (open recursion)

coq-sgdt

Agda-Sheaves

Sheaves in Agda (will be superseded by https://github.com/jonsterling/constructive-sheaf-semantics which has sheaves on a site)

agda-nominal-sets

coq-meaning-explanation

sml-pronominal-ml

An experiment with nominal features in a programming language

twelf-nbe

normalization by evaluation for MLTT in twelf

ocaml-modular-typechecking

Modular type checking using open types

guarded-theories

sml-spreads

A library for Brouwerian data structures (spreads, fans, choice sequences)

purescript-lcf

A general-purpose library for LCF+validations refiners

stlc-type-inference

bar-induction-slides

racket-grit

Grit: the kernel around which a PRL forms

agda-directed-plump-ordering

bibtex-references

agda-sheaf-semantics

here we go again

tt-singletons

experiments with singleton types & identity types in type theory

Luitzen

A possibly-wrong implementation of OTT (a fork of pi-forall)

ocaml-abt

(intrinsically typed) ABTs for OCaml

lean-syntax

just learning to use lean

latex-diagrams

An extension of Paul Taylor's excellent diagrams package with an improved default arrow head, using METAFONT

twelf-itt

modular development of intensional type theory in twelf

sml-elaborating-typechecker

An example of how to use LCF + validations to type check and normalize lambda terms (via cut admissibility)

latex3-jmsdelim

Tmux-Haskell

A DSL for scripting Tmux in Haskell. [BTW, this doesn't really work. Sorry!]

coq-synthetic-realizability

Some experiments

coq-algebra-experiments

Formalizing some basic commutative algebra in Coq in order to procrastinate on my thesis proposal and paper reviews.

hs-aws-dynamodb-streams

Bindings for DynamoDb Streams

Coq-Up

A tarpit in Coq

purescript-abt

Abstract binding trees for purescript

choice-sequences

twelf-cmcp

ITT 1979 in Twelf (à la Constructive Mathematics and Computer Programming)

sml-ifol-completeness

intuitionistic completeness of first order logic à la Constable & Bickford

Lithos

A processor for Literate Haskell, inspired by Docco. Uses Pandoc, Highlighting-Kate, BlazeHtml and Shakespearean templates.

coq-presheaf-cwf

agda-cubical-sets

sml-open-ended

open-ended data types in standard ml (i.e. the ultimate benign effect)

.TeXmacs-progs

My TeXmacs configuration files

sml-kripke-schema

Kripke's Schema as a computational effect

CCG-Framework

A framework for testing multi-modal CCG constructions

systems-study-notes

some very sad notes for a very sad class

agda-groupoids

Groupoids in Agda with no postulates (by Darin Morrison)

sml-ipl-completeness

Constructive witness to completeness of realizability interpretation for IPL, using exceptions. Based on an idea from Mark Bickford and Bob Constable

sml-abt

This is the CMU ABT library, with some minor improvements. DEPRECATED in favor of https://github.com/JonPRL/sml-typed-abts

higher-dimensional-pers

experiments with higher dimensional partial equivalence relations for mixing exact equality with fibrant equality

agda-meaning-explanations

Demonstration of meaning explanations in agda

LaTeX-Macros

My personal macros

sml-abt-parser

A parser library for ABTs based on parcom. DEPRECATED in favor of https://github.com/jonsterling/sml-typed-abts

coq-cbpv

Diaconescu-TT

An Agda proof of Diaconescu's Theorem for Constructive Type Theory using Setoids

latex-ebproof-rules

A package to support combining ebproof with mathpartir

burnt-offering-secrets

sml-nominal-sets

agda-mltt-forcing

a model of MLTT over the Baire spread

sml-open-abt

An open-ended operator structure for abts

c0ns

An experimental nameserver written in C0

singletons

Adding GHC type literal promotion to http://www.cis.upenn.edu/~eir/packages/singletons/. There are trade-offs.

music

lambdapi

An in-progress port of LambdaPi to Standard ML

sml-zipper

ETT-Lite

A fork of Stephanie Weirich's pi-forall, which does away with the parametric quantifier (not my research question) and adds equality reflection