May 7-10, 2017 Asilomar, California

Search for Program Structure

Gabriel Scherer

The community of programming language research loves the Curry-Howard correspondence between proofs and programs. Cut-elimination as computation, theorems for free, \texttt{call/cc} as excluded middle, dependently typed languages as proof assistants, etc. Yet we have, for all these years, missed an obvious observation: ``the structure of \emph{programs} corresponds to the structure of proof \emph{search}''. For pure programs and intuitionistic logic, more is known about the latter than the former. We think we know what programs are, but logicians know \emph{better}! To motivate the study of proof search for program structure, we retrace recent research on applying \emph{focusing} to study the canonical structure of simply-typed $\lambda$-terms. We then motivate the open problem of extending canonical forms to support richer type systems, such as polymorphism, by discussing a few enticing applications of more canonical program representations.