I am interested in elegant computational abstractions
that support creative practices. Since I view programming and mathematics
as creative practices, this is a purposefully broad scope, but my prior
work has been situated mainly in the scope of representing and reasoning
about
rule systems. Rule systems 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 inference rules defining programming languages (e.g. in the context
of mechanizing metatheory).
My weapon of choice is the deep relationship between
(constructive) logics and computation, via (1) logic programming
and (2) type systems. This often means extrapolating interesting
logics (e.g. substructural, epistemic, modal) into type systems and logic programming languages.
Polarity and focusing pervade my thinking about type structure and language
design. I believe in the broad potential of dependently-typed languages,
largely because they blur the proof/program distinction.
At Northeastern, I am affiliated with the
Programming Research Laboratory (PRL)
and Games at Northeastern.
- Cynthia Li, Ph.D.
student
- Emma Tosch, Ph.D. (research
scientist, Northeastern University)
- Luis Garcia (Ph.D. student, Northeastern University)
- Chinmaya Dabral (Ph.D. student, NCSU)
- Abhijeet Krishnan
(Ph.D. student, NCSU; co-advised with Arnav
Jhala)
Alumni
Finite-Choice Logic
Programming
Chris Martens, Robert J. Simmons, and Michael Arntzenius.
To appear in
POPL 2025,
Denver, CO, January 2025. (ArXiV
| DOI)
Authoring
Games with Tile Rewrite Rule Behavior Trees
Jiayi Zhou, Chris Martens, and Seth Cooper.
FDG 2024, Worcester, MA, May 2024.
Probabilistic Logic Programming
Semantics For Procedural Content Generation.
Abdelrahman Madkour, Chris Martens, Steven Holtzen, Casper Harteveld and Stacy Marsella.
AIIDE 2023,
Salt Lake City, Utah, October 2023.
Modeling
Game Mechanics with Ceptre.
Chris Martens, Alexander Card, Henry Crain, and Asha Khatri.
In IEEE Transactions on Games, July 2023.
Additional publications
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
|