Principles of Programming Seminar

Thursday, October 8, 2015 -
2:00pm to 3:00pm


Traffic 21 Classroom 6501 Gates & Hillman Centers


JON M. STERLING, Programmer

For More Information, Contact:

sdinardo @

An adequate type-theoretic semantics for natural language expressions must account for the presuppositions that are expressed by determiners and pronouns. To this end, we extend Type Theory with a choice operator called "require", which functions as a non-deterministic oracle to retrieve the synthesis of a previously-effected verification of a proposition. Then, we give an intuitionistic semantics to this operator by appealing to Brouwer's theory of the Creating Subject, and eliminate non-determinism via spreads and choice sequences. This is based on joint work with Darryl McAdams, to be published in O. Pombo, A. Nepomuceno, J. Redmond (Ed.) "Epistemology, Knowledge and the Impact of Interaction" (Springer).
Jon Sterling completed his undergraduate at UC Berkeley in 2013, where he focused on philology, historical linguistics and cuneiform languages. He is currently developing a proof assistant for computational type theory in the Nuprl tradition, and is interested in Brouwerian mathematics and higher-dimensional type theory.


Seminar Series