Events Calendar
Jun 19
09:30 - 16:45
Practical and Foundational Aspects of Type Theory
Centre for Reasoning Interdisciplinary Workshop

Students of formal logic or foundations of mathematics often first encounter the phrase "type theory" in the context of Bertrand Russell's ramified theory of types. But type theory is in fact a diverse field of formal systems, many of which are currently undergoing rapid and fruitful development. This workshop will be devoted to certain theoretical aspects and practical implementations of dependent type theory - notably developed by Swedish logician, philosopher, and computer scientist Per Martin-Löf - which has been shown to have surprising and powerful connections to abstract fields of mathematics such as category theory and more recently homotopy theory. Dependent type theory can serve as: a foundation for constructive/intuitionistic mathematics; a logic and functional programming language under the propositions-as-types paradigm or Curry-Howard correspondence; and even as a basis for formal semantics of natural language. More generally, dependent type theory as a logic offers an alternative to classical first order predicate calculus in its various applications.


  • David Corfield (Philosophy, Kent)
  • Noam Zeilberger (Computer Science, Birmingham)
  • Sam Speight (Computer Science, Oxford)
  • Dominic Orchard (Computer Science, Kent)
  • Marco Paviotti (Computer Science, Kent)
  • Gavin Thomson (Philosophy, Kent)

For a full programme, please see the external website link below.

Visit the event web page


Seminar Room 5,
Woolf College,
The Pavilion,
Giles Lane,
University of Kent,
United Kingdom


Open to all,

Contact: Gavin Ronald Thomson


Corporate Communications - © University of Kent

The University of Kent, Canterbury, Kent, CT2 7NZ, T: +44 1227 764000

Last Updated: 10/01/2012