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