Chris Martens, Ph.D.
CV as of December 2015
I got my Ph.D. with the Principles of
Programming group in the Computer Science Department
at Carnegie Mellon University, advised by Karl Crary and Frank Pfenning. I graduated in
September 2015 with my thesis Programming
Interactive Worlds with Linear Logic. As of December 2015, I'm doing a postdoc
with the Expressive Intelligence
Studio at UC Santa Cruz!
I am looking for tenure-track faculty positions to start Fall 2017.
Please get in touch if your department is hiring in Programming
Languages, Formal Methods, or Interactive Media!
I investigate how to use mathematical tools, such
as proof theory, to better understand and create interactive
rule systems. I place an emphasis on games and
computational creativity, but I am broadly interested in modeling
computational and scientific systems by way of logical rules. My prior
experience spans logical frameworks, dependent types, algebraic/categorical
methods, functional programming, logic
programming, generative methods, interactive fiction authoring,
experimental game design, AI for social simulation, and emergent
My thesis project is a programming language for the design of
interactive narratives and game
mechanics. The language is based on forward-chaining linear logic
programming, a way of declaratively describing state change. This
methodology makes it feasible to encode generative rules that create
procedural content for interactive simulations that give rise to emergent
The language semantics' basis in proof theory enables a structural
understanding of these narratives, making it possible to analyze them for
concurrent behavior among multiple agents. On a larger timescale, I
imagine growing the technology underlying this language into a high-level
sketching tool for game designers, usable for rapid prototyping and
Thesis page | Project
| Patreon to support
- Chris Martens.
"Ceptre: A Language for Modeling Generative
In proceedings of Artificial Intelligence and Interactive
Digital Entertainment 2015.
[pdf, 7 pages]
- Chris Martens, Joao F. Ferreira, Anne-Gwenn Bosser, and Marc
"Generative Story Worlds as Linear Logic Programs."
Intelligent Narrative Technologies 7, 2014.
[pdf, 7 pages; talk slides (html)]
- Chris Martens, Anne-Gwenn Bosser, Joao F. Ferreira, and Marc
"Linear Logic Programming for Narrative
In proceedings of Logic Programming and Nonmonotonic
[pdf, 6 pages]
- Chris Martens and Karl Crary.
"LF in LF: Mechanizing the Metatheory of LF in Twelf."
Logical Frameworks and Metalanguages: Theory and Practice, 2012.
[pdf, 12 pages
| project repo
| talk slides]
- Charles Cusack, Chris Martens, and Priyanshu Mutreja.
"Volunteer Computing Using Casual Games."
In proceedings of Future Play International Conference on the Future
of Game Design and Technology, 2006.
- Ulas Bardak, Eugene Fink, Chris R Martens, Jamie Carbonell.
"Scheduling with Uncertain Resources Part 3: Elicitation of Additional
In Proceedings of the IEEE International Conference on Systems, Man,
and Cybernetics, 2006.
Talks and Workshop Submissions
- Invited Talk: "Proofs as Stories," delivered at the UConn Logic
Seminar, October 16, 2015. Slides!
- Invited Talk: "Ceptre: A Language for Modeling Interactive
Worlds." Future Programming Workshop at Strange Loop 2015.
***** Watch the
- "Proof-Theoretic Study of Game Mechanics," delivered at the
Foundations of Digital Games (FDG) Doctoral Consortium:
3-page PDF; slides
- "Creating and Analyzing Playable Narratives with Linear Logic,"
delivered at the CMU Graphics Lab Seminar, April 2015. Slides!
- "Modularity & Abstraction in Functional Programming," delivered at
Compose Conference 2015:
Watch the video!
- "Linear Logic Programming," delivered at Strange Loop 2013.
- "Systems of Play as Linear Logic Programs," delivered at NJPLS May 2014.
- "Languages for Computational Creativity," delivered at OBT 2014:
talk (html, Twine) |
abstract (2pg pdf)
- "Rule-based Interactive Fiction," delivered at OBT 2012:
talk slides |
Unpublished drafts and projects
- Linear Logic Programming for Narrative Generation: long version (draft)
- Logical analysis of logic programs, at INRIA Parsifal:
- Type inference for a nested configuration language. (Google
internship; not yet open-sourced.)
- Banyan, a
distributed computation framework for recursive programs. For 15-712
Advanced & Distributed Operating Systems.
- Ordered Hybrid LF.
As an undergraduate, I was advised by Frank
Pfenning and Jason Reed on a senior
thesis extending Hybrid LF
to the case of ordered logic. pdf, 28 pages
Notes and Other Writing