A computer-verified monadic functional implementation of the integral

DOI10.1016/J.TCS.2010.05.031zbMATH Open1209.68108OpenAlexW2078543558MaRDI QIDQ987984FDOQ987984

Authors: Russell O'Connor, Bas Spitters 

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

Recommendations

• A monadic, functional implementation of real numbers
• A functional algorithm for exact real integration with invariant measures
• scientific article; zbMATH DE number 1222580
• Realizability interpretation of proofs in constructive analysis
• Constructive Mathematics and Functional Programming (Abstract)

zbMATH Keywords

functional programmingmonadstype theoryexact real analysis

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Cites Work

• Mathematical Knowledge Management
• Theorem Proving in Higher Order Logics
• The crisis in contemporary mathematics
• Title not available (Why is that?)
• Setoids in type theory
• Real numbers and other completions
• Title not available (Why is that?)
• Lectures on the Curry-Howard isomorphism
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Title not available (Why is that?)
• Title not available (Why is that?)
• Comprehending monads
• Title not available (Why is that?)
• The calculus of constructions
• Certified Exact Transcendental Real Number Computation in Coq
• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Computing with classical real numbers
• 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
• Title not available (Why is that?)
• Types for Proofs and Programs

Cited In (12)

• Type classes for mathematics in type theory
• A functional algorithm for exact real integration with invariant measures
• Computer Certified Efficient Exact Reals in Coq
• Formally verified approximations of definite integrals
• Formally verified approximations of definite integrals
• Verified interactive computation of definite integrals
• Wave equation numerical resolution: a comprehensive mechanized proof of a C program
• The gauge integral theory in HOL4
• Computable analysis with applications to dynamic systems
• Formalization of real analysis: a survey of proof assistants and libraries
• A monadic, functional implementation of real numbers
• Coquelicot: a user-friendly library of real analysis for Coq

Uses Software

• Coq
• C-CoRN
• PoplMark

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)