Properties of Sequent-Calculus-Based Languages

Date and time: 
Friday, November 17, 2017 - 13:00
Location: 
220 Deschutes
Author(s):
Philip Johnson-Freyd
University of Oregon
Host/Committee: 
  • Zena Ariola (Chair)
  • Boyana Norris
  • Michal Young
  • Alison Kwok, Architecture
  • Geoffrey Hulette, Sandia Labs

Programmers don't just have to write programs, they are have to reason about them. Programming languages aren't just tools for instructing computers what to do, they are tools for reasoning. And, it isn't just programmers who reason about programs: compilers and other tools reason similarly as they transform from one language into another one, or as they optimize an inefficient program into a better
one. Languages, both surface languages and intermediate ones, need therefore to be both efficiently implementable and to support effective logical reasoning. However, these goals often seem to be in
conflict.

This dissertation studies a series of programming language calculi inspired by the \emph{Curry-Howard correspondence}, relating programming languages to proof systems. Our focus is on calculi
corresponding logically to classical sequent calculus and connected computationally to abstract machines. We prove that these calculi have desirable properties to help bridge the gap between reasoning and implementation.

Firstly, we explore a persistent conflict between extensionality and effects for lazy functional programs that manifests in a loss of confluence. Building on prior work, we develop a new rewriting theory
for lazy functions and control which we first prove corresponds to the desired equational theory and then prove, by way of reductions into smaller system, to be confluent. Next, we turn to the inconsistency
between weak-head normalization and extensionality. Using ideas from our study of confluence, we develop a new operational semantics and series of abstract machines for head reduction which show us how to retain weak-head reduction's ease of implementation.

After demonstrating the limitations of the above approach with strict evaluation or types other than functions, we turn to typed calculi, showing how a type system can be used not only for mixing different
kinds of data, but also different evaluation strategies in a single program. Building on variations of the reducibility candidates method such as biorthogonality and symmetric candidates, we preset a uniform
proof of strong normalization for our mixed-strategy system which works so long as all the strategies used satisfy criteria we isolate.