Abstract Sean Moss

Title: The Dialectica interpretation and models of dependent type theory

Gödel devised his Dialectica interpretation to show the relative consistency of
intuitionistic arithmetic. Generalizing the work of de Paiva [1], Hyland [2], and
others, von Glehn showed that there is a model of intensional dependent type
theory whose types are Dialectica propositions [3]. There are several variants of
the original Dialectica which also give rise to models of type theory. Without
assuming any knowledge of the Dialectica interpretations, I will outline how
these models fit into a general framework and what this says about a general
model theory of dependent type theory.

[1] Valeria Correa Vaz de Paiva. The Dialectica categories. Technical Report
UCAM-CL-TR-213, University of Cambridge, Computer Laboratory, January 1991.
[2] J. M. E. Hyland. Proof theory in the abstract. Ann. Pure Appl. Logic,
114(1-3):43–78, 2002. Commemorative Symposium Dedicated to Anne S.
Troelstra (Noordwijkerhout, 1999).
[3] Tamara von Glehn. Polynomials and Models of Type Theory. PhD thesis,
University of Cambridge, September 2014.

Share this page:

Contact details

Department of Mathematics
University of Leicester
University Road
Leicester LE1 7RH
United Kingdom

Tel.: +44 (0)116 229 7407

Campus Based Courses

Undergraduate: mathsug@le.ac.uk
Postgraduate Taught: mathspg@le.ac.uk

Postgraduate Research: pgrmaths@le.ac.uk

Distance Learning Course  

Actuarial Science:

DL Study

Student complaints procedure

AccessAble logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has detailed accessibility guides for College House and the Michael Atiyah Building.