[PL-sem-jr] Talk tomorrow, Wed 4/14, 11:45

[Vincent St-Amour]

Wed 4/14 Room WVH366 11:45-13:30

Ian - How to Write a Trustworthy Theorem Prover

Have you read the source code for ACL2? I have. It's long. And
confusing. Tags-apropos will only help a little bit. How do we know
it's sound? Well, we /trust/ it's sound because J Moore and Matt
Kaufmann will beat you any day when it comes to being really
smart. That's not good enough for some people. It wasn't good enough
for Jared Davis. In this talk I will discuss the thesis work of Jared
Davis on the first order logic inductive theorem prover, Milawa, and
how it can prove itself sound.

The focus of the talk will be three-fold:
1) How to write a rewriting-based theorem prover.
2) What technology a good theorem prover needs.
3) How to prove that technology sound using a tiny trusted core.

If this sounds like LCF-style proof checkers to you, you're not far
off, but there is a crucial difference that makes this work cool: the
sheer minuteness of trust needed, and the fact that Milawa is first
order. Details in the talk.