Lab Lunch by Wilmer Ricciotti
Wilmer Ricciotti will speak about Formal Language Theory in MF2. Biscuits as usual by Fabian Peternek.
What 


When 
Sep 29, 2015 from 01:10 PM to 02:00 PM 
Where  MF2 
Add event to calendar 
vCal iCal 
Speaker: Wilmer Ricciotti
Title: Formalizing Turing Machines
Abstract: We discuss some lessons learned in the formalization, in a proof assistant, of basic results on Turing Machines, up to the existence of a (certified) Universal Machine. Turing Machines provide an interesting benchmark for proof assistants, since their noncompositional nature makes naive approaches to formalization unfeasible, except for very simple cases. Our formalization shows how to define a compositional semantics for this domain, essentially providing a straightforward verification style for suitably written Turing Machines.