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

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

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)

Cites Work

• The Isabelle Framework
• A Brief Overview of HOL4
• Proof-producing translation of higher-order logic into pure and stateful ML
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• HOL Light: An Overview
• CakeML
• Partial Recursive Functions in Higher-Order Logic
• Purely Functional Data Structures
• Title not available (Why is that?)

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)