jonsterling Goto Github PK

second-brain

A curated list of awesome Public Zettelkastens 🗄️ / Second Brains 🧠 / Digital Gardens 🌱

sheafification

Sheafification functor in type theory

singletons

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

sml-abt

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

sml-abt-parser

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

sml-abt-patterns

DEPRECATED in favor of https://github.com/JonPRL/sml-typed-abts

sml-abt-unify

Simple unification for ABTs in SML

sml-elaborating-typechecker

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

sml-ifol-completeness

intuitionistic completeness of first order logic à la Constable & Bickford

sml-intensional-lcf

extensions to the LCF signature for interactive refinement proof

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-kripke-schema

Kripke's Schema as a computational effect

sml-logical-framework

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

sml-modernized-algol

Harper's Modernized ALGOL in SML using multi-sorted nominal abstract binding trees

sml-nominal-sets

sml-open-abt

An open-ended operator structure for abts

sml-open-ended

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

sml-parcom-wrapper

Please just use http://github.com/RedPRL/sml-parcom instead

sml-pronominal-ml

An experiment with nominal features in a programming language

sml-spreads

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

sml-system-f

An implementation of System F, as described in PFPL.

sml-zipper

Huet's Zipper

stlc-type-inference

symposium-speeches-paper

Derivative and Novel Speeches in Plato's Symposium

systems-study-notes

some very sad notes for a very sad class

taskpaper

TaskPaper parser written in Swift

taskwarriorweb

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

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.

texmacs

Source Code of GNU TeXmacs, Developers Guide ==>

theories-with-judgement

A theory of theories with judgement