A computer-verified monadic functional implementation of the integral
type: Item
instance of: scholarly article
title: A computer-verified monadic functional implementation of the integral
zbMATH Open document ID: 1209.68108
author: Russell O'Connor
author: Bas Spitters
published in: Theoretical Computer Science
publication date: 2010-08-24T00:00:00Z
Mathematics Subject Classification ID: 68N18
zbMATH DE Number: 5774340
zbMATH Keywords: type theory
zbMATH Keywords: functional programming
zbMATH Keywords: exact real analysis
zbMATH Keywords: monads
describes a project that uses: Coq
describes a project that uses: C-CoRN
describes a project that uses: PoplMark
MaRDI profile type: Publication
full work available at URL: j.tcs.2010.05.031
OpenAlex ID: W2078543558
cites work: Theorem Proving in Higher Order Logics
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Setoids in type theory
cites work: Q5579535
cites work: From Coinductive Proofs to Exact Real Arithmetic
cites work: Q5573965
cites work: The crisis in contemporary mathematics
cites work: A constructive theory of continuous domains suitable for implementation
cites work: Q5701018
cites work: Q4435465
cites work: Mathematical Knowledge Management
cites work: Program Extraction from Large Proof Developments
cites work: The calculus of constructions
cites work: Types for Proofs and Programs
cites work: Q5753923
cites work: Q4938619
cites work: A compiled implementation of strong reduction
cites work: Constructive analysis, types and exact real numbers
cites work: Extensional Constructs in Intensional Type Theory
cites work: Q3184782
cites work: Q4695311
cites work: Q3328540
cites work: Q4247306
cites work: The view from the left
cites work: Q3202991
cites work: Applicative programming with effects
cites work: Q3999860
cites work: A monadic, functional implementation of real numbers
cites work: Certified Exact Transcendental Real Number Computation in Coq
cites work: Real numbers and other completions
cites work: Q3481701
cites work: Foundations of Software Science and Computational Structures
cites work: Realizability interpretation of proofs in constructive analysis
cites work: Q4218119
cites work: Lectures on the Curry-Howard isomorphism
cites work: Q4003339
cites work: Comprehending monads
DOI: 10.1016/J.TCS.2010.05.031
description: scientific article; zbMATH DE number 5774340