Paper Info
Title
On the Logical Content of Computational Type Theory: A Solution to Curry's Problem
Abstract
In this paper we relate the lax modality O to Intuitionistic Propositional Logic (IPL) and give a complete characterisation of inhabitation in Computational Type Theory (CTT) 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.
Year
Venue
Keywords
2000
TYPES
logical content,constraint context,complete characterisation,computational type theory,intuitionistic propositional logic,formal syntactic interpretation,lax modality o,type theory,propositional logic
Field
DocType
ISBN
Intuitionistic logic,Discrete mathematics,Autoepistemic logic,Computer science,Type theory,Zeroth-order logic,Algorithm,Many-valued logic,Well-formed formula,Intermediate logic,Propositional variable
Conference
3-540-43287-6
Citations 
PageRank 
References 
3
0.39
14
Authors
2
Name
Order
Citations
PageRank
Matt Fairtlough1716.75
Michael Mendler231434.60