Output details
11 - Computer Science and Informatics
University of Cambridge
Article title
A verified runtime for a verified theorem prover
Type
D - Journal article
Title of journal
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Article number
-
Volume number
6898 LNCS
Issue number
-
First page of article
265
ISSN of journal
0302-9743
Year of publication
2011
URL
-
Number of additional authors
1
Additional information
<07> In a recent EU research proposal "Proof Assistants: the Next
Generation (PANG)", Prof. Geuvers of Radboud University Nijmegen
referred to this paper when writing "Proof assistants have already
been used for highly non-trivial proofs [...]. For example, [...], the
self-verified proof assistant Milawa by Jared Davis running on top of
a Lisp implementation verified using HOL4 by Magnus Myreen." This
paper managed to make formal verification techniques for full
functional correctness scale better than people expected and is, as a
result, used as an example that the next generation of proof assistants
should learn from.
Interdisciplinary
-
Cross-referral requested
-
Research group
None
Citation count
4
Proposed double-weighted
No
Double-weighted statement
-
Reserve for a double-weighted output
No
Non-English
No
English abstract
-
