Pattern matches in HOL: a new representation and improved code generation

DOI10.1007/978-3-319-22102-1_30zbMATH Open1465.68299OpenAlexW2404704125MaRDI QIDQ2945657FDOQ2945657

Authors Thomas Tuerk, Magnus O. Myreen, Ramana Kumar

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_30

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 2185700
• A new look at pattern matching in abstract data types
• A verified compiler from Isabelle/HOL to CakeML
• Pattern minimization problems over recursive data types
• Code generation via higher-order rewrite systems

Cites work

• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• A Brief Overview of HOL4
• CakeML
• HOL Light: An Overview
• HOL with definitions: semantics, soundness, and a verified implementation
• Partial Recursive Functions in Higher-Order Logic
• Proof-producing translation of higher-order logic into pure and stateful ML
• Purely Functional Data Structures
• The Isabelle Framework

Describes a project that uses

Uses Software

• Isabelle/HOL
• HOL
• HOL Light
• CakeML

This page was built for publication: Pattern matches in HOL: a new representation and improved code generation

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