EPSRC logo

Details of Grant 

EPSRC Reference: GR/R29697/01
Title: The Semantics of Classical Proofs
Principal Investigator: Hyland, Professor JME
Other Investigators:
Researcher Co-Investigators:
Project Partners:
Department: Pure Maths and Mathematical Statistics
Organisation: University of Cambridge
Scheme: Standard Research (Pre-FEC)
Starts: 21 February 2002 Ends: 20 February 2005 Value (£): 77,518
EPSRC Research Topic Classifications:
Fundamentals of Computing Logic & Combinatorics
EPSRC Industrial Sector Classifications:
Information Technologies No relevance to Underpinning Sectors
Related Grants:
Panel History:
Panel DatePanel NameOutcome
22 Feb 2001 MathFIT Deferred
Summary on Grant Application Form
Classical proof is of fundamental importance in both Mathematics and Computer Science. In proof theory some of the most interesting and hardest problems centre round the equivalence of proofs and the classification of this through rules of local permutability. The sequent calculus in particular exhibits strong symmetry properties which make it hard to model. Current research concentrates on semantics which pass through a double negation translation and which therefore violate some of these symmetries. We propose to harness recent work in enriched cateogry theory to furnish a fully symmetric calculus and to provide the natural supporting theoretical results. We intend to use this analysis in a search for concrete and interesting models, inspired perhaps by process calculus and by conventional combinatorial and mathematical structures. We plan to commence an investigation of applications in mathematics (Herbrand's theorem, Ramsay's theorem) and Computer Science (productive use of failure in classical proof search).
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