Proof-producing synthesis of ML from higher-order logic

DOI10.1145/2364527.2364545zbMath1291.68364OpenAlexW2014904806MaRDI QIDQ5168887

Scott Owens, Magnus O. Myreen

Publication date: 21 July 2014

Published in: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2364527.2364545

zbMATH Keywords

theorem proving

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (2)

Extensible Extraction of Efficient Imperative Programs with Foreign Functions, Manually Managed Memory, and Proofs ⋮ Verification and code generation for invariant diagrams in Isabelle

Uses Software

• Coq
• ML
• Haskell
• HOL
• PLT Redex
• Milawa
• CFML

This page was built for publication: Proof-producing synthesis of ML from higher-order logic