General Recursion and Formal Topology
Author(s) -
Claudio Sacerdoti Coen,
Silvio Valentini
Publication year - 2018
Publication title -
epic series in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 2398-7340
DOI - 10.29007/hl75
Subject(s) - recursion (computer science) , network topology , computer science , computation , theoretical computer science , topology (electrical circuits) , type (biology) , algebra over a field , mathematics , algorithm , pure mathematics , combinatorics , ecology , biology , operating system
It is well known that general recursion cannot be expressed within Martin-Löf's type theory and that various approaches have been proposed to overcome this problem still maintaining the termination of the computation of the typable terms. In this work we propose a new approach to this problem based on the use of inductively generated formal topologies.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom