General Recursion and Formal Topology

12 pages•Published: May 15, 2012

Claudio Sacerdoti Coen and Silvio Valentini

Abstract

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.

Keyphrases: general recursion, inductively generated formal topologies, recursion operator

In: Ekaterina Komendantskaya, Ana Bove and Milad Niqui (editors). PAR-10. Partiality and Recursion in Interactive Theorem Provers, vol 5, pages 72-83.

Links:	https://easychair.org/publications/paper/q9b2
	https://doi.org/10.29007/hl75

BibTeX entry

@inproceedings{PAR-10:General_Recursion_Formal_Topology,
  author    = {Claudio Sacerdoti Coen and Silvio Valentini},
  title     = {General Recursion and Formal Topology},
  booktitle = {PAR-10. Partiality and Recursion in Interactive Theorem Provers},
  editor    = {Ekaterina Komendantskaya and Ana Bove and Milad Niqui},
  series    = {EPiC Series in Computing},
  volume    = {5},
  publisher = {EasyChair},
  bibsource = {EasyChair, https://easychair.org},
  issn      = {2398-7340},
  url       = {/publications/paper/q9b2},
  doi       = {10.29007/hl75},
  pages     = {72-83},
  year      = {2012}}

Download PDF Open PDF in browser