David McAllester - Dependent Type Theory from the Perspective of Mathematics, Physics, and (...)

Dependent type theory imposes a type system on Zemelo-Fraenkel set theory (ZFC). From a mathematics and physics perspective dependent type theory naturally generalizes the Bourbaki notion of structure and provides a universal notion of isomorphism and symmetry. This comes with a universal substitution theorem --- isomorphic objects are inter-substitutable in well-typed contexts (Hofmann and Streicher 1995). From an AI perspective, or automated reasoning perspective, dependent type theory underlies the LEAN interactive verifier which is currently the go-to system for formal verification of mathematics. This talk will review dependent type theory as a discipline on set theory (the set model of type theory) and discuss approaches to improving automated reasoning based on SMT (SAT Modulo a theory) technology. This results in a class of inference algorithms under the name SAT modulo type theory or SMTT. Speculations on the relationship between SMTT and deep learning will be discussed briefly.
David McAllester (TTIC)