scientific article; zbMATH DE number 7106521
From MaRDI portal
Publication:5195290
DOI10.6092/issn.1972-5787/8124zbMath1451.68329MaRDI QIDQ5195290
Damien Rouhling, Cyril Cohen, Reynald Affeldt
Publication date: 18 September 2019
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Foundations: limits and generalizations, elementary topology of the line (26A03) Formalization of mathematics in connection with theorem provers (68V20)
Related Items (9)
Unnamed Item ⋮ Competing Inheritance Paths in Dependent Type Theory: A Case Study in Functional Analysis ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Measure construction by extension in dependent type theory with application to integration ⋮ Formally-verified round-off error analysis of Runge-Kutta methods ⋮ Unnamed Item ⋮ Nine Chapters of Analytic Number Theory in Isabelle/HOL. ⋮ A trustful monad for axiomatic reasoning with probability and nondeterminism
Uses Software
Cites Work
- A formal proof in Coq of Lasalle's invariance principle
- Coquelicot: a user-friendly library of real analysis for Coq
- A fistful of dollars: formalizing asymptotic complexity claims via deductive program verification
- Proving divide and conquer complexities in Isabelle/HOL
- Construction of Real Algebraic Numbers in Coq
- Packaging Mathematical Structures
- A Modular Formalisation of Finite Group Theory
- Automated Reasoning
- Canonical Structures for the Working Coq User
- Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
- Homotopy Type Theory: Univalent Foundations of Mathematics
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication:
