User loginNavigation |
Milawa: A Self-Verifying Theorem Prover for an ACL2-Like LogicMilawa: A Self-Verifying Theorem Prover for an ACL2-Like Logic
This might help inform discussions of the relationship between the de Bruijn criterion (the "social process" of mathematics) and formal verification. I think it also serves as an interesting signpost on the road forward: it's one thing to say that starting with a de Bruijn core and evolving a more powerful prover is possible in principle; it's another thing for it to actually have been done. The author's thesis defense slides provide a nice, quick overview. By Paul Snively at 2010-05-29 17:49 | DSL | Functional | Implementation | Lambda Calculus | Logic/Declarative | Semantics | other blogs | 14111 reads
|
Browse archives
Active forum topics |
Recent comments
17 weeks 11 hours ago
17 weeks 11 hours ago
17 weeks 11 hours ago
23 weeks 21 hours ago
1 year 11 weeks ago
1 year 11 weeks ago
1 year 11 weeks ago
1 year 33 weeks ago
1 year 37 weeks ago
1 year 39 weeks ago