Proofs, programs, processes

DOI10.1007/S00224-011-9325-8zbMath1280.68078OpenAlexW2076405698MaRDI QIDQ693063

Ulrich Berger, Monika Seisenberger

Publication date: 7 December 2012

Published in: Theory of Computing Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00224-011-9325-8

zbMATH Keywords

realizabilityprogram extractioncoinductionexact real number computationverified programs

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Relative consistency and interpretations (03F25)

Related Items (9)

Limits of real numbers in the binary signed digit representation ⋮ Eliminating disjunctions by disjunction elimination ⋮ Extracting total Amb programs from proofs ⋮ Nonflatness and totality ⋮ Type-theoretic approaches to ordinals ⋮ Intuitionistic fixed point logic ⋮ On the Constructive and Computational Content of Abstract Mathematics ⋮ Computing with continuous objects: a uniform co-inductive approach ⋮ Polynomial time over the reals with parsimony

Uses Software

• Unnamed Item
• Haskell

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A certified, corecursive implementation of exact real numbers
• Coinduction for exact real number computation
• Realizability interpretation of proofs in constructive analysis
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Dependent choice, `quote' and the clock
• Semantics of a sequential language for exact real-number computation
• Exploring the Computational Content of the Infinite Pigeonhole Principle
• From coinductive proofs to exact real arithmetic: theory and applications
• Structural Analysis of Narratives with the Coq Proof Assistant
• Constructive analysis, types and exact real numbers
• Affine functions and series with co-inductive real numbers
• Hybrid Functional Interpretations
• Coinductive Formal Reasoning in Exact Real Arithmetic
• From Coinductive Proofs to Exact Real Arithmetic

This page was built for publication: Proofs, programs, processes