Types for proofs and programs

by Paul Callaghan, Zhaohui Luo, James McKinna, Robert Pollack

This book contains a selection of papers presented at the ?rst annual workshop of the TYPES Working Group (Computer-Assisted Reasoning Based on Type Theory, EU IST project 29001), which was held 8t…