Mechanised Computability Theory
Michael Norrish (NICTA)
LOGIC AND COMPUTATION SEMINARDATE: 2011-05-03
TIME: 15:30:00 - 16:30:00
LOCATION: RSISE Seminar Room, ground floor, building 115, cnr. North and Daley Roads, ANU
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
I will describe how I have mechanised a chunk of basic computability theory, using two models: the recursive functions and the lambda-calculus. I mechanised the result that these models have equivalent computational power. I have also proved simple results such as Rice's Theorem and closure properties for recursive and r.e. sets. I will discuss some technical details about how the mechanisation played out in the HOL4 system, and some of the improvements it prompted.
