Proofs, programs, processes
From MaRDI portal
Publication:693063
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
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
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
