Realizability interpretation of coinductive definitions and program synthesis with streams

DOI10.1016/0304-3975(94)90204-6MaRDI QIDQ1314420zbMATH OpenOpenAlexFDO

Authors Makoto Tatsuta

Publication date 29 November 1994

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(94)90204-6

zbMATH Keywords

coinductive definitionsgreatest fixed pointprogram extractionprogram synthesisprogram transformationrealizability interpretationstreamsverification

Mathematics Subject Classification ID

Logic in computer science (03B70) Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 970725
• Proofs, programs, processes
• Program extraction via typed realisability for induction and coinduction
• Proofs, programs, processes
• Realisability for induction and coinduction with applications to constructive analysis

Cites work

• A functional programming approach to the specification and verification of concurrent systems
• scientific article; zbMATH DE number 3900744 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• Monotone recursive definition of predicates and its realizability interpretation
• Program synthesis using realizability

Cited in

(4)

• Program synthesis using realizability
• Program extraction via typed realisability for induction and coinduction
• Dual Calculus with Inductive and Coinductive Types
• scientific article; zbMATH DE number 970725 (Why is no real title available?)

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: Realizability interpretation of coinductive definitions and program synthesis with streams

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