Quantitative continuity and Computable Analysis in Coq
From MaRDI portal
Publication:5875440
DOI10.4230/LIPIcs.ITP.2019.28OpenAlexW2979066956MaRDI QIDQ5875440
Laurent Théry, Florian Steinberg, Holger Thies
Publication date: 3 February 2023
Full work available at URL: https://hal.archives-ouvertes.fr/hal-02426470
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Uses Software
Cites Work
- Unnamed Item
- 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
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- A formalization of metric spaces in HOL Light
- Towards computability of elliptic boundary value problems in variational formulation
- On the constructive Dedekind reals
- Theory of representations
- Constructivism in mathematics. An introduction. Volume II
- Polynomial and abstract subrecursive classes
- Extended admissibility.
- Distant decimals of \(\pi \): formal proofs of some algorithms computing them and guarantees of exact computation
- Parameterized complexity for uniform operators on multidimensional analytic functions and ODE solving
- Computability on computable metric spaces
- Type-two polynomial-time and restricted lookahead
- 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
- Game semantics approach to higher-order complexity
- δ as a Continuous Function of x and ɛ
- Multi-valued Functions in Computability Theory
- Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
- Relative computability and uniform continuity of relations
- Complexity Theory for Operators in Analysis
- Spaces allowing Type‐2 Complexity Theory revisited
- On the definitions of computable real continuous functions
- Higher-Order Computability
- On a simple definition of computable function of a real variable‐with applications to functions of a complex variable
- Recursively enumerable sets and degrees
- On a theory of computation and complexity over the real numbers: 𝑁𝑃- completeness, recursive functions and universal machines
- A new Characterization of Type-2 Feasibility
- Computing Solutions of Symmetric Hyperbolic Systems of PDE's
- Representations and evaluation strategies for feasibly approximable functions
- Bounded time computation on metric spaces and Banach spaces
- Mathematical Knowledge Management
- Real Benefit of Promises and Advice
- The Picard Algorithm for Ordinary Differential Equations in Coq
- Theorem Proving in Higher Order Logics
- On the topological aspects of the theory of represented spaces
- On Computable Numbers, with an Application to the Entscheidungsproblem
- On Computable Numbers, with an Application to the Entscheidungsproblem. A Correction
This page was built for publication: Quantitative continuity and Computable Analysis in Coq
