Skip to main content

State Time Geometry: A Formal Model Describing Execution of Real-World Software

Peter Braam

State Time Geometry (STG) is a formal model of program execution inspired by the physical modelling of evolving systems. It uses category theory both in the style of typed programming languages and in novel ways to describe abstract and physical computing infrastructure, transient computational failures, and state observability. Traditional formal models often arise as quotients of STG, yielding narrower, focussed models tailored for precise evaluation and proof.

(In a companion lecture in the Mathematical Institute at 14:00 on 12 Nov, we will discuss how STG can model causal performance profiles and optimal data transport.)

Speaker bio

Peter Braam is a scientist and technologist working on problems in systems software, large-scale scientific computing, and formal methods. Educated as a pure mathematician under Sir Michael Atiyah, he began his career in academia at Oxford, Carnegie Mellon, and Cambridge. He later co-founded a startup that developed the Lustre file system, which remains the de facto standard in large-scale scientific computing more than 25 years after its introduction. His current work focuses on declarative infrastructure software and geometric approaches to reasoning about the execution of computations. He is presently affiliated with Oxford’s Mathematical Institute and Department of Physics, and with Computer Science at Waseda University.