User loginNavigation 
Milawa: A SelfVerifying Theorem Prover for an ACL2Like LogicMilawa: A SelfVerifying Theorem Prover for an ACL2Like 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 20100529 17:49  DSL  Functional  Implementation  Lambda Calculus  Logic/Declarative  Semantics  other blogs  11669 reads

Browse archivesActive forum topics
New forum topics

Recent comments
7 hours 35 min ago
7 hours 46 min ago
1 day 13 hours ago
6 days 20 hours ago
1 week 1 day ago
2 weeks 5 days ago
3 weeks 4 days ago
4 weeks 4 days ago
6 weeks 2 days ago
6 weeks 5 days ago