Proofs, programs, processes

DOI10.1007/978-3-642-13962-8_5MaRDI QIDQ3576189zbMATH OpenOpenAlexFDO

Authors Ulrich Berger, Monika Seisenberger

Publication date 29 July 2010

Published in Programs, Proofs, Processes (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.187.2805

zbMATH Keywords

coinductionprogram extractionrealisabilityexact real number computation

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
• Program extraction via typed realisability for induction and coinduction
• From coinductive proofs to exact real arithmetic: theory and applications
• Realisability and adequacy for (co)induction
• Realisability for induction and coinduction with applications to constructive analysis

Cited in

(15)

• A realizability interpretation of Church's simple theory of types
• Proofs, programs, processes
• Programs, proofs, processes. 6th conference on computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30--July 4, 2010. Proceedings
• Program extraction in exact real arithmetic
• Realisability for induction and coinduction with applications to constructive analysis
• Proofs and programs
• Typed vs. untyped realizability
• Proofs as processes
• The theory of spectrum exchangeability
• Computing with continuous objects: a uniform co-inductive approach
• Optimized program extraction for induction and coinduction
• From coinductive proofs to exact real arithmetic: theory and applications
• Program extraction via typed realisability for induction and coinduction
• Intuitionistic fixed point logic
• scientific article; zbMATH DE number 7526292 (Why is no real title available?)

Describes a project that uses

Uses Software

• Minlog
• 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 Q3576189)