On the Logical Content of Computational Type Theory: A Solution to Curry's Problem

Matt Fairtlough and Michael Mendler

In this paper we relate the lax modality O to Intuitionistic Propositional Logic and give a complete characterisation of inhabitation in Computational Type Theory as a logic of constraint contexts. This solves a problem open since the 1940's, when Curry was the first to suggest a formal syntactic interpretation of O in terms of contexts. 

Michael Mendler

Last modified: Wed Apr 25 13:12:27 BST 2001