A computer-verified monadic functional implementation of the integral

DOI10.1016/j.tcs.2010.05.031zbMath1209.68108OpenAlexW2078543558MaRDI QIDQ987984

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

zbMATH Keywords

monadsfunctional programmingtype theoryexact real analysis

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Wave equation numerical resolution: a comprehensive mechanized proof of a C program, 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, Computer Certified Efficient Exact Reals in Coq, Computable analysis with applications to dynamic systems, Type classes for mathematics in type theory, Formally Verified Approximations of Definite Integrals

Uses Software

• Coq
• C-CoRN
• PoplMark

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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
• Realizability interpretation of proofs in constructive analysis
• A constructive theory of continuous domains suitable for implementation
• The calculus of constructions
• The crisis in contemporary mathematics
• A compiled implementation of strong reduction
• Constructive analysis, types and exact real numbers
• A monadic, functional implementation of real numbers
• Certified Exact Transcendental Real Number Computation in Coq
• Program Extraction from Large Proof Developments
• From Coinductive Proofs to Exact Real Arithmetic
• Comprehending monads
• Setoids in type theory
• Extensional Constructs in Intensional Type Theory
• The view from the left
• Mathematical Knowledge Management
• Applicative programming with effects
• Real numbers and other completions
• Theorem Proving in Higher Order Logics
• Foundations of Software Science and Computational Structures
• Types for Proofs and Programs