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

Registration: https://www.smartsurvey.co.uk/s/D8MKWE/

External：https://meeting.huaweicloud.com/welink/j/97912020/9moDE7UtWXQYiqGG1PJ3UdJR3ddxuxSD8

Meeting ID：97912020

Passcode：237421

Abstract:

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.

【BAYES COFFEE HOUSE TECH TALK SERIES】The Denotational Semantics of Static Single Assignment (SSA) Form / Huawei-Edinburgh Joint Lab by blogadmin is licensed under a Creative Commons Attribution CC BY 3.0