2011 Poster Sessions : A Theorem Compiler

Student Name : Pokey Rule
Advisor : David Cheriton
Research Areas: Computer Systems
A key difficulty in understanding and applying general mathematical theorems is the abstract manner in which they are specified. Such abstraction is critical to the
generality of a particular theorem, but to learn the theorem, we must see special cases, and to apply it, we must translate the theorem to a particular application
domain. However, the process of restating the theorem in various special cases is tedious, error-prone, and results in duplicate specifications that need to be
maintained. To address this problem, we present a library for representing abstract mathematical theorems on a computer, along with a compiler that generates natural language statements of these theorems in their various application domains. The benefits of our high level representation over human languages parallels the
benefits of high level computer languages: we gain portability, because the same theorem representation can be used across languages and application domains,
extensibility, in that adding a new language module automatically allows all theorems to be generated in the given language, and maintainability, by avoiding a
proliferation of statements of the same theorem in different languages and application domains.

Pokey Rule is a Ph.D. student in Stanford's Distributed Systems Group. His research interests include programming language theory and distributed systems. He has been involved with several start-up companies, including OptumSoft, Acuitus, and Through
The Lens. He received his Bachelor's Degree in Computer Science from Stanford University.