Proof-producing translation of higher-order logic into pure and stateful ML

DOI10.1017/S0956796813000282zbMath1297.68053MaRDI QIDQ2875232

Magnus O. Myreen, Scott Owens

Publication date: 14 August 2014

Published in: Journal of Functional Programming (Search for Journal in Brave)

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

Uses Software

• Coq
• ML
• Haskell
• HOL
• HOL Light
• CFML