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

Since 2008, I am a Ph.D. student in the Computer Science Department and Pure and Applied Logic Program at Carnegie Mellon University, studying programming languages. My advisor is Karl Crary.

Research

Broadly, I study proof theory and its relationship with programming. I am particularly interested in logic programming (execution as proof search), substructural logics, and dependent type theory, which so far I have examined primarily in the context of logical frameworks.

Projects:

• A certified compiler for Elf. (Coming soon!)
• Rule-based Interactive Fiction. (Coming soon!)
• Logical analysis of logic programs. (Coming soon!)
• LFinLF. I formalized the metatheory of LF in Twelf: source tarball | talk slides
• 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)

Research blog

Teaching

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

Notes

• 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's what I look like when doing science.

I love games as a medium for interactive storytelling and emergent systems. I highly recommend the games, puzzles, and essays of Zarf.

I read comics and make them myself sometimes.

I climb (boulder) at The Climbing Wall.

I occasionally remember things other people say.

I write other things down elsewhere.