Realisability for induction and coinduction with applications to constructive analysis

MaRDI QIDQ3075213zbMATH OpenFDO

Authors Ulrich Berger

Publication date 10 February 2011

Full work available at URL http://www.jucs.org/jucs_16_18/realisability_for_induction_and

zbMATH Keywords

coinductioncomputable analysisexact real number computationextensions of first-order theoriesprogram extractionrealisability interpretationuntyped \(\lambda \)-calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Inductive definability (03D70) Computation over the reals, computable analysis (03D78) Constructive and recursive analysis (03F60)

Recommendations

• Realisability and adequacy for (co)induction
• Program extraction via typed realisability for induction and coinduction
• Proofs, programs, processes
• Proofs, programs, processes
• From coinductive proofs to exact real arithmetic: theory and applications

Cited in

(26)

• Recursion over realizability structures
• Induction and recursion on the partial real line with applications to Real PCF
• Realizability interpretation of coinductive definitions and program synthesis with streams
• Axiomatizing higher-order Kleene realizability
• Intuitionistic formal theories with realizability in subrecursive classes
• Optimized program extraction for induction and coinduction
• \textsc{Prawf}: an interactive proof system for program extraction
• Intuitionistic fixed point logic
• Type-theoretic approaches to ordinals
• Realisability and adequacy for (co)induction
• Global semantic typing for inductive and coinductive computing
• Program extraction via typed realisability for induction and coinduction
• Typed vs. untyped realizability
• On the constructive and computational content of abstract mathematics
• Proofs, programs, processes
• From Coinductive Proofs to Exact Real Arithmetic
• TWO REALIZABILITY INTERPRETATIONS OF MONOTONE INDUCTIVE DEFINITIONS
• A realizability interpretation of Church's simple theory of types
• scientific article; zbMATH DE number 2085168 (Why is no real title available?)
• scientific article; zbMATH DE number 1841837 (Why is no real title available?)
• A TYPE-FREE THEORY OF HALF-MONOTONE INDUCTIVE DEFINITIONS
• scientific article; zbMATH DE number 832104 (Why is no real title available?)
• A coinductive semantics of the unlimited register machine
• Computing with continuous objects: a uniform co-inductive approach
• Internalising modified realisability in constructive type theory
• Proofs, programs, processes

Describes a project that uses

Uses Software

• RZ

This page was built for publication: Realisability for induction and coinduction with applications to constructive analysis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3075213)