David Corfield Practical and Foundational Aspects of Type Theory

Contents

Idea of the 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 class 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.

Slides are available from a previous related workshop Type Theory and Philosophy.

The workshop is sponsored by the Centre for Reasoning at the University of Kent.

Schedule

Day: 19 June 2018

Venue: Woolf Seminar Room 5 (W1-SR5), University of Kent

  • 9.00-9.30 Welcome and coffee

  • 9.30-10.00 David Corfield (Philosophy, Kent) - “Modal Homotopy Type Theory: The new new logic”

  • 10.00-10.30 Gavin Thomson (Philosophy, Kent) - “Proof-Theoretic Semantics: From Natural Deduction to (Homotopy) Type Theory”

  • 10.30-11.30 Noam Zeilberger (Computing, Birmingham) - “Type Refinement Systems and the Categorical Perspective on Type Theory”

  • 11.30-12.00 COFFEE BREAK

  • 12.00-13.00 Dominic Orchard (Computing, Kent) - “Graded Modal Logic for Linear Dependent Type Theory”

  • 13.00-14.30 LUNCH

  • 14.30-15.30 Samuel Speight (Computing, Oxford) - “Encoding Inductive Types in Impredicative Intensional Dependent Type Theory”

  • 15.30-15.45 COFFEE BREAK

  • 15.45-16.45 Marco Paviotti (Computing, Kent) - “Denotational Semantics in Synthetic Guarded Domain Theory”

Workshop dinner: 18.45 in Café du Soleil.

Anyone wishing to attend please contact Gavin Thomson (grt20@kent.ac.uk).

Last revised on June 18, 2018 at 10:23:58. See the history of this page for a list of all contributions to it.