Computational Type Theory [1/5] - Robert Harper - OPLSS 2018

Oregon Programming Languages Summer School
Parallelism and Concurrency
July 3-21, 2018
University of Oregon
www.cs.uoregon.edu/research/s...
Title: Computational Type Theory [1/5]
Speaker: Robert Harper, Carnegie Mellon University
Date: Monday, 16 July 2018, Session 1
Topics:
- fundamental premise of constructivism
- type theory as basis for all mathematics
- type theory as a programming language
- theory of truth vs. theory of formal proof
- deterministic operational semantics
- abstract syntax with binding, scope, and substitution
- forms of expression
- judgment forms: values and transition rules
- derived notion
- binary decision diagrams
- types are specifications of program behavior
- judgments as forms of expression
- algorithms as communication
- behavioral vs. structural expressions
- types and values are programs
- families of types
- type-indexed families of types (a.k.a., dependent types)
- hypothetical/general judgments
- functionality: respecting equality of indices
- what is equality of types?
- equi-satisfaction
- preview of higher-dimensional/cubical type theory
- meanings of judgments, a.k.a., meaning explanations, a.k.a., computational semantics
- equality of canonical types, a.k.a., type-values
- head expansion lemma, a.k.a., reverse execution
© 2018, University of Oregon