<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><div style="font-family: Avenir-Book;">This is a reminder of Benjamin Waldman's MS Presentation</div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;">===============================================</div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;">Candidate: Benjamin Waldman</div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;">Date: Tuesday, May 6, 2025</div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;">Time: 3:00 pm CT</div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;">Location: JCL 390</div><div style="font-family: Avenir-Book;"><br></div><div><span style="font-family: Avenir-Book;">Title: </span><font color="#000000" face="Avenir-Book">PROVING ARROW’S IMPOSSIBILITY THEOREM USING REFINEMENT TYPES</font></div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;">Abstract: Arrow’s impossibility theorem is a landmark result in theoretical economics that led to the</div><div style="font-family: Avenir-Book;">formation of modern social choice theory. I develop a new, computer-verified proof of Arrow’s</div><div style="font-family: Avenir-Book;">impossibility using refinement types, a concept from type theory that allows functions to</div><div style="font-family: Avenir-Book;">return both data and predicates on that data. I then argue that refinement types are a</div><div style="font-family: Avenir-Book;">natural paradigm for formally verifying many theorems in economics and political science.</div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;"><font color="#000000">Advisors: Stuart Kurtz</font></div><div style="font-family: Avenir-Book;"><br></div><div style="font-family: Avenir-Book;">Committee Members: Stuart Kurtz, Adam Shaw, and Robert Rand</div></div><br class="Apple-interchange-newline" style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><div dir="auto" style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"><div dir="auto" style="overflow-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;"></div></div></div></div></body></html>