- This event has passed.
Colloquium – William Bowman
March 16 @ 9:50 am - 11:30 am
March 16, 2018
Host: Alex Lex
Do compilers respect programmers?
Programmers write code in different ways to express more than mere functionality—that is, to express invariants about code such as correctness criteria, performance constraints, or security concerns. Their belief is that the compiler can rely on those invariants, or at least will output code that still satisfies those invariants. Unfortunately, this belief is usually wrong. Existing compilers do not respect programmers and their invariants. Worse still, for years researchers understood that it was *not possible*, in general, to preserve invariants through compilation. Thankfully, this understanding was also wrong.
In this talk, I will introduce this problem and its history, and demonstrate that compilers *can be* designed to respect programmers and their invariants.
William J. Bowman is a 6th year Ph.D. candidate in the College of Computer and Information Science (specializing in programming languages) at Northeastern University. Broadly speaking, he is interested in making it easier for programmers to communicate their intent to machines, and preserving that intent through the stages of compilation. More specifically, his research interests include secure and verified compilation, dependently typed programming, verification, and meta-programming. His recent work examines type-preserving compilation of dependently typed programming language like Coq, a technique that can enable preserving security and correctness invariants of verified software through compilation and statically enforcing those invariants in the low-level (assembly-like) code generated by compilers.