# Proof and definition in logic and type theory

## Robin Adams

(Royal Holloway, University of London)

Most approaches to logic focus on proof. The logic consists of the axioms and rules of deduction that may be used when proving a theorem. Definitions are secondary: to say that a function is definable typically means just that a certain formula is provable. Type theory takes the opposite approach. A type theory specifies which operations are acceptable when constructing an object. With type theory, proof is secondary: to say that a theorem is provable means just that an object of a certain type is constructible.

**Wednesday 2nd September 2009, 14:00**

Robert Recorde Room

Department of Computer Science