Gates-Hillman Center 9005
I'm studying programming languages and logic in the Computer Science Department and Pure and Applied Logic Program
at Carnegie Mellon University, advised by Karl Crary and Frank Pfenning.
I believe that formalisms are good not
only for correctness but for expressiveness and creativity.
My thesis project makes use of the formal ideas underlying the logical
framework Celf to specify, test, and reason about systems of play,
In general I am interested in logical frameworks, dependent types,
algebraic/categorical accounts of logic and type theory, interactive
storytelling, interactive fiction, experimental game design,
emergent/simulationist story worlds, functional programming,
and logic programming.
- Chris Martens, Joao F. Ferreira, Anne-Gwenn Bosser, and Marc
Generative Story Worlds as Linear Logic Programs Intelligent
Narrative Technologies 7 (to appear). [pdf, 7
pages; talk slides]
- Chris Martens, Anne-Gwenn Bosser, Joao F. Ferreira, and Marc Cavazza.
Linear Logic Programming for Narrative
Generation 2013 Logic Programming and Nonmonotonic
Reasoning. [pdf, 6 pages]
- Chris Martens and Karl Crary.
LF in LF: Mechanizing the Metatheory of LF in Twelf. 2012
Logical Frameworks and Metalanguages: Theory and Practice.
[pdf, 12 pages
| project repo
| (old) talk slides]
Talks and Workshop Submissions
Unpublished drafts and projects
- Interactive and Reactive Logic Programming: project
- 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
- The Contingent Transition Problem: [pdf]
- Canonical forms-style LF as presented in
Computation and Deduction, Spring 2009: [pdf]
Other things and people
- I attend and speak at conferences, often outside the usual academic
spheres. I document conferences through sketchnotes and travelogues; you
can find some of this work (and, if you feel like, support it
with dollars) on Patreon.
- Here are some interactive fiction experiments I have
- Here are some older comics, including a few travelogues.
- I occasionally make music with
synthesizers, guitars, and vocal chords.
- I occasionally remember things other people say.
- I'm a twit.