scientific article; zbMATH DE number 7350782
From MaRDI portal
Publication:4989411
Laurent Théry, Florian Steinberg, Holger Thies
Publication date: 25 May 2021
Full work available at URL: https://arxiv.org/abs/1904.13203
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items (2)
Axiomatic reals and certified efficient exact real computation ⋮ On preserving the computational content of mathematical proofs: toy examples for a formalising strategy
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A constructive manifestation of the Kleene-Kreisel continuous functionals
- Closed choice and a uniform low basis theorem
- Partial combinatory algebras of functions
- Towards computability of elliptic boundary value problems in variational formulation
- Theory of representations
- Constructivism in mathematics. An introduction. Volume I
- Polynomial and abstract subrecursive classes
- A taxonomy of complexity classes of functions
- Extended admissibility.
- Comparing representations for function spaces in computable analysis
- Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving
- Computability on computable metric spaces
- Quasi-Polish spaces
- Type-two polynomial-time and restricted lookahead
- Coquelicot: a user-friendly library of real analysis for Coq
- Parametrised second-order complexity theory with applications to the study of interval computation
- Call-by-value lambda calculus as a model of computation in Coq
- Second-order linear-time computability with applications to computable analysis
- δ as a Continuous Function of x and ɛ
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Relative computability and uniform continuity of relations
- Complexity Theory for Operators in Analysis
- The Vitali Covering Theorem in the Weihrauch Lattice
- Formalization of real analysis: a survey of proof assistants and libraries
- Many-one reductions and the category of multivalued functions
- Effective Choice and Boundedness Principles in Computable Analysis
- Spaces allowing Type‐2 Complexity Theory revisited
- On the definitions of computable real continuous functions
- Higher-Order Computability
- A Modular Formalisation of Finite Group Theory
- Proving Bounds on Real-Valued Functions with Computations
- A Continuous Modulus of Continuity
- On a simple definition of computable function of a real variable‐with applications to functions of a complex variable
- Recursively enumerable sets and degrees
- A new Characterization of Type-2 Feasibility
- Computing Solutions of Symmetric Hyperbolic Systems of PDE's
- Mathematical Knowledge Management
- Real Benefit of Promises and Advice
- The Picard Algorithm for Ordinary Differential Equations in Coq
- On the topological aspects of the theory of represented spaces
- On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
- Fixed Point Theorems for Multi-Valued Transformations
This page was built for publication:
