Trusted Source Translation of a Total Function Language

DOI10.1007/978-3-540-78800-3_37MaRDI QIDQ5458345zbMATH OpenOpenAlexFDO

Authors Guodong Li, Konrad Slind

Publication date 11 April 2008

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-78800-3_37

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Recommendations

• A verified compiler from Isabelle/HOL to CakeML
• Automatically Translating Type and Function Definitions from HOL to ACL2
• Proof-producing translation of higher-order logic into pure and stateful ML
• Proof-producing synthesis of ML from higher-order logic
• Compilation as Rewriting in Higher Order Logic

Cited in

(3)

• Automatically Translating Type and Function Definitions from HOL to ACL2
• Trusted Translation Services
• Types for Proofs and Programs

Describes a project that uses

Uses Software

• HOL
• Isabelle/HOL

This page was built for publication: Trusted Source Translation of a Total Function Language

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