Proofs, programs, processes
DOI10.1007/S00224-011-9325-8zbMATH Open1280.68078OpenAlexW2076405698MaRDI QIDQ693063FDOQ693063
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
Recommendations
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Functional programming and lambda calculus (68N18) Relative consistency and interpretations (03F25)
Cites Work
- Coinduction for exact real number computation
- Title not available (Why is that?)
- Dependent choice, `quote' and the clock
- Title not available (Why is that?)
- Exploring the computational content of the infinite pigeonhole principle
- Constructive analysis, types and exact real numbers
- Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
- Continuous functions on final coalgebras
- Hybrid Functional Interpretations
- Structural Analysis of Narratives with the Coq Proof Assistant
- Realizability interpretation of proofs in constructive analysis
- Semantics of a sequential language for exact real-number computation
- From coinductive proofs to exact real arithmetic: theory and applications
- Realisability for induction and coinduction with applications to constructive analysis
- Affine functions and series with co-inductive real numbers
- Coinductive Formal Reasoning in Exact Real Arithmetic
- From Coinductive Proofs to Exact Real Arithmetic
- A certified, corecursive implementation of exact real numbers
Cited In (18)
- Type-theoretic approaches to ordinals
- Nonflatness and totality
- Proofs, programs, processes
- Extracting total Amb programs from proofs
- Realisability for induction and coinduction with applications to constructive analysis
- Proofs and programs
- On the Constructive and Computational Content of Abstract Mathematics
- Procedural representation of CIC proof terms
- Proofs as processes
- Computing with continuous objects: a uniform co-inductive approach
- Constructive analysis with witnesses
- Title not available (Why is that?)
- Limits of real numbers in the binary signed digit representation
- Program extraction via typed realisability for induction and coinduction
- Intuitionistic fixed point logic
- Eliminating disjunctions by disjunction elimination
- Title not available (Why is that?)
- Polynomial time over the reals with parsimony
Uses Software
This page was built for publication: Proofs, programs, processes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q693063)
