Discover @jonsterling Open Source projects

Top Rating
- Top Contributors
  Discover the Top Open Source contributors by country or by language
- Interviews
  Discover real stories from Open Source developers
Discover

Discover your Favorite Language
Discover the top trending repositories and projects on Github. Explore the latest trends in your preferred languages.

Haskell

Shell

Ruby

C++

PowerShell

Assembly

OCaml

HTML

More Languages
Awesome

Awesome repositories
Discover the most awesome repositories and projects of your favorite languages. Inspired by the Awesome-* lists trend in GitHub.

Rust

PowerShell

Dart

Perl

R

Shell

Go

Crystal

More Languages
By Country

Rankings by Country
Discover the community of talented open source contributors in each country.

🇹🇼 Taiwan

🇰🇮 Kiribati

🇦🇼 Aruba

🇨🇰 Cook Islands

🇨🇻 Cabo Verde

🇸🇴 Somalia

🇶🇦 Qatar

🇾🇹 Mayotte

All Countries Compare Countries

Jon Sterling (@jonsterling)

jonsterling

Stars
1,081
Global Rank 28,394 (Top 1.0 %)
Followers 715
Following 330
Registered almost 16 years ago
Most used languages

Agda 21.1 %

TeX
17.9 %

Standard ML 16.8 %

Haskell
12.6 %

Coq 9.5 %

OCaml
6.3 %

Objective-C
2.1 %

Lean 2.1 %

Makefile 2.1 %

PureScript 2.1 %

Racket
1.1 %

LilyPond 1.1 %

Scheme
1.1 %

HTML
1.1 %

Python
1.1 %

C++
1.1 %

Shell
1.1 %
Location 🇬🇧 United Kingdom
Country Total Rank 155
Country Ranking

Coq 2

Standard ML 3

Agda 5

Lean 11

LilyPond 12

OCaml
22

PureScript 23

TeX
28

Racket
31

Scheme
71

Haskell
86

Objective-C
161

Shell
351

Makefile 359

C++
1,360

Python
3,574

HTML
6,463

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

ocaml-forester

Mirror of ocaml-forester

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.

Lens.hpp

Functional Lenses in C++

coq-guarded-computational-type-theory

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

RAFExamples

An example of ReactiveFormlets use in the MVVM style

coq-domains

agda-synthetic-domain-theory

tt

agda-stc

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

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

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

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

hs-monad-open

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

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

agda-sheaf-semantics

here we go again

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

tt-singletons

experiments with singleton types & identity types in type theory

twelf-itt

modular development of intensional type theory in twelf

latex-diagrams

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

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

bibtex-references

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

CCG-Framework

A framework for testing multi-modal CCG constructions

agda-groupoids

Groupoids in Agda with no postulates (by Darin Morrison)

sml-kripke-schema

Kripke's Schema as a computational effect

systems-study-notes

some very sad notes for a very sad class

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

coq-cbpv

sml-abt-parser

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

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

c0ns

An experimental nameserver written in C0

sml-open-abt

An open-ended operator structure for abts

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