Toward Gamification of Proofs about Programs | Sorin Lerner | Design@Large

Описание: ABSTRACT:

Toward Gamification of Proofs about Programs

In this talk, I will present our ongoing research on turning the task of doing proofs about programs into puzzle games that can played for fun. I will first present Polymorphic Blocks, a block-based UI in which a connector’s shape visually represents the structure of the data being passed through the connector. I will show how this UI can be used to add visual type information to block-based languages like Blockly, but more importantly, how it can be used to represent logical proofs in natural deduction. In this context, if we erase all the symbols, our UI becomes a visual puzzle game, where solving a puzzle is tantamount to building a proof in natural deduction. Using this gamification of natural deduction as a springboard, I will go on to discuss (1) implications of this result for doing proofs about programs (2) our follow up work on gamification of loop invariants, and finally (3) lessons learned from this project.

BIO:

Sorin Lerner is a Professor and Vice-Chair in the Department of Computer Science and Engineering at the University of California, San Diego. He received his Bachelors degree in Computer Engineering from McGill University in 1999 and his PhD from the University of Washington in 2006. His research interests lie in programming language and analysis techniques for making software more reliable and more secure. Recent projects include the Quark formally verified browser, the VeriDrone framework for foundational verification of cyber-physical systems, and a new project on gamification of proofs about programs. Professor Lerner has graduated 8 PhD students, including Zachary Tatlock, now assistant professor at the University of Washington, and Ross Tate, now assistant professor at Cornell. Professor Lerner is the recipient of an NSF Career Award (2007), and the 2003 PLDI Best paper award.