Tuesday, October 25 from 3 to 4pm
Room: MB 124
Speaker: Randall Holmes (BSU)
Title: Constructing proofs with a dependent type checker
Abstract: I’ll discuss my latest theorem proving work, and present examples. I’ll explain what dependent type theory is and how a type checker for a dependent type theory can be a theorem prover. The talk should be accessible to students.