LVC – Linear Verified Compiler

I was just reading the editorial reviews for the "Why Programs Fail" [0] that you recommended and couldn't agree more with this statement:

"Today every computer program written is also debugged, but debugging is not a widely studied or taught skill. Few books beyond this one present a systematic approach to finding and fixing programming errors." --James Larus, Microsoft Research

This was something my school's CS program severely lacked.

[0] https://www.amazon.com/Why-Programs-Fail-Systematic-Debuggin...

Also there's the (very good) Max Planck Institute for Informatics next door: https://www.mpi-inf.mpg.de/

The SSA Book from INRIA is a fun deep dive in SSA. Amazing what you can do on such a 'dumb' representation. Previous hn link with interesting comments on HN: https://news.ycombinator.com/item?id=9376184

Excellent paper. Just submitted it: https://news.ycombinator.com/item?id=18800570

There’ve been some follow-up papers to Appel’s Compiling with Continuations over the years. The most recent one, Compiling with Contiuations, or Without? Whatever. [1] is pretty interesting — they show a direct-style functional IR with 2nd-class continuations, and describe how it can be used for both traditional SSA-style optimizations, as well as some optimizations that more naturally operate on CPS-style IR.

[1]: https://www.cs.purdue.edu/homes/rompf/papers/cong-preprint20...