-
Notifications
You must be signed in to change notification settings - Fork 140
/
README
27 lines (19 loc) · 1.06 KB
/
README
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
This directory contains a soundness proof of Jared Davis' Milawa
theorem prover. Milawa is a theorem prover styled after systems such
as Nqthm and ACL2, but differs from these in that it has a small
logical kernel and support for reflection. Its main proof checker can
at runtime be swapped for a different user-supplied proof checker.
Two subdirectories:
lisp-runtime
-- constructs and proves the correctness of a Lisp runtime which is
able to run through Milawa's lengthy bootstrapping process.
(This involves processing a 4-gigabyte input.)
milawa-prover
-- formalises the logic Milawa uses, proves the logic sound and
proves that Jared Davis' Milawa implementation is sound when run
on top of the lisp runtime mentioned above.
The top-level result is in milawa-prover/soundness-thm where a theorem
states: when Milawa is run on top of the verified runtime it will only
ever prove statements that are true w.r.t. the semantics of Milawa's
formulas -- no matter how reflection or any other feature is used.
Copyright Magnus O. Myreen 2012