Realizability interpretation of coinductive definitions and program synthesis with streams

DOI10.1016/0304-3975(94)90204-6zbMath0801.68027OpenAlexW2054667551MaRDI QIDQ1314420

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

verificationprogram transformationprogram extractionprogram synthesisstreamsrealizability interpretationgreatest fixed pointcoinductive definitions

Mathematics Subject Classification ID

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

Related Items (1)

Dual Calculus with Inductive and Coinductive Types

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• A functional programming approach to the specification and verification of concurrent systems
• Program synthesis using realizability
• Monotone recursive definition of predicates and its realizability interpretation

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