Randall Holmes: Constructing proofs with a dependent type checker

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.

Leave a Reply

Your email address will not be published. Required fields are marked *

Time limit is exhausted. Please reload CAPTCHA.