Professor of Programming Methods/creator of Scala
I design programming languages, and the type systems that let us reason about promises programs make. Most of my work now is about capabilities: how a we can state precisely what a piece of code (or an AI agent) is allowed to do so that a compiler can check it.
Capture checking adds a lightweight form of dependent typing to Scala 3: a type can record the set of capabilities its values retain. Effects and resources — a file handle, a network connection, the ability to throw an exception or to suspend — become ordinary program variables, and the type system tracks where they flow. That makes salient properties usually left to convention or runtime discipline checkable at compile time. Examples are: a capability cannot escape the scope that owns it, or a computation declared pure cannot quietly acquire capabilities.
The theory is set out in our paper Capturing Types (TOPLAS 2023); the implementation ships as an experimental feature of the Scala 3 compiler, where it is now being used to give safe, direct-style effect handling and concurrency a static foundation.
// Capabilities are values; their types carry the ^ marker. def usingLogFile[T](op: (f: FileOutputStream^) => T): T = val f = FileOutputStream("log") val result = op(f) f.close() result // An escaping capability is a compile-time error, not a dangling handle: val later = usingLogFile { f => () => f.write(0) } // ^^^^^^^^^^^^^^^^^ // local reference f leaks into outer capture set
An AI agent that calls tools directly is a security risk: it can leak private data, hack other systems, or cause harmful side effects nobody asked for, maybe steered by a prompt injection buried in the data it reads. We address this problem by building safety harnesses that leverage capabilities tracked in types. To use a tool, the agent writes code in a capability-safe language — Scala 3 with capture checking — and the compiler decides whether the code is allowed to run. Tools are protected by interfaces that can express fine-grained, context-dependent permissions in their type signatures. This approach is described in our paper Securing Agents With Tracked Capabilities at CAIS 2026.
Designing and implementing software that is reliable, maintainable and efficient: functional programming, data abstraction, parallelism and effects, alongside specification, testing, proof and modularity.
A doctoral seminar on the security of AI agents, read through the current research literature: prompt injection, capability control, sandboxing and provable containment. Students present papers and discuss them.
Earlier, I built EPFL's first MOOC, Functional Programming Principles in Scala, and the specialisation that grew out of it — together more than 800,000 enrolments. The textbook Programming in Scala, written with Lex Spoon, Bill Venners and Frank Sommers, is in its fifth edition, rewritten for Scala 3.
I studied mathematics at LMU Munich and took my doctorate at ETH Zürich in 1989 under Niklaus Wirth, on formal language definition. After postdoctoral years at IBM Research and Yale I taught in Karlsruhe and in South Australia, and came to EPFL in 1999.
In the 1990s, with Philip Wadler, I designed Pizza and then — with Gilad Bracha and colleagues at Sun — GJ, the generics extension that entered Java 5; the GJ compiler became javac, Java's reference compiler. Scala began in 2001 and was first released in 2004, fusing functional and object-oriented programming; Scala 3, a thorough redesign carrying a decade of research, followed in 2021. I founded Typesafe (later Lightbend) in 2011 to support the language commercially, and since 2016 I have been academic director of the Scala Center at EPFL, its not-for-profit home for open source and education.
A full list is on dblp.