Chris Martens Ph.D. candidate Gates-Hillman Center 9005 (412) 268-5940 cmar...@cs.cmu.edu

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.

Research

Currently I am interested in formalizing reactive and interactive media. My tools of choice are proof theory and type theory, specifically as they pertain to logic programming, logical frameworks and specification languages. I believe that formalisms are good not only for correctness but for expressiveness and creativity.

Research blog

Projects:

• Linear Logic Programming for Narrative Generation: paper draft
• Interactive and Reactive Logic Programming: project repo
• LFinLF, aka the formalized metatheory of LF in Twelf. Presented at LFMTP'12: paper | project repo | (old) talk slides
• Rule-based Interactive Fiction, presented at OBT'12: talk slides | talk abstract
• Logical analysis of logic programs, at INRIA Parsifal: internship report
• 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. document (ps)

Publications

• Chris Martens and Karl Crary. LF in LF: Mechanizing the Metatheory of LF in Twelf. 2012 Logical Frameworks and Metalanguages: Theory and Practice. [pdf]

Teaching

• In Fall 2011 I TAed 15-210 Parallel and Sequential Data Structures and Algorithms.
• In Fall 2010 TAed 15-317 Constructive Logic.

Notes

• The Contingent Transition Problem: [pdf]
• Canonical forms-style LF as presented in Computation and Deduction, Spring 2009: [pdf]

Other things and people

• ConCert Reading Group, a weekly student-run PL-oriented reading group.
• The Principles of Programming group.

Not Research

• Here are some interactive fiction experiments I have made.
• Comics
• Music
• I occasionally remember things other people say.
• I'm a twit.