[pl-seminar] Any interest in automated theorem proving and Coq talks?

[mulhern <mulhern@xxxxxxxxxxx>]

Hi!

Would anybody be interested if I were to give one or several talks about automated theorem proving, automated theorem proving in Coq, and if interest holds for that long mechanizing metatheory in Coq? The talks would include frequent hands-on activity by the attendees. Chalk and the chalkboard would be used in preference to slides and overheads. The material in the talks would be cumulative.

If there is sufficient interest I would be happy to schedule one talk and if that experience doesn't turn everybody off several more.

The first few talks should be accessible to someone with a basic knowledge of ML, a passing acquaintance with Peano arithmetic, a notion of type-checking and type inference, and a passing acquaintance with dependent types.

Tentative titles for the first few talks:

Introduction

Proof by Induction

Proof by Evaluation

Proof by Reflection

Tacticals

-mulhern

P.S. I'm sorry if you receive multiple postings---I posted to this list via my gmail account before I remembered that I'm subscribed via my cs account.