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
【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
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.)
Bio:
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.
Comments are closed
Comments to this thread have been closed by the post author or by an administrator.