Quantitative continuity and Computable Analysis in Coq
From MaRDI portal
Cites work
- A constructive manifestation of the Kleene-Kreisel continuous functionals
- A formalization of metric spaces in HOL Light
- A new Characterization of Type-2 Feasibility
- Bounded time computation on metric spaces and Banach spaces
- Call-by-value lambda calculus as a model of computation in Coq
- Complexity theory for operators in analysis
- Computability on computable metric spaces
- Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
- Computing Solutions of Symmetric Hyperbolic Systems of PDE's
- Constructivism in mathematics. An introduction. Volume II
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Extended admissibility.
- Game semantics approach to higher-order complexity
- Higher-order computability
- scientific article; zbMATH DE number 3144514 (Why is no real title available?)
- scientific article; zbMATH DE number 4070894 (Why is no real title available?)
- scientific article; zbMATH DE number 42077 (Why is no real title available?)
- scientific article; zbMATH DE number 54277 (Why is no real title available?)
- scientific article; zbMATH DE number 52121 (Why is no real title available?)
- scientific article; zbMATH DE number 1969324 (Why is no real title available?)
- scientific article; zbMATH DE number 1460545 (Why is no real title available?)
- scientific article; zbMATH DE number 1746043 (Why is no real title available?)
- scientific article; zbMATH DE number 1746052 (Why is no real title available?)
- scientific article; zbMATH DE number 3216998 (Why is no real title available?)
- Mathematical Knowledge Management
- Multi-valued functions in computability theory
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- On a simple definition of computable function of a real variable‐with applications to functions of a complex variable
- On a theory of computation and complexity over the real numbers: 𝑁𝑃- completeness, recursive functions and universal machines
- On Computable Numbers, with an Application to the Entscheidungsproblem
- On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
- On the constructive Dedekind reals
- On the definitions of computable real continuous functions
- On the topological aspects of the theory of represented spaces
- Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving
- Parametrised second-order complexity theory with applications to the study of interval computation
- Polynomial and abstract subrecursive classes
- Real benefit of promises and advice
- Recursively enumerable sets and degrees
- Relative computability and uniform continuity of relations
- Representations and evaluation strategies for feasibly approximable functions
- Second-order linear-time computability with applications to computable analysis
- Spaces allowing Type‐2 Complexity Theory revisited
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Theorem Proving in Higher Order Logics
- Theory of representations
- Towards computability of elliptic boundary value problems in variational formulation
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- δ as a Continuous Function of x and ɛ
Cited in
(2)
This page was built for publication: Quantitative continuity and Computable Analysis in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5875440)
