Proof-producing translation of higher-order logic into pure and stateful ML
type: Item
instance of: scholarly article
title: Proof-producing translation of higher-order logic into pure and stateful ML
zbMATH Open document ID: 1297.68053
DOI: 10.1017/S0956796813000282
author: Magnus O. Myreen
author: Scott Owens
published in: Journal of Functional Programming
publication date: 2014-08-14T00:00:00Z
Mathematics Subject Classification ID: 68N18
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 6330158
describes a project that uses: HOL Light
describes a project that uses: ML
describes a project that uses: HOL
describes a project that uses: CFML
describes a project that uses: Coq
describes a project that uses: Haskell
MaRDI profile type: Publication
cites work: A formally verified compiler back-end
cites work: Verification of the Miller-Rabin probabilistic primality test.
cites work: Proof producing synthesis of arithmetic and cryptographic hardware
cites work: The calculus of constructions
cites work: Adapting functional programs to higher order logic
cites work: Proving Theorems about LISP Functions
cites work: A Thread of HOL Development
full work available at URL: s0956796813000282
OpenAlex ID: W1969704856
description: scientific article; zbMATH DE number 6330158