Isabelle talk this Friday by Christian Urban

Skip to first unread message

Cameron Freer

Nov 19, 2008, 11:52:50 AM11/19/08
Those of you in the Boston area may be interested in this talk.

Christian Urban is a researcher in logic, theorem provers, and
programming languages, and an Isabelle developer:

- 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


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.


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

Nov 19, 2008, 12:53:40 PM11/19/08
Hi Cameron,

This sounds great.  I live on the West Coast.  Is there any chance that this will be video'd and posted on the web?

If you like number theory, check out:

Want something way simpler than blogging, check out HubPages.Com:
Reply all
Reply to author
0 new messages