Stream Fusion for Isabelle’s Code Generator

DOI10.1007/978-3-319-22102-1_18MaRDI QIDQ2945639zbMATH OpenOpenAlexFDO

Authors Alexandra Maximova, Andreas Lochbihler

Publication date 14 September 2015

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-22102-1_18

Mathematics Subject Classification ID

Data structures (68P05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Rough diamond: an extension of equivalence-based rewriting
• Verification and code generation for invariant diagrams in Isabelle
• Combinators for program generation
• Imperative streams—a monadic combinator library for synchronous programming
• An embedding of Ruby in Isabelle
• Programming with streams in Coq a case study: The Sieve of Eratosthenes
• Towards an algebraic specification of code generation
• scientific article; zbMATH DE number 970725

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• CeTA
• Stream Fusion
• Stream Fusion Code

This page was built for publication: Stream Fusion for Isabelle’s Code Generator

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