Computing + Mathematical Sciences Lecture

Speaker's Bio:
Adam Chlipala's research applies computer theorem-proving and type systems to problems throughout the software stack, from assembly to high-level, higher-order languages.  His focus is reducing the human cost of mathematically rigorous assurance about software.  He finished his PhD at Berkeley in 2007, with a thesis on compiler verification for higher-order source languages.  Since starting as a postdoc at Harvard, he has continued that line of work, as well as getting involved with semi-automated correctness verification for imperative programs via separation logic, first with the Ynot project, which focuses on high-level functional programs, and more recently with the Bedrock project, which deals with assembly-level reasoning.  Adam also has a longstanding interest in web application programming, including the development of several domain-specific languages.  Through his company Impredicative LLC, he has recently gotten involved in consulting based on his latest web language Ur/Web.