Santiago Cuellar will present his FPO "Concurrent Permission Machine for modular proofs of optimizing compilers with shared memory concurrency" on Friday, March 13, 2020 in CS 402 at 10:30am. The members of his committee are Andrew Appel (adviser); Readers: Zachary Kincaid and Gil Hur (Seoul National University); Examiners: Lennart Beringer, Aarti Gupta, and Andrew Appel. A copy of his thesis, is available upon request. Please email ngotsis@cs.princeton if you would like a copy of the thesis. Everyone is invited to attend his talk. The talk abstract follows below: Optimizing compilers change a program based on a formal analysis of its code, and modern processors further rearrange the program order. It is hard to reason about such transformations, which makes them a source of bugs, particularly for concurrent shared-memory programs where the order of execution is critical. On the other hand, programmers should reason about their program in the source language, which abstracts such low level details. We present the Concurrent Permission Machine (CPM), a semantic model for shared-memory concurrent programs, which is: (1) sound for higerh-order Concurrent Separation Logic, (2) convenient to reason about compiler correctness, and (3) useful for proving reduction theorems on weak memory models. The key feature of the CPM is that it exploits the fact that correct shared-memory programs are permission coherent: threads have (at any given time) noncompeting permission to access memory, and their load/store operations respect those permissions. Compilers are often written with sequential code in mind, and proving the correctness of those compilers is hard enough without concurrency. Indeed, the machinechecked proof of correctness for the CompCert C compiler was a major advance in the field. Using the CPM to conveniently distinguish sequential execution from concurrent interactions, I show how to reuse the (sequential) CompCert proof, without major changes, to guarantee a stronger concurrent-permission-aware notion of correctness