Graduate Programs      Graduate Home Ph D Programs Masters Degree Ph D Program Requirements Course Descriptions Current Courses Admissions Current Graduate Students Graduate Student Seminar SIAM Chapter Seminar Recent Graduates Incoming Students Graduate Seminar Will Gunther Carnegie Mellon University Title: Lemmas are Unnecessary Abstract: Imagine a game that you play on a pool table without cues. There are $n$ balls on the table, each with some natural number label. You and an adversary alternate turns. On your turn, you remove a ball. Your adversary then places as many balls on the table as they wish, with the condition that each ball they place on the table is labeled with a number less than the ball you removed. You win if you clear the table of balls. Who has a winning strategy? In my talk, I will resolve this question, and use the resolution, typed lambda calculi, and the Curry Howard Isomorphism to prove that lemmas are unnecessary.Date: Thursday, April 25, 2013Time: 5:30 pmLocation: Wean Hall 8220Submitted by:  Brian Kell