Proofs, programs, processes

DOI10.1007/S00224-011-9325-8MaRDI QIDQ693063zbMATH OpenOpenAlexFDO

Authors 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

realizabilitycoinductionprogram extractionexact real number computationverified programs

Mathematics Subject Classification ID

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

Recommendations

• Proofs, programs, processes
• From coinductive proofs to exact real arithmetic: theory and applications
• Program extraction in exact real arithmetic
• Program extraction via typed realisability for induction and coinduction
• From Coinductive Proofs to Exact Real Arithmetic

Cites work

• scientific article; zbMATH DE number 1552509 (Why is no real title available?)
• scientific article; zbMATH DE number 2090725 (Why is no real title available?)
• A certified, corecursive implementation of exact real numbers
• Affine functions and series with co-inductive real numbers
• Coinduction for exact real number computation
• Coinductive Formal Reasoning in Exact Real Arithmetic
• Constructive analysis, types and exact real numbers
• Continuous functions on final coalgebras
• Dependent choice, `quote' and the clock
• Exploring the computational content of the infinite pigeonhole principle
• From Coinductive Proofs to Exact Real Arithmetic
• From coinductive proofs to exact real arithmetic: theory and applications
• Hybrid Functional Interpretations
• Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies
• Realisability for induction and coinduction with applications to constructive analysis
• Realizability interpretation of proofs in constructive analysis
• Semantics of a sequential language for exact real-number computation
• Structural analysis of narratives with the Coq proof assistant

Cited in

(24)

• Proofs as processes
• Polynomial time over the reals with parsimony
• Extracting total Amb programs from proofs
• Computing with continuous objects: a uniform co-inductive approach
• Nonflatness and totality
• Proofs and programs
• Extracting non-deterministic concurrent programs
• scientific article; zbMATH DE number 2003158 (Why is no real title available?)
• Limits of real numbers in the binary signed digit representation
• Constructive analysis with witnesses
• scientific article; zbMATH DE number 7526292 (Why is no real title available?)
• A coinductive semantics of the unlimited register machine
• Proofs, programs, processes
• Program extraction via typed realisability for induction and coinduction
• Minlog -- a tool for program extraction supporting algebras and coalgebras
• Procedural representation of CIC proof terms
• Type-theoretic approaches to ordinals
• Program extraction from proofs: the fan theorem for uniformly coconvex bars
• On the constructive and computational content of abstract mathematics
• Realisability for induction and coinduction with applications to constructive analysis
• From coinductive proofs to exact real arithmetic: theory and applications
• Optimized program extraction for induction and coinduction
• Eliminating disjunctions by disjunction elimination
• Intuitionistic fixed point logic

Describes a project that uses

Uses Software

• Coq
• Haskell

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)