Seminar 7 : Solving the Halting Problem (One Language at a Time)

Abstract: In the CompLogic group, we study the design of programming languages that can enforce safety properties at compile time. In this talk, I will describe a small language in which program termination is enforced by the typechecker. Though it restricts the programs one can write, the technique can be extended to more expressive languages. I will show the steps involved in proving the termination property, from defining a formal semantics to writing a machine-checked proof.