π Congratulations to Nicholas Coltharp for passing his Research Proficiency Exam!
Portland State University
Programming Languages & Verification
Welcome to the Portland PLV Group! We are a research group focused on Programming Languages and Verification.
Our research spans type systems, functional programming, formal methods, interactive theorem proving, program analysis, and security. We work on both theoretical foundations and practical applications, contributing to the advancement of programming languages and software verification techniques.
News
-
-
π Nicholas Coltharp and Yao Li’s paper Unifying Hindsight and Foresight: Lazy Cost Analysis as Functional Logic Programming was accepted to FLOPS 2026. This is a joint work with Steven Libby and Laura Israel.
-
π Yao Li’s paper SymCode: A Neurosymbolic Approach to Mathematical Reasoning via Verifiable Code Generation was accepted to Findings of EACL 2026. This is a joint work with Sina Bagheri Nezhad and Ameeta Agrawal.
More info -
π Yao Li’s paper The Memorist Tale: Every Thunk Every Cost All At Once was accepted to ESOP 2026. This is a joint work with Xing Li, Peter Schachte, and Christine Rizkallah.
-
π Congratulations to Grant VanDomelen for passing his Research Proficiency Exam!
-
π Congratulations to Yiming Lin for passing his Research Proficiency Exam!
-
π€ Grant VanDomelen gave a talk at the Haskell Symposium 2025 on Freer Arrows and Why You Need Them in Haskell.
More info -
π Congratulations to Ian Kariniemi for passing his Research Proficiency Exam!
-
π Yao Li’s paper A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants was accepted to the LMPL 2025 workshop. This is a joint work with BarΔ±Ε BayazΔ±t and Xujie Si.
More info -
π Ian Kariniemi has been awarded the Bloomberg Infrastructure & Security Fellowship. He is among the 4 students who received this award this year. Congratulations Ian!
Faculty
-
James Hook
Professor
- Research Areas
- Abstraction Carrying Code, Computer Science for Oregon, High-Assurance Systems Programming (HASP), Programatica, Relativistic Programming (RP)
-
Mark P. Jones
Professor
- Research Areas
- Functional Programming, Language Implementation, Low-level Systems Programming, Programming Languages
-
Jingke Li
Associate Professor
- Research Areas
- Compilers, Parallel Computation, Programming Languages
-
Yao Li
Assistant Professor
- Research Areas
- Formal Verification, Functional Programming, Interactive Theorem Proving, LLMs for Verification
-
Bart Massey
Associate Professor
- Research Areas
- Functional Programming, Open Source Software Development, Programming Languages, Software Engineering
-
Andrew Tolmach
Professor
- Research Areas
- Compilers, Formal Verification, Functional Programming, Interactive Theorem Proving, Runtime Verification, Security
-
Fei Xie
Professor
- Research Areas
- Embedded Systems, Formal Methods, Software Engineering
Current Students
-
Allison Naaktgeboren
Ph.D. Candidate
Advisor: Andrew Tolmach
- Research Areas
- Security
-
KC
Katie Casamento
Ph.D. Student
Advisor: Andrew Tolmach
- Research Areas
- Functional Programming, Type Systems
-
Nicholas Coltharp
Ph.D. Student
Advisor: Yao Li
- Research Areas
- Formal Verification, Functional Programming
-
Ian Kariniemi
Ph.D. Student
Advisor: Yao Li
- Research Areas
- Formal Verification
-
YL
Yiming Lin
Ph.D. Student
Advisor: Yao Li
- Research Areas
- Formal Verification
-
KP
Katherine Philip
Ph.D. Student
Advisor: Mark P. Jones
- Research Areas
- Functional Programming, Type Systems
-
GV
Grant VanDomelen
Ph.D. Student
Advisor: Yao Li
- Research Areas
- Formal Verification, Functional Programming
-
Julay Leatherman-Brooks
Master's Student
Advisor: Andrew Tolmach
- Research Areas
- Formal Verification, Security
Affiliated Faculty
-
Andrew Black
Professor Emeritus
Portland State University
-
Steven Libby
Assistant Professor
University of Portland
-
Marly Roncken
Research Professor
Director of Asynchronous Research Center
Portland State University
Alumni
-
Laura Israel
website- Advisor
- Yao Li
- Graduated
- Degree
- MSc
- Current Position
- Ph.D. Student at University of Konstanz
- Research Areas
- Formal Verification, Privacy
-
Sean Noble Anderson
Thesis: Tag-based Security in C: Writing and Specifying Flexible Protection
- Advisor
- Andrew Tolmach
- Graduated
- Degree
- Ph.D.
- Research Areas
- Formal Verification, Runtime Verification, Security