Proof methods for corecursive programs

MaRDI QIDQ5472879zbMATH OpenFDO

Authors Jeremy Gibbons, Graham Hutton

Publication date 19 June 2006

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Coalgebras in functional programming and type theory
• Functional programming with apomorphisms (corecursion)
• Foundational extensible corecursion: a proof assistant perspective
• Co-induction in relational semantics
• Practical coinduction

Cited in

(16)

• Theories for mechanical proofs of imperative programs
• The generic approximation lemma
• Algorithms and proofs inheritance in the FOC language
• Distributivity of categories of coalgebras
• Interactive verification of architectural design patterns in FACTum
• Procedural representation of CIC proof terms
• Proof relevant corecursive resolution
• Bisimulations generated from corecursive equations
• Aspects preserving properties
• When is a function a fold or an unfold?
• Proof by computation in the Coq system
• Coalgebras in functional programming and type theory
• Recursion schemes in Coq
• Proof methods of declarative properties of definite programs
• Checking equivalence in a non-strict language
• A contextual formalization of structural coinduction

This page was built for publication: Proof methods for corecursive programs

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