# Papers.

### Algebraic Foundations of Proof RefinementJanuary 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.

### Forcing Bar Induction in System TDecember 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.

### Dependent Types for PragmaticsJuly 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.

### Derivative and Novel Speeches in Plato's SymposiumMay 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.

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.