A computer-verified monadic functional implementation of the integral
From MaRDI portal
Publication:987984
Recommendations
Cites work
- scientific article; zbMATH DE number 4179333 (Why is no real title available?)
- scientific article; zbMATH DE number 3859117 (Why is no real title available?)
- scientific article; zbMATH DE number 4152376 (Why is no real title available?)
- scientific article; zbMATH DE number 50149 (Why is no real title available?)
- scientific article; zbMATH DE number 53088 (Why is no real title available?)
- scientific article; zbMATH DE number 1222580 (Why is no real title available?)
- scientific article; zbMATH DE number 1302061 (Why is no real title available?)
- scientific article; zbMATH DE number 2003153 (Why is no real title available?)
- scientific article; zbMATH DE number 204193 (Why is no real title available?)
- scientific article; zbMATH DE number 1405640 (Why is no real title available?)
- scientific article; zbMATH DE number 3291139 (Why is no real title available?)
- scientific article; zbMATH DE number 3296291 (Why is no real title available?)
- scientific article; zbMATH DE number 2222246 (Why is no real title available?)
- scientific article; zbMATH DE number 4189687 (Why is no real title available?)
- A compiled implementation of strong reduction
- A constructive theory of continuous domains suitable for implementation
- A monadic, functional implementation of real numbers
- Applicative programming with effects
- Certified Exact Transcendental Real Number Computation in Coq
- Comprehending monads
- Computing with classical real numbers
- Constructive analysis, types and exact real numbers
- Extensional Constructs in Intensional Type Theory
- Foundations of Software Science and Computational Structures
- From Coinductive Proofs to Exact Real Arithmetic
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Lectures on the Curry-Howard isomorphism
- Mathematical Knowledge Management
- Program extraction from large proof developments
- Real numbers and other completions
- Realizability interpretation of proofs in constructive analysis
- Setoids in type theory
- The calculus of constructions
- The crisis in contemporary mathematics
- The view from the left
- Theorem Proving in Higher Order Logics
- Types for Proofs and Programs
Cited in
(12)- Formalization of real analysis: a survey of proof assistants and libraries
- Formally verified approximations of definite integrals
- Formally verified approximations of definite integrals
- The gauge integral theory in HOL4
- A functional algorithm for exact real integration with invariant measures
- Type classes for mathematics in type theory
- A monadic, functional implementation of real numbers
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Verified interactive computation of definite integrals
- Coquelicot: a user-friendly library of real analysis for Coq
- Computer Certified Efficient Exact Reals in Coq
- Computable analysis with applications to dynamic systems
This page was built for publication: A computer-verified monadic functional implementation of the integral
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q987984)
