Details of Grant 

EPSRC Reference:	EP/F031114/1
Title:	Proof Theory and Constraint Satisfaction
Principal Investigator:	Gent, Professor IP
Other Investigators:	Dyckhoff, Dr R
Researcher Co-Investigators:
Project Partners:
Department:	Computer Science
Organisation:	University of St Andrews
Scheme:	Standard Research
Starts:	24 January 2008	Ends:	23 August 2008	Value (£):	44,237
EPSRC Research Topic Classifications:	Fundamentals of Computing
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
Methods for correct-by-construction software development are finding more and more applications. A fundamental technology here is the application of methods based on the propositions-as-types/proofs-as-programs interpretation of constructive logics to particularproblems. The research proposed here is twofold.The first proposed research is the application of the proofs-as-programs methodology to a fundamental problem in constraint programming. We intend to constructively prove a theorem about establishing generalized arc consistency (GAC) whose proof will implicitly contain an algorithm for synthesizing watched literal propagators. This work will be collaborative between the visitor James Caldwell and Ian Gent and his colleagues working on the CIRCA project. The second proposed research workpackage is more directly related to the proofs-as-programs methodology. In this part of the project, we propose to examine methods forefficiently extracting programs from proofs in a certain class of logical system: multi-succedent intuitionistic sequent calculi. Theoretical results show that proofs in these calculi can be much smaller than proofs in the more widely used natural deduction based or single succedent based logical systems. Under the auspices of this grant we intend to explore methods of extracting programs from formal proofs in these more efficient proof systems. The goal here is to extract readable and efficient programs from these proofs. This research will be performed collaboratively between the visitor James Caldwell and Roy Dyckhoff.
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.st-and.ac.uk