You are in : Home » Results & submissions » Select UOA » 11 - Computer Science and Informatics » View submission: University of Cambridge » Outputs » Detail

Output details

11 - Computer Science and Informatics

Return to search Previous output Next output

Output 0 of 0 in the submission

Output title

Proof-producing synthesis of ML from higher-order logic.

Type

E - Conference contribution

DOI

Name of conference/published proceedings

ICFP

Volume number

Issue number

First page of article

115

ISSN of proceedings

Year of publication

2012

URL

Number of additional authors

Additional information

<07> Recent verification projects such as CompCert (POPL 2006) have caught people's imagination. In these, algorithms are verified in a proof

assistant, then printed into the syntax of a real programming

language and finally run. People within the proof assistant community

have been sceptical about this printing which the highly regarded Dr

John Harrison (author of one of the leading proof assistants, HOL

light) describes as a "glaring leap of faith" in a report from SRI

Cambridge, 1995. This paper shows how this "glaring leap of faith"

can be avoided using automation that proves the correctness of the

printing step.

Interdisciplinary

Cross-referral requested

Research group

None

Citation count

Proposed double-weighted

Double-weighted statement

Reserve for a double-weighted output

Non-English

English abstract