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.
In Spring 2014 I am teaching StuCo:
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.
- 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
- The Contingent Transition Problem: [pdf]
- Canonical forms-style LF as presented in
Computation and Deduction, Spring 2009: [pdf]
Other things and people