Well-definedness and observational equivalence for inductive–coinductive programs

DOI10.1093/LOGCOM/EXV091MaRDI QIDQ5225850zbMATH OpenOpenAlexFDO

Authors Henning Basold, Helle Hvid Hansen

Publication date 29 July 2019

Published in Journal Of Logic And Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/exv091

zbMATH Keywords

coinductive typesinductive typesobservational equivalenceproductivityterminationtesting logic

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical semantics of formal languages (18C50) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Program equivalence is coinductive
• Inductive completeness of logics of programs
• Inductive Logic Programming
• scientific article; zbMATH DE number 1670488
• scientific article; zbMATH DE number 2061716
• Deductive and inductive synthesis of equational programs
• scientific article; zbMATH DE number 2247255
• Inductive assertions and operational semantics

Cited in

(3)

• scientific article; zbMATH DE number 2185719 (Why is no real title available?)
• Mixed Inductive/Coinductive Types and Strong Normalization
• Dependent type refinements for futures

This page was built for publication: Well-definedness and observational equivalence for inductive–coinductive programs

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