Proofs and Computations

DOI10.1017/CBO9781139031905zbMath1294.03006OpenAlexW4205623740MaRDI QIDQ3110202

Stanley S. Wainer, Helmut Schwichtenberg

Publication date: 27 January 2012

Full work available at URL: https://doi.org/10.1017/cbo9781139031905

zbMATH Keywords

connections between proof theory and recursive function theory

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Complexity of computation (including implicit computational complexity) (03D15) Functionals in proof theory (03F10) Second- and higher-order arithmetic and fragments (03F35) Recursive ordinals and ordinal notations (03F15) Gödel numberings and issues of incompleteness (03F40) Higher-type and set recursion theory (03D65)

Related Items (43)

A stream calculus of bottomed sequences for real number computation ⋮ Limits of real numbers in the binary signed digit representation ⋮ Limit spaces with approximations ⋮ Atomicity, coherence of information, and point-free structures ⋮ Proof-relevance in Bishop-style constructive mathematics ⋮ Extracting a DPLL Algorithm ⋮ Direct spectra of Bishop spaces and their limits ⋮ Unnamed Item ⋮ Unnamed Item ⋮ SELF-REFERENCE UPFRONT: A STUDY OF SELF-REFERENTIAL GÖDEL NUMBERINGS ⋮ Eliminating disjunctions by disjunction elimination ⋮ Arithmetical conservation results ⋮ Lookahead analysis in exact real arithmetic with logical methods ⋮ A note on equality in finite‐type arithmetic ⋮ An intuitionistic formula hierarchy based on high‐school identities ⋮ A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory ⋮ Normal forms, linearity, and prime algebraicity over nonflat domains ⋮ Maximal elements with minimal logic ⋮ Extracting total Amb programs from proofs ⋮ Nonflatness and totality ⋮ A constructive notion of codimension ⋮ Intuitionistic fixed point logic ⋮ Unnamed Item ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ About Truth and Types ⋮ Higman’s Lemma and Its Computational Content ⋮ Pointwise Transfinite Induction and a Miniaturized Predicativity ⋮ On the Constructive and Computational Content of Abstract Mathematics ⋮ From Mathesis Universalis to Provability, Computability, and Constructivity ⋮ Computational Interpretations of Classical Reasoning: From the Epsilon Calculus to Stateful Programs ⋮ Computing with continuous objects: a uniform co-inductive approach ⋮ Program extraction in exact real arithmetic ⋮ Principles for object-linguistic consequence: from logical to irreflexive ⋮ GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN–PÉTER FUNCTION ⋮ Unnamed Item ⋮ Cut Elimination, Substitution and Normalisation ⋮ Tiered Arithmetics ⋮ Feferman and the Truth ⋮ The Parametric Complexity of Lossy Counter Machines ⋮ An adequacy theorem for dependent type theory ⋮ Complexity Hierarchies beyond Elementary ⋮ On preserving the computational content of mathematical proofs: toy examples for a formalising strategy ⋮ An algorithmic version of Zariski's lemma

This page was built for publication: Proofs and Computations