Details of Grant 

EPSRC Reference:	GR/S58522/01
Title:	Abstract Stone Duality
Principal Investigator:	Aczel, Professor P
Other Investigators:	Rydeheard, Dr D Schalk, Dr AC
Researcher Co-Investigators:	Dr H Simmons
Project Partners:
Department:	Computer Science
Organisation:	University of Manchester, The
Scheme:	Standard Research (Pre-FEC)
Starts:	01 September 2003	Ends:	31 December 2006	Value (£):	231,876
EPSRC Research Topic Classifications:	Fundamentals of Computing Logic & Combinatorics
EPSRC Industrial Sector Classifications:	No relevance to Underpinning Sectors
Related Grants:
Panel History:
Summary on Grant Application Form
Computer Science has enjoyed topological interpretations for thirty years, but arbitrary infinite joins have precluded the converse, a computational interpretation of general topology. Abstract Stone Duality (ASD) is a type theory in which the topology on a space is an exponential with a lambdacalculus, not an infinitary lattice. But instead of rewriting old proofs in a pre-conceived logic, it exploits a deep mathematical theme, Stone duality, reconciling conceptual and computational traditions in mathematics. ASD gives a computational interpretation to continuous functions, not only for domains but between all locally compact spaces, including those from geometry. Published work develops the necessary infrastructure, defining notions such as compact Hausdorff spaces very naturally, with lattice duality between open and closed phenomena. Recent work generalises interval analysis from the real numbers to other spaces, but the intervals themselves are only mentioned during compilation. The categorical structure allows a conceptual development, whilst the lambda-calculus handles higher types. This will be used to investigate differential and integral calculus. ASD also throws new light on discrete mathematics, giving a computational status to the powerset and other constructions, following Stone's dictum that they carry topologies. ASD can be implemented by compilation by continuation-passing into a language that combines functional and logic programming.
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.man.ac.uk