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...
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