Proofs and computations
From MaRDI portal
Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) Complexity of computation (including implicit computational complexity) (03D15) Higher-type and set recursion theory (03D65) Functionals in proof theory (03F10) Recursive ordinals and ordinal notations (03F15) Second- and higher-order arithmetic and fragments (03F35) Gödel numberings and issues of incompleteness (03F40)
Recommendations
Cited in
(72)- Kleene computable functionals and the higher order existence property
- A slow growing analogue to Buchholz' proof
- Handbook of proof theory
- Eliminating disjunctions by disjunction elimination
- Arithmetical conservation results
- On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
- An algorithmic version of Zariski's lemma
- Intuitionistic fixed point logic
- Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting)
- An adequacy theorem for dependent type theory
- A constructive notion of codimension
- A stream calculus of bottomed sequences for real number computation
- Lookahead analysis in exact real arithmetic with logical methods
- A finitization of Littlewood's Tauberian theorem and an application in Tauberian remainder theory
- Complexity hierarchies beyond elementary
- Limit spaces with approximations
- Atomicity, coherence of information, and point-free structures
- scientific article; zbMATH DE number 5899421 (Why is no real title available?)
- scientific article; zbMATH DE number 5862941 (Why is no real title available?)
- Extracting a DPLL algorithm
- 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
- A framework for priority arguments
- scientific article; zbMATH DE number 4033738 (Why is no real title available?)
- scientific article; zbMATH DE number 481375 (Why is no real title available?)
- scientific article; zbMATH DE number 2006635 (Why is no real title available?)
- Proof and computation. Digitization in mathematics, computer science, and philosophy. Based on the international autumn school ``Proof and computation, Fischbachau, Germany, October 3--8, 2016
- Nonflatness and totality
- GOODSTEIN SEQUENCES BASED ON A PARAMETRIZED ACKERMANN–PÉTER FUNCTION
- Direct spectra of Bishop spaces and their limits
- Logic for exact real arithmetic
- Proof and computation II. From proof theory and univalent mathematics to program extraction and verification. Based on the international autumn school ``Proof and computation, September 20--26, 2019
- Modal functional (``Dialectica) interpretation
- Limits of real numbers in the binary signed digit representation
- Proof-relevance in Bishop-style constructive mathematics
- The Parametric Complexity of Lossy Counter Machines
- A note on equality in finite‐type arithmetic
- An intuitionistic formula hierarchy based on high‐school identities
- Normal forms, linearity, and prime algebraicity over nonflat domains
- A syntactic approach to continuity of T-definable functionals
- Ordinal Analysis with an Introduction to Proof Theory
- Computing with continuous objects: a uniform co-inductive approach
- Cut elimination, substitution and normalisation
- Tiered arithmetics
- Feferman and the Truth
- Conversations with Bill about functionals and terms
- scientific article; zbMATH DE number 5269066 (Why is no real title available?)
- scientific article; zbMATH DE number 5070526 (Why is no real title available?)
- Program extraction in exact real arithmetic
- Constructive domains with classical witnesses
- SELF-REFERENCE UPFRONT: A STUDY OF SELF-REFERENTIAL GÖDEL NUMBERINGS
- Maximal elements with minimal logic
- Extracting total Amb programs from proofs
- Proofs and algorithms. An introduction to logic and computability
- Another combination of classical and intuitionistic conditionals
- Sufficient convexity and best approximation
- Subsystems of true arithmetic and hierarchies of functions
- Constructive validity of a generalized Kreisel-Putnam rule
- Strong negation in the theory of computable functionals TCF
- Conservation as translation
- On the Weihrauch degree of the additive Ramsey theorem
- Hilbert's tenth problem for term algebras with a substitution operator
- Complemented subsets and Boolean-valued, partial functions
- Peano arithmetic, games and descent recursion
- Principles for object-linguistic consequence: from logical to irreflexive
- Verified program extraction in number theory: the fundamental theorem of arithmetic and relatives
- Lectures on the Curry-Howard isomorphism
- Proof theory. The first step into impredicativity
This page was built for publication: Proofs and computations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3110202)
