Any views expressed within media held on this service are those of the contributors, should not be taken as approved or endorsed by the University, and do not necessarily reflect the views of the University in respect of any particular issue.

【BAYES COFFEE HOUSE TECH TALK SERIES】The Denotational Semantics of Static Single Assignment (SSA) Form

Neel Krishnaswami from the University of Cambridge will give a talk, in person and online, for the Coffee House Tech Talk Series. Details of the talk are below.

Title: The Denotational Semantics of Static Single Assignment (SSA) Form

Speaker: Neel Krishnaswami

Professor of Logic, Semantics and Computation in the department of computer science at the University of Cambridge

When: 11am Tue 19 March (UTC+00:00)London

Where: 4th floor Bayes Centre



Meeting ID97912020



Static single-assignment form (SSA) is one of the most widely used compiler intermediate representations. In this talk, I build on the observation that SSA can be seen as a language of basic blocks with arguments (or first-order procedures tail-calling one another) to give a type theory for SSA programs. I then give a categorical semantics for this type theory, and show that the equational theory of the language is sound with respect to it. The categorical axiomatization is very standard, namely a Freyd category with Elgot structure, and exhibits a wide variety of concrete models, including even models of weak memory concurrency. This demonstrates that our approach is strong enough to connect machine models of concurrency to compiler IRs supporting a rich collection of sound rewrites. (Joint work with Jad Ghalayini.)


Neel Krishnaswami is Professor of Logic, Semantics and Computation in the department of computer science at the University of Cambridge. His research interests involve applying ideas from type theory, proof theory, and denotational semantics to programming language design and program verification. His current research is focused on applying separation logic to verify the pKVM hypervisor in the Linux kernel, and on the semantics and logical foundations of bidirectional type inference algorithms.

Before coming to Cambridge, he was a lecturer at the University of Birmingham, and held postdocs at Microsoft Research with Nick Benton and the Max Planck Institute for Software Systems with Derek Dreyer. His PhD was supervised by John C. Reynolds and Jonathan Aldrich at Carnegie Mellon University.


Report this page

To report inappropriate content on this page, please use the form below. Upon receiving your report, we will be in touch as per the Take Down Policy of the service.

Please note that personal data collected through this form is used and stored for the purposes of processing this report and communication with you.

If you are unable to report a concern about content via this form please contact the Service Owner.

Please enter an email address you wish to be contacted on. Please describe the unacceptable content in sufficient detail to allow us to locate it, and why you consider it to be unacceptable.
By submitting this report, you accept that it is accurate and that fraudulent or nuisance complaints may result in action by the University.