Cyrus Omar designs intelligent user interfaces for modern programming languages.

Hazel: Live Functional Programming with Typed Holes

Hazel is a new kind of live programming environment that can reason about and run incomplete programs, i.e. programs with holes of various forms. The following publications develop the semantic foundations for live hole-driven development.

Grove: New Foundations for Collaborative Editing

We are developing a new semantics for collaborative editing that dispenses with diff-and-merge in favor of a commutative structure edit language. This resolves a number of problems, particularly related to relocation conflicts, and opens up new design avenues for a computational commons.

Tylr: Eliminating Parse Errors with Holes

Parse errors are a pain for beginners and experts alike. The Tylr project eliminates parse errors (!) by automatically tracking syntactic obligations and materializing them as holes and other affordances. This benefits both humans and downstream tooling.

ChatLSP: Semantically Contextualizing AI Programming Assistants

We are integrating modern language implementations (i.e. language servers) with modern AI coding assistants. We are finding dramatic performance improvements when AI models are properly contextualized by programming language semantics (e.g. types, live run-time information, and structured/destructured task contexts)!

Livelits: Filling Typed Holes with Live GUIs

We are working on integrating graphical and programmatic modes of interaction by developing language mechanisms that allow you to define type-specific user interfaces that generate code underneath, i.e. they serve as interactive graphical literal notation.

Hazel Tutor: Semantically Grounded Educational Technology

We are developing educational technology, including classroom proof assistants, grounded in the semantic foundations of typed hole-driven development.

RustViz: Interactively Visualizing Ownership and Borrowing

The Rust programming language achieves memory and thread safety using a static ownership and borrowing analysis. This has led to explosive adoption, but learning Rust remains challenging. We are developing RustViz, a system that makes learning Rust easier by visualizing the invisible static state changes that occur within Rust code.

Read our RustViz-based quick introduction to Rust!

RustViz, which is developed by an all-undergraduate team, reached 2700+ stars on GitHub!

Bastion: Capability Safety for AI Safety

We argue for concise formal architectural policy descriptions which are responsible for specifying constraints and passing a minimal set of capabilities to downstream system component and AI agents working within these components. By constructing the operating system for AI agents atop a capability safe programming language, we will be able to provide formally provable bounds on AI capabilities, addressing a major problem in governing agentic AIs.

Relit: Reasonably Programmable Literal Notation

My thesis research developed mechanisms that allow library providers to express new type-specific literal notation (e.g. SQL literals) while ensuring that client programmers can still reason abstractly and compositionally about types and binding.

Relit implements the mechanism from the ICFP 2018 paper into Reason, which is Facebook's new front-end for OCaml. The Wyvern programming language implements the mechanism from the ECOOP 2014 paper.

There has been a great deal of excitement around both Relit [1, 2, 3, 4, 5] and Wyvern [1, 2, 3, 4, 5]!

typy: Programmable Semantic Fragments

typy allows library providers to install new statically typed semantic fragments into Python, while leaving its syntax alone (which cleverly sidesteps the "expression problem"). We have applied typy to problems in web security and data science.

SciUnit: Collaborative Infrastructure for Test-Driven Scientific Model Validation

One of the pillars of the scientific method is model validation: comparing a scientific model’s predictions against empirical data. The SciUnit project casts this as a form of collaborative software testing and develops useful infrastructure.

Neurobiological Circuit Dynamics

I entered grad school as a computational neurobiologist. I was interested in how biological circuits process information, so I developed a model of how the excitatory-inhibitory circuitry in the rodent whisker barrel cortex responds to stimulation.

Information Theoretic Foundations for Brain-Computer Interfaces

We built a provably optimal EEG-based brain-computer interface by studying the information theoretic properties of noisy asymmetric channels and developing statistical models of user intent for various types of communication/control tasks.