POPL 2017
Sun 15 - Sat 21 January 2017
Fri 20 Jan 2017 11:20 - 11:45 at Auditorium - Type Systems 3 Chair(s): Derek Dreyer

Formal constructive type theory has proved to be an effective language for mechanized proof. By avoiding non-constructive principles, such as the law of the excluded middle, type theory admits sharper proofs and broader interpretations of results. From a computer science perspective, interest in type theory arises from its applications to programming languages. Standard constructive type theories used in mechanization admit computational interpretations based on meta-mathematical normalization theorems. These proofs are notoriously brittle; any change to the theory potentially invalidates its computational meaning. As a case in point, Voevodsky’s univalence axiom raises questions about the computational meaning of proofs.

We consider the question: Can higher-dimensional type theory be construed as a programming language? We answer this question affirmatively by providing a direct, deterministic operational interpretation for a representative higher-dimensional dependent type theory with higher inductive types and an instance of univalence. Rather than being a formal type theory defined by rules, it is instead a computational type theory in the sense of Martin-L"{o}f’s meaning explanations and of the NuPRL semantics. The definition of the type theory starts with programs, and defines types as specifications of program behavior. The main result is a canonicity theorem, the first of its kind, stating that closed programs of boolean type evaluate to true or false.

Fri 20 Jan

POPL-2017-papers
10:30 - 12:10: POPL - Type Systems 3 at Auditorium
Chair(s): Derek DreyerMPI-SWS
POPL-2017-papers10:30 - 10:55
Talk
Andrej DudenhefnerTechnical University Dortmund, Jakob RehofTechnical University Dortmund
POPL-2017-papers10:55 - 11:20
Talk
Nada AminEPFL, Tiark RompfPurdue University
POPL-2017-papers11:20 - 11:45
Talk
Carlo AngiuliCarnegie Mellon University, Robert Harper, Todd WilsonCalifornia State University Fresno
POPL-2017-papers11:45 - 12:10
Talk
Stephen ChangNortheastern University, Alex KnauthNortheastern University, Ben GreenmanNortheastern University