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

IMG_0301

Date: April 7
Time: 1:00-2:00pm
Location: McConnell Room 320

Speaker: Rohan Jacob-Rao
Title: 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.

Leave a Reply

Your email address will not be published. Required fields are marked *