Trustworthy Human-AI Collaboration in a Live Type-Theoretic Computational Commons
Assistant Professor of Computer Science
This talk presents a vision for a live type-theoretic computational commons, detailing foundational work on incremental type checking, evaluation with typed holes, and an object-capability architecture for bounding AI agent behavior based on the principle of least authority.
Rooted in Cyrus Omar's group's work on the Hazel live programming environment, this talk presents a vision for a "live type-theoretic computational commons": a shared monorepo where humans and swarms of AI agents make verifiable progress on parallel coding tasks. The collaboration model combines novel editing primitives (e.g. CRDT-based structure editing and Unison-style versioning) with familiar type-theoretic structure (e.g. OCaml-style modules and interfaces, Isabelle-style proofs).
Two research problems take center stage. First, large-scale collaboration requires that incomplete programs remain continuously analyzable and executable — Cyrus will present recent foundational work on live, incremental type checking and evaluation of programs with typed holes. Second, as agent swarms grow in size and ambition, giving them direct terminal access to our machines and data becomes more risky. He will present a type-theoretic object-capability architecture that provably bounds agent behavior, with per-task capability signatures shaped by humans and weak AI supervisors to enforce the principle of least authority.