Algebraic Foundations of Proof Refinement January 9, 2017

Jonathan Sterling and Robert Harper. Under review for LICS 2017.

We contribute a general apparatus for dependent tactic-based proof refinement in the LCF tradition, in which the statements of subgoals may express a dependency on the proofs of other subgoals; this form of dependency is extremely useful and can serve as an algorithmic alternative to extensions of LCF based on non-local instantiation of schematic variables. Additionally, we introduce a novel behavioral distinction between refinement rules and tactics based on naturality. Our framework, called Dependent LCF, is already deployed in the nascent RedPRL proof assistant for computational cubical type theory.

Links: Manuscript

Forcing Bar Induction in System T December 8, 2016

Jonathan Sterling. Under review for the Journal of Functional Programming.

Using Martin Escardo’s effectful forcing technique, we demonstrate the constructive validity of Brouwer’s monotone Bar Theorem for any System T-definable bar. We have not assumed any non-constructive (Classical or Brouwerian) principles in this proof, and have carried out the entire development formally in the Agda proof assistant for Martin-Löf’s Constructive Type Theory.

Links: Agda code

Dependent Types for Pragmatics July 23, 2015

Darryl McAdams and Jonathan Sterling. Published in Epistemology, Knowledge and the Impact of Interaction (Springer).

This paper proposes the use of dependent types for pragmatic phenomena such as pronoun binding and presupposition resolution as a type-theoretic alternative to formalisms such as Discourse Representation Theory and Dynamic Semantics.

Links: arXiv preprint

Derivative and Novel Speeches in Plato's Symposium May 19, 2013

Jonathan Sterling. Unpublished

The six speeches of the Symposium may be divided into two sets: on the one hand, there is Phaedrus’s speech and those which are derivative of his, and on the other hand, there are the novel speeches; and these are the ones which reject the previous approaches and propose unique theories of Eros.

Links: Download PDF

A Survey of Phrase Projectivity in the Antigone April 28, 2013

Jonathan Sterling. Unpublished

In this paper, I demonstrate how, and to what degree, phrase projectivity corresponds with register and meter in Sophocles’s Antigone, by developing a quantitative metric \(\wp\) for projectivity and comparing it across lyrics, trimeters and anapaests using the data provided by the Perseus Ancient Greek Dependency Treebank. In the appendices, the formal algorithm for the computations done herein is developed in Haskell.

Links: Download PDF