Jon Sterling.

Software engineer, dilettante type theorist, syntactician, and philologist. Student of Ancient Greek, Sumerian, Hittite, Akkadian, Latin, Old English and German. I also co-host The Type Theory Podcast.

Realizing the Truth in Intensional Type Theory August 23, 2014

The key idea of Observational Type Theory1 is to make the propositional equality coextensive with the equality which is validated under the standard semantics for Type Theory, which is the meaning explanations and their metamathematical counterpart, the realizability interpretation. Now, Extensional Type Theory is usually characterized in terms of typechecking (membership) being undecidable because the “true” equality is made to hold judgementally; but this is a deceptive characterization when applied to Computational Type Theory (Nuprl), since there are many types besides equality which may be given meaning explanations but which have an undecidable membership judgement.

Synthetic Judgements in Interactive Proof: In Defense of Tactics August 14, 2014

Whilst the judgements of type theory are preferred to be analytic, the practice of operating a proof assistant is inherently and unavoidably synthetic, and is always accompanied by some manner of refinement and tactics: and so the question is never whether to use tactics, but rather how much pain one intends to experience in the process of using them: this is inextricable from the activity of proving.

Interview with Peter Dybjer: types and testing August 13, 2014

I’m so pleased to be able to announce the first fruit of a joint project with David Christiansen and Darin Morrison, which is an interview of Peter Dybjer for The Type Theory Podcast. We spoke to Peter about QuickCheck-style testing and its relation to proofs and verification in type theory. Subscribe to the RSS feed or follow us on Twitter if you are interested in listening to discussions with researchers, because we have more to come.

A Type Theory with Scoped Realizability June 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 Theory June 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 Theory May 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 Types May 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 Proof February 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.

All posts…