Short Course: Type Theory

When:
March 29, 2017 @ 11:00 am – 12:15 pm
2017-03-29T11:00:00-10:00
2017-03-29T12:15:00-10:00
Where:
Keller Hall (4th fl)

Title: Introduction to Type Theory

Speaker: William DeMeo

Abstract: Type Theory is a foundation for mathematics and computer science and was developed by logicians like Alonzo Church and Per Martin-Löf. Suitable as a basis for computer-assisted proof, it is receiving increasing interest from mathematicians (e.g., for verifying mathematical proofs) and computer scientists (e.g. for verifying compilers and operating systems). Type theory is based on the Curry-Howard Isomorphism, which describes a precise relationship between proofs of a proposition and programs of the corresponding type. In this brief course, we introduce the basics of Type Theory, and practice programming and proving in one of several software implementations of the theory.