COMPUTATION VIA TYPES, LOGIC, AND TOPOLOGY

Course Description

This is a seminar style course which will explore two frameworks for thinking
about programming languages, Stone Duality and the Curry-Howard Correspondence. Stone Duality is an observation about the deep connection between certain kinds of lattices and topological spaces. This connection can be leveraged to describe (Scott) domains which give a denotational semantics, or mathematical model, of programming languages such as the lambda calculus. The Curry-Howard Correspondence describes a deep connection between the simply typed lambda calculus and propositional logic which can be extended to describe a variety of different languages and associated logics. These two frameworks give us a wide toolbox for studying computation (in the form of the lambda calculus), the allowable behaviors of a language (in the form of the type system), and the
mathematical content of these behaviors (in the form of the corresponding topology).

The goal of this course is to develop 3 different perspectives on computation
1). types, 2). logic, 3). topology. There will be a few assignments about select topics or theorems, however the main part of this course is to encourage students to find a topic that interests them, in any of the frameworks/perspectives, and work with the instructor to develop a project that explores the topic more deeply. This can be implementing a programming language, proving a property, writing a paper, etc.

Optional Text

Steven Vickers, Topology via Logic