Increasingly, being a functioning member of society requires systems literacy: an operational understanding of things like online security and privacy, conversations with virtual assistants, recommendation engines, and automated vehicles. For both users and authors of these systems, we need more tools to develop this literacy and communicate system designs more clearly. Digital games have great potential for teaching systems literacy, and formal specification techniques provide a good platform for specifying systems unambiguously. By providing language-based abstractions for both specifying and running interactive systems, we can run our theories as programs and perform both experimentation and analysis over the same formal artifact.

In this talk, I introduce the Ceptre logic programming language, which is based on forward-chaining linear logic, as an example of a system for writing these executable specifications, especially in the domains of game mechanics and interactive storytelling. I will then discuss a design space for generative methods using logic- and language-based abstractions and describe plans for future research to explore that space.

Chris Martens is a postdoctoral researcher at UC Santa Cruz, working on generative methods for game design in the Expressive Intelligence Studio. Previously, she got her Ph.D. in the Principles of Programming group at Carnegie Mellon University, where she developed a modeling language called Ceptre, which can be used for interactive simulations, game mechanic prototyping, and narrative generation.