Jon Sterling
Programmer at SlamData, Inc

Oracles and Choice Sequences for Type-theoretic Pragmatics

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"

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.

Thursday, October 8, 2015
3:30 PM
Gates & Hillman Centers 6501

Principles of Programming Seminars