Phase Distinctions in Type Theory

Abstract: (Joint work with Jon Sterling and Yue Niu)

The informal phase distinction between compile-time and run-time in programming languages is formally manifested by the distinction between kinds, which classify types, and types, which classify code. The distinction underpins standard programming methodology whereby code is first type-checked for consistency before being compiled for execution. When used effectively, types help eliminate bugs before they occur.

Program modules, in even the most rudimentary form, threaten the distinction, comprising as they do both types and programs in a single unit. Matters worsen when considerating "open" modules, with free module variables standing for its imports. To maintain the separation in their presence it is necessary to limit the dependency of types, the static parts of a module, to their imported types. Such restrictions are fundamental for using dependent types to express modular structure, as originally suggested by MacQueen.

To address this question Moggi gave an "analytic" formulation of program modules in which modules are explicitly separated into their static and dynamic components using tools from category theory. Recent work by Dreyer, Rossberg, and Russo develops this approach fully in their account of ML-like module systems. In this talk we consider instead a "synthetic" formulation using a proposition to segregate the static from the dynamic, in particular to define static equivalence to manage type sharing and type dependency

Robert Harper is a Professor of Computer Science at Carnegie Mellon, where he has been a member of faculty since 1988. He is past recipient of the Allen Newell Award for research excellence and the Herbert Simon Award for teaching excellence. He is author of Practical Foundations for Programming Languages, a textbook account of programming language theory. His work focuses on the application of type theory to program development, language design, compiler construction, and mechanized proof.

Computer sciencealgebraic topologycategory theorylogic

Audience: learners

( chat )

Topos Institute Colloquium