Jon Sterling.

Software engineer, dilettante type theorist, syntactician, and philologist. Student of Ancient Greek, Sumerian, Hittite, Akkadian, Latin, Old English and German. I also compose music; hit me up if I can help on one of your projects!

A Type Theory with Scoped RealizabilityJune 30, 2014

Here I present an idea for a type theory which retains the benefits of wholesale adherence to the realizability interpretation1 à la Nuprl2, and yet seems to maintain a better division of labor between operator and machine.

Non-discrete Records in Type TheoryJune 11, 2014

In my recent post I demonstrated a type-theoretic formulation of non-dependent record types as presheaves on a particular topological space $$X$$ of keys given an assignment $$El_X : X\to\mathbf{Type}$$. Today, I’ll construct more interesting records by endowing the key space with a non-discrete topology.

Family Union Types in Intensional Type TheoryMay 28, 2014

Family union types have existed for a few years in Extensional Type Theory à la Nuprl;1 here, I demonstrate a lightweight approach to adding them to Intensional Type Theory as an extension of Altenkirch, McBride, Swierstra’s OTT.2

Records are Sheaves of TypesMay 11, 2014

Let us define a record type as being given by a type $$X$$ of keys and an interpretation function $$F$$ which maps every key $$x:X$$ to a type. We assume the existence of a powerset functor $$\mathcal{P}: \mathbf{Type}\to\mathbf{Type}$$, which endows the discrete topology on $$X$$. Then a record type is the product of the image of $$F$$ over a subset of $$X$$: $\mbox{for}\ U\subseteq X,\quad \mathsf{Rec}(U,F) :\equiv \prod_{s:U} F(s)$

The Circle Is Not Contractible: A Short ProofFebruary 1, 2014

To those of us without a background in topology, it may have initially been surprising that the unit circle $$S^1$$ is not contractible. In this post, I’ll outline a homotopy type-theoretic proof for why this is in fact the case.

Standard ML as a Proof System, without GADTsJanuary 4, 2014

It is well known that generalized algebraic data types (a sort of phase-locked inductive family) suffice in languages like Haskell1 and OCaml to be used as a deductive system for intuitionistic logic. I’ll demonstrate how type-level axioms can be given and used in Standard ML, using only signatures and functors.

Ditransitives & Datives Without Movement: A Multi-Modal ApproachDecember 14, 2013

The issue of verbs which appear to take multiple arguments has long been a sticking point for Chomskyan grammarians, with various proposals having taken shape. Here, I’ll describe current approaches in transformational grammar, and demonstrate another approach in Multi-Modal Combinatorial Categorial Grammar. Finally, I’ll discuss the pros and cons of each approach.

A Primer of Smooth Infinitesimal Analysis: Some Exercises from Ch. 1November 7, 2013

As I read Bell’s A Primer of Smooth Infinitesimal Analysis, I thought it would be useful for me to write down my workings of the exercises as I went. The proofs are in the language of Intuitionistic Type Theory; according to common practice, I will sometimes omit arguments from application which can easily be inferred from the others.