A computer-verified monadic functional implementation of the integral
From MaRDI portal
Publication:987984
DOI10.1016/J.TCS.2010.05.031zbMATH Open1209.68108OpenAlexW2078543558MaRDI QIDQ987984FDOQ987984
Bas Spitters, Russell O'Connor
Publication date: 24 August 2010
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.tcs.2010.05.031
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Mathematical Knowledge Management
- Theorem Proving in Higher Order Logics
- The crisis in contemporary mathematics
- Setoids in type theory
- Real numbers and other completions
- Lectures on the Curry-Howard isomorphism
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Comprehending monads
- The calculus of constructions
- Certified Exact Transcendental Real Number Computation in Coq
- Constructive analysis, types and exact real numbers
- Extensional Constructs in Intensional Type Theory
- Applicative programming with effects
- The view from the left
- Realizability interpretation of proofs in constructive analysis
- From Coinductive Proofs to Exact Real Arithmetic
- A compiled implementation of strong reduction
- Foundations of Software Science and Computational Structures
- A constructive theory of continuous domains suitable for implementation
- A monadic, functional implementation of real numbers
- Program Extraction from Large Proof Developments
- Types for Proofs and Programs
Cited In (9)
- Type classes for mathematics in type theory
- Computer Certified Efficient Exact Reals in Coq
- Formally verified approximations of definite integrals
- Verified interactive computation of definite integrals
- Wave equation numerical resolution: a comprehensive mechanized proof of a C program
- Computable analysis with applications to dynamic systems
- Formalization of real analysis: a survey of proof assistants and libraries
- Formally Verified Approximations of Definite Integrals
- Coquelicot: a user-friendly library of real analysis for Coq
Uses Software
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)
