Details of Grant 

EPSRC Reference:	GR/R95975/01
Title:	CATEGORICAL LOGIC AND PROOF THEORY: REALIZABILITY INTERPRETATIONS FOR CONSTRUCTIVE THEORIES
Principal Investigator:	Gambino, Dr N
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department:	Pure Maths and Mathematical Statistics
Organisation:	University of Cambridge
Scheme:	Postdoc Res Fellowship PreFEC
Starts:	01 January 2003	Ends:	31 December 2004	Value (£):	66,191
EPSRC Research Topic Classifications:	Logic & Combinatorics
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:	Panel Date Panel Name Outcome 20 Mar 2002 Maths Postdoctoral Sift March 2002 Deferred
Summary on Grant Application Form
Realizability is a technique of proof theory. Its original version was obtained by defining a relation between natural numbers and sentences of arithmetic so that if a number and a sentence are related, then the former can be seen as a proof of the latter. Since then, realizability has been extensively developed and applied to the study of arithmetic and analysis. Recent developments in categorical logic generated a renewed interest in realizability interpretations.The aim of the proposed research is to extend and apply realizability to a wide class of constructive theories. One reason for the interest in constructive theories is that proofs formalized in them are intended to have computational content. This is usually referred to as the proofs-as-algorithms principle. Realizability provides a means to make this idea mathematically precise. Remarkably, constructive theories are sufficiently expressive to formalize large parts of mathematics. On the whole, constructive theories can be formulated in different settings: set theory, type theory and category theory. Research both in Britain and elsewhere is actively focusing on relating constructive theories formulated in different settings. The first main goal of the research is to obtain a general account of realizability interpretations using categorical logic. The second main goal is to apply realizability interpretations to obtain proof theoretic results.
Key Findings
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Potential use in non-academic contexts
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Impacts
Description This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk Summary Date Materialised
Sectors submitted by the Researcher
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
Project URL:
Further Information:
Organisation Website:	http://www.cam.ac.uk