Jonathan Sterling receives Marie Sklodowska-Curie postdoc fellowship
Congratulations to postdoc Jonathan Sterling, from the Logic and Semantics research group, who has received the highly prestigious Marie Sklodowska-Curie postdoc fellowship. Jonathan will be working on synthetic methods in program verification, and the aim of the project is to extend the successful STC approach to a wider class of programming models, in particular programming languages with effects.
Software systems mediate a growing proportion of human activity, e.g., communication, transport, medicine, industrial and agricultural production. As a result, it is urgent to understand and better control both the correctness and security properties of these increasingly complex software systems. The diversity of verification requirements speaks to a need for models of program execution that smoothly interpolate between many different levels of abstraction.
Models of program execution vary in expressiveness along the spectrum of possible programming languages and specification logics. At one extreme, dependent type theory is a language for mathematically-inspired functional programming that is sufficiently expressive to serve as its own specification logic. Dependent type theory has struggled, however, to incorporate several computational effects that are common in every-day programming languages, such as state and concurrency. Languages that support these features require very sophisticated specification logics due to the myriad details that must be surfaced in their semantic models.
In the context of dependent type theory, Jonathan has recently developed a new technique called Synthetic Tait Computability (STC) that smoothly combines multiple levels of abstraction into a single language. Inspired by sophisticated mathematical techniques invented in topos theory and category theory for entirely different purposes, STC enables low-level details (even down to execution steps) to be manipulated in a simpler and more abstract way than ever before, making them easier to control mathematically. Perhaps more importantly, the STC method makes it possible to import ideas and techniques from other mathematical fields that are comparatively more developed than programming languages.
*** About the Marie Skłodowska-Curie fellowship ***
The Marie Skłodowska-Curie fellowships are among Europe’s most competitive and prestigious awards, aimed at supporting the best and most promising scientists. The fellowship aims to foster the career development and further training of excellent researchers. Read more about the Marie Sklodowska-Curie postdoc Fellowship on the European Union’s website. Next deadline is September 14, 2022.