About

Shriram Krishnamurthi is a Professor of Computer Science at Brown University whose research vision centers on the essential role of abstractions in computing. He is fascinated by the beauty and complexity of abstractions and is deeply interested in how people can effectively learn them. Since 2016, his work has increasingly incorporated human-factors ideas, cognitive science, and education research into technical work, reflecting a broad view of education that extends beyond traditional teaching to include any tool that produces output as part of the education process. His research spans programming languages and formal methods, computing education, and cognitive engineering, conducted across three groups at Brown University. Krishnamurthi was primarily trained in programming languages but has expanded his expertise to include software engineering, formal methods, human-computer interaction, security, and networking. He has contributed to several innovative software systems such as JavaScript tools, Flowlog, Racket, WeScheme, Margrave, Flapjax, FrTime, Continue, FASTLINK, and (Per)Mission. Currently, his work focuses on projects like Pyret, Forge, the SMoL Tutor, and the LTL Tutor. His research is closely connected to his passion for teaching, particularly in undergraduate courses like the Accelerated Introduction to Computer Science and Programming Languages, where he aims to help students experience the excitement of learning profound and beautiful topics. Beyond Brown, Krishnamurthi is committed to educational outreach and has co-directed the Bootstrap program since 2007, which integrates computing into various disciplines internationally. He has co-authored several freely available books and has been involved in computing outreach since 1995. His professional philosophy emphasizes the interplay between research and teaching, viewing them as mutually informing activities central to his career.

Research topics

• Computer Science
• Psychology
• Mathematics education
• Engineering
• Pedagogy
• Mathematics

Selected publications

• Artifact For: Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages

  Zenodo (CERN European Organization for Nuclear Research) · 2026-04-15

  otherOpen access
  PublisherDOI

• Artifact For: Meaningful Human-in-the-Loop Checking of GenAI Synthesis for Restricted Languages

  Zenodo (CERN European Organization for Nuclear Research) · 2026-04-17

  otherOpen access
  PublisherDOI

• Porpoise: An LLM-Based Sandbox for Novices to Practice Writing Purpose Statements

  2025-10-09

  articleOpen access1st authorCorresponding

  Software developers have long emphasized the need for clear textual descriptions of programs, through documentation and comments. Similarly, curricula often expect students to write purpose statements that articulate in prose what program components are expected to do. Unfortunately, it is difficult to motivate students to do this and to evaluate student work at scale.

  PublisherOA PDFDOI

• A Misconception-Driven Adaptive Tutor for Linear Temporal Logic

  Lecture notes in computer science · 2025-01-01

  book-chapterOpen accessSenior author

  Abstract Linear Temporal Logic (LTL) is used widely in verification, planning, and more. Unfortunately, users often struggle to learn it. To improve their learning, they need drill, instruction, and adaptation to their strengths and weaknesses. Furthermore, this should fit into whatever learning process they are already part of (such as a course). In response, we have built a misconception-based automated tutoring system. It assumes learners have a basic understanding of logic, and focuses on their understanding of LTL operators. Crucially, it takes advantage of multiple years of research (by our team, with collaborators) into misconceptions about LTL amongst both novices and experts. The tutor generates questions using these known learner misconceptions; this enables the tutor to determine which concepts learners are strong and weak on. When learners get a question wrong, they are offered immediate feedback in terms of the concrete error they made. If they consistently demonstrate similar errors, the tool offers them feedback in terms of more general misconceptions, and tailors subsequent question sets to exercise those misconceptions. The tool is hosted for free on-line, is available open source for self-hosting, and offers instructor-friendly features.

  PublisherOA PDFDOI

• Accepted Artifact for Little Tricky Logic: Misconceptions in the Understanding of LTL

  Zenodo (CERN European Organization for Nuclear Research) · 2025-08-06 · 1 citations

  datasetOpen accessSenior author

  Datasets and source materials for our studies of Linear Temporal Logic (LTL). Includes: Labelled responses to our surveys The surveys themselves The coding rubric that guided our categorization

  PublisherDOI

• Sharing Is Scaring: Linking Cloud File-Sharing to Programming Language Semantics

  2025-10-09

  articleOpen access

  Users often struggle with cloud file-sharing applications. Problems appear to arise not only from interface flaws, but also from misunderstanding the underlying semantics of operations like linking, attaching, downloading, and editing. We argue that these difficulties echo long-standing challenges in understanding concepts in programming languages like aliasing, copying, and mutation.

  PublisherOA PDFDOI

• An Interactive Debugger for Rust Trait Errors

  Proceedings of the ACM on Programming Languages · 2025-06-10

  articleOpen accessSenior author

  Compiler diagnostics for type inference failures are notoriously bad, and type classes only make the problem worse. By introducing a complex search process during inference, type classes can lead to wholly inscrutable or useless errors. We describe a system, Argus, for interactively visualizing type class inferences to help programmers debug inference failures, applied specifically to Rust’s trait system. The core insight of Argus is to avoid the traditional model of compiler diagnostics as one-size-fits-all, instead providing the programmer with different views on the search tree corresponding to different debugging goals. Argus carefully uses defaults to improve debugging productivity, including interface design (e.g., not showing full paths of types by default) and heuristics (e.g., sorting obligations based on the expected complexity of fixing them). We evaluated Argus in a user study where N = 25 participants debugged type inference failures in realistic Rust programs, finding that participants using Argus correctly localized 2.2× as many faults and localized 3.3× faster compared to not using Argus.

  PublisherDOI

• Privacy-Respecting Type Error Telemetry at Scale

  The Art Science and Engineering of Programming · 2024-02-15

  articleOpen access

  Context Roblox Studio lets millions of creators build interactive experiences by programming in a variant of Lua called Luau.The creators form a broad group, ranging from novices writing their first script to professional developers; thus, Luau must support a wide audience.As part of its efforts to support all kinds of programmers, Luau includes an optional, gradual type system and goes to great lengths to minimize false positive errors.Inquiry Since Luau is currently being used by many creators, we want to collect data to improve the language and, in particular, the type system.The standard way to collect data is to deploy client-side telemetry; however, we cannot scrape personal data or proprietary information, which means we cannot collect source code fragments, error messages, or even filepaths.The research questions are thus about how to conduct telemetry that is not invasive and obtain insights from it about type errors.Approach We designed and implemented a pseudonymized, randomly-sampling telemetry system for Luau.Telemetry records include a timestamp, a session id, a reason for sending, and a numeric summary of the most recent type analyses.This information lets us study type errors over time without revealing private data.We deployed the system in Roblox Studio during Spring and collected over . million telemetry records from over , sessions.Knowledge We present several findings about Luau, all of which suggest that telemetry is an effective way to study type error pragmatics.One of the less-surprising findings is that opt-in gradual types are unpopular: there is anx gap between the number of untyped Luau sessions and the number of typed ones.One surprise is that the strict mode for type analysis is overly conservative about interactions with data assets.A reassuring finding is that type analysis rarely hits its internal limits on problem size.Grounding Our findings are supported by a dataset of over . million telemetry records.The data and scripts for analyzing it are available in an artifact.Importance Beyond the immediate benefits to Luau, our findings about types and type errors have implications for adoption and ergonomics in other gradual languages such as TypeScript, Elixir, and Typed Racket.Our telemetry design is of broad interest, as it reports on type errors without revealing sensitive information.

  PublisherOA PDFDOI

• Iterative Student Program Planning using Transformer-Driven Feedback

  2024-07-03 · 11 citations

  articleOpen accessSenior author

  Problem planning is a fundamental programming skill, and aids students in decomposing tasks into manageable subtasks. While feedback on plans is beneficial for beginners, providing this in a scalable and timely way is an enormous challenge in large courses.

  PublisherOA PDFDOI

• Forge: A Tool and Language for Teaching Formal Methods

  Proceedings of the ACM on Programming Languages · 2024-04-29 · 7 citations

  articleOpen accessSenior author

  This paper presents the design of Forge , a tool for teaching formal methods gradually. Forge is based on the widely-used Alloy language and analysis tool, but contains numerous improvements based on more than a decade of experience teaching Alloy to students. Although our focus has been on the classroom, many of the ideas in Forge likely also apply to training in industry. Forge offers a progression of languages that improve the learning experience by only gradually increasing in expressive power. Forge supports custom visualization of its outputs, enabling the use of widely-understood domain-specific representations. Finally, Forge provides a variety of testing features to ease the transition from programming to formal modeling. We present the motivation for and design of these aspects of Forge, and then provide a substantial evaluation based on multiple years of classroom use.

  PublisherDOI

Recent grants

• TWC: Small: Extensible Web Browsers and User Privacy

  NSF · $375k · 2012–2015

• SHF: Medium: Collaborative Research: Semantics Engineering for Scripting Languages

  NSF · $472k · 2011–2015

• Exploring Transfer Between Computing and Algebra and Its Effects on Mathematics Pedagogy and Self-efficacy in Computing Teachers

  NSF · $1.5M · 2015–2020

• SHF: Small: Little Tricky Logics: Misconceptions in Understanding Logics and Formal Properties

  NSF · $600k · 2023–2026

• Collaborative Research: Robust Interactive Web Services

  NSF · $147k · 2003–2007

Frequent coauthors

• Kathi Fisler

  Providence College

  143 shared

• Matthias Felleisen

  101 shared

• Robert Bruce Findler

  Northwestern University

  83 shared

• Matthew Flatt

  70 shared

• Joe Gibbs Politz

  University of California, San Diego

  63 shared

• Tim Nelson

  Providence College

  63 shared

• Arjun Guha

  Northeastern University

  55 shared

• Benjamin S. Lerner

  Northeastern University

  34 shared

Labs

• PLTPI

  Programming Languages and Formal Methods

Awards & honors

• SIGPLAN's Robin Milner Young Researcher Award
• SIGSOFT's Influential Educator Award
• SIGPLAN's Software Award
• Brown's Henry Merritt Wriston Fellowship for distinguished c…
• honorary doctorate from the Università della Svizzera Italia…