Pattern Matches in HOL:

DOI10.1007/978-3-319-22102-1_30zbMath1465.68299OpenAlexW2404704125MaRDI QIDQ2945657

Magnus O. Myreen, Thomas Tuerk, 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)

Uses Software

• Isabelle/HOL
• HOL
• HOL Light
• CakeML

Cites Work

• Unnamed Item
• 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
• A Brief Overview of HOL4
• The Isabelle Framework
• Partial Recursive Functions in Higher-Order Logic
• Purely Functional Data Structures
• CakeML