SHF: Small: Game Logic Programming

The project develops a new programming language based on the mathematical idea of a two-player game. The project's impacts are that it provides a powerful new tool for modeling interactive systems in challenging adversarial environments and also helps productively write code that remains correct in worst-case environments. The investigator especially focuses on the impacts of this new tool in security applications, such as mathematical games where one agent pursues another. The project's novelties are that it improves our ability to model code and data as separate, yet interacting things, and that, for the first time, it transforms a yet-unexploited logical tradition into a practical programming language, called dynamic logics and game logics. The technical approach combines two well-established ideas: the paradigm of logic programming and a family of formal logics called game logics. Logic programming is a style of programming where programs are made up of formal logical rules and running a program is equivalent to searching for proofs. Game logic is a family of modal logics where every modal operator defines a model of a zero-sum game between two players. This project builds on the investigator's development of a theoretical connection between game logic proofs and computation, transforming it into a practical connection. This transformation will build upon prior literature on both automated analysis of dynamic logic formulas and on other rich logic programming languages such as answer-set programming languages. The impact is to provide a concise, expressive language for modeling interactive systems, software included, with adversarial environments. Because game proofs correspond to winning strategies, a major impact will be the blurring of lines between proof search and program synthesis, providing an elegant mechanism for automatically searching for the winning strategies of the programmer's game models. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.