Chris Martens

Associate Professor
Khoury College of Computer Sciences
College of Arts, Media, and Design
Northeastern University

Ph.D. in Computer Science
Carnegie Mellon University

Email: c.martens at northeastern.edu
Office: Meserve 138 (Boston campus)
Pronouns: they/them

Research Interests

My work is about both human and computational interpretations of logical reasoning, and the cool things that can happen where they overlap. I'm interested in interpretations of logics as expressive type systems for programming languages and proof assistants, as well as settings for proof search in the context of interactive reasoning tools and automatic generation of data that adheres to constraints. Much of my past work involves language design and authoring tools that support specific creative and cognitive practices, such as analyzing and generating narrative structures, prototyping interactive simulations, and reasoning about the implications of privacy policies. Another theme is representing and reasoning about rule systems, which show up in my work via games (rules as game mechanics), privacy policies (rules as governance documents), procedural design and data generation (rules as constraints and search directives), and programming language specification (rules as in inference rules).

Lately, I am interested in mathematics and programming as creative activities in their own right. My weapon of choice is the deep relationship between (constructive) logics and computation, via (1) logic programming (via sequent calculus) and (2) type systems (via natural deduction). I am especially interested in relationships between these interpretations, and the potential uses of those relationships in contexts such as interactive proof, iterative specification/hypothesis refinement, and exploration of possibility spaces.

At Northeastern, I am affiliated with the Programming Research Laboratory (PRL) and Games at Northeastern.

Teaching

Professional Activities

  • Program Committee, POPL 2025
  • Invited speaker, TYPES 2025: "A guided tour of polarity and focusing"
  • Review Committee, OOPSLA 2025
  • Organizer, NEPLS at Northeastern, September 2024

Students and Collaborators

Alumni

Working Drafts

Featured Publications

Is truth future-proof? On the possible futures of mechanized proofs.
Chris Martens, Emma Tosch, Elan Semenova, and Cynthia Li.
PLATEAU 2026, Pittsburgh, PA. (talk slides | DOI)

Substructural Parametricity.
C. B. Aberlé, Karl Crary, Chris Martens, and Frank Pfenning.1
FSCD 2025. (DOI | ArXiv preprint).

1 Authors listed alphabetically.

Finite-Choice Logic Programming.
Chris Martens, Robert J. Simmons, and Michael Arntzenius.
POPL 2025, Denver, CO, January 2025. (ArXiV | DOI)

Modeling Game Mechanics with Ceptre.
Chris Martens, Alexander Card, Henry Crain, and Asha Khatri.
In IEEE Transactions on Games, July 2023.

Additional publications

Funded Projects

Explorable Formal Models of Privacy Policies and Regulations.
Funding source: NSF CAREER Award (2019-2024)
People: Emma Tosch, Luis Garcia, Chinmaya Dabral
Aims: We are developing techniques to represent privacy policies and regulations that are both formal and explorable, permitting users and policy crafters to answer 'what if'? questions about specific scenarios in addition to providing provable guarantees. We are formalizing privacy documents and scenarios using a relational programming model known as Answer Set Programming (ASP) as a lightweight semantic modeling framework, in which we have build a narrative planner that generates partial-ordered event structures from agent intentions and capabilities. We are augmenting ASP and narrative planning with support for answering queries, generating scenarios that reveal privacy loopholes, generating counterexamples to global correctness conditions, suggesting repairs for broken policies, and enabling the exploration of hypothetical scenarios by policy developers and users.

Formal Methods in Software Support for Sound Experimentation.
Funding source: NSF FMITF (2022-2026)
People: Emma Tosch (PI) (My role: co-PI)
Aims: This project will produce a high-level domain-specific language (DSL) for experimentation that enforces constraints on hypotheses, analyses, and treatment assignment according to the underlying principles of experimental design. Experiments written in this language will be correct by construction vis a vis consistency of hypotheses and treatment assignments with respect to their identifiable effects. The team will then integrate the experimentation DSL into legacy socio-technical software for education, leveraging existing support for gradual typing to implement an orthogonal type system for experimental interventions. To evaluate these tools and promote continued research around formal methods approaches to the experimentation-analysis pipeline, the team will build a publicly available searchable experiment repository.

Past projects

Notes, Slides, and Drafts

Recorded Talks

Elsewhere