<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><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">This is a reminder of Benjamin Waldman's MS Presentation</div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">===============================================</div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Candidate: Benjamin Waldman</div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Date: Tuesday, May 6, 2025</div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Time: 3:00 pm CT</div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Location: JCL 390</div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div><span style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Title: </span><font color="#000000" face="Avenir-Book"><span style="caret-color: rgb(0, 0, 0);">PROVING ARROW’S IMPOSSIBILITY THEOREM USING REFINEMENT TYPES</span></font></div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book;"><span style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Abstract: </span>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; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book;"><font color="#000000">Advisors: Stuart Kurtz</font></div><div style="font-family: Avenir-Book; caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);"><br></div><div style="font-family: Avenir-Book;"><span style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Committee Members: </span><span style="caret-color: rgb(0, 0, 0); color: rgb(0, 0, 0);">Stuart Kurtz, </span><span style="color: rgb(0, 0, 0);">Adam Shaw, and Robert Rand</span></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>