Parametric Church's thesis: synthetic computability without choice

DOI10.1007/978-3-030-93100-1_6OpenAlexW4200256317MaRDI QIDQ2151397

Yannick Forster

Publication date: 1 July 2022

Full work available at URL: https://arxiv.org/abs/2112.11781

Mathematics Subject Classification ID

Logic in computer science (03B70)

Uses Software

• Coq
• ETPS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The consistency of some intuitionistic and constructive principles with a set theory
• Incompleteness in intuitionistic metamathematics
• Constructivism in mathematics. An introduction. Volume II
• Classical recursion theory. The theory of functions and sets of natural numbers.
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Weak call-by-value lambda calculus as a model of computation in Coq
• Consistency of the intensional level of the minimalist foundation with Church's thesis and axiom of choice
• An introduction to mathematical logic and type theory: To truth through proof.
• Church's thesis without tears
• Mechanised Computability Theory
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES
• An injection from the Baire space to natural numbers
• Classes of Recursively Enumerable Sets and Their Decision Problems
• Recursive Predicates and Quantifiers
• On the interpretation of intuitionistic number theory

This page was built for publication: Parametric Church's thesis: synthetic computability without choice