[PL-sem-jr] Talk tomorrow, Mon 2/8

[Vincent St-Amour]

Mon 2/8 Room WVH166 10:00-12:00

Vasilis - Theorem Proving with ACL2

ACL2 is both a programming language in which you can model computer
systems and a mechanical theorem prover to help you reason about
their properties.  This seminar session will be a hands-on
introduction to theorem proving with ACL2. We will state formal
theorems about list processing and go through the process of proving
them.