Isabelle talk this Friday by Christian Urban
Cameron Freer
Christian Urban is a researcher in logic, theorem provers, and
programming languages, and an Isabelle developer:
http://www4.in.tum.de/~urbanc/
- Cameron
-----------------------------------------------------
Nominal Techniques in the Theorem Prover Isabelle
or, How Not to be Intimidated by the Variable Convention
Christian Urban, Technical University of Munich
Date: Friday, November 21, 2008
Time: 11:00 AM
Location: 32-D463 -- Star Conference Room
Stata Center, MIT
Refreshments: 10:45 AM
ABSTRACT:
Bound variables play an important role in programming language
research and in logic. Nearly all informal induction proofs
involving bound variables make use of the variable convention. In
the talk I will show how strong induction principles can be derived
that have the variable convention already built-in. However, I will
also show that this convention is in general an unsound reasoning
principle and requires restrictions in order to be safe. The aim of
this work is to provide all proving technology necessary for
reasoning conveniently about programming languages and logic calculi.
BIO:
Christian Urban is an Emmy Noether Fellow at the Technical
University of Munich (Germany). He received his Ph.D. in 2000 from
the University of Cambridge (UK). He was a post-doctoral research
fellow at Corpus Christi College in Cambridge from 2000-2004, and
moved to Germany in 2004 with the help of a fellowship from the
Alexander-von-Humboldt Foundation. His current interests include
theorem provers, type systems and semantics of programming languages.
HOST: Professor Martin Rinard -- (For more information please
contact Mary McDavitt, 3-9620)
Larry Freeman
This sounds great. I live on the West Coast. Is there any chance that this will be video'd and posted on the web?
-Larry
If you like number theory, check out:
http://fermatslasttheorem.blogspot.com
Want something way simpler than blogging, check out HubPages.Com:
http://hubpages.com/_yf9r1u5aiqlc/