One-Day Tutorial on Nominal Isabelle at IJCAR 2008 --------------------------------------------------
Time: 11th August (just before main conference) Location: Sydney, Australia. Overview: Dealing with binders, renaming of bound variables, capture-avoiding substitution, etc., is very often a major problem in formal proofs about the lambda-calculus and programming language theory. Nominal Isabelle provides an infrastructure for reasoning conveniently about bound variables and alpha-equivalence classes in the proof assistant Isabelle. The aim of this tutorial is to give participants a reading knowledge of nominal techniques and allow them to start using Nominal Isabelle in their own work. The tutorial will be hands-on and therefore participants are encouraged to bring their own laptop. Programme: The tutorial will be organised around four sessions: Session I: basics, substitution lemma, Isar proof language Session II: strong induction principles, contexts with holes, beta-reduction Session III: variable convention and rule inductions, evaluation relation Session IV: function definitions, freshness, support Target audience for the tutorial: Researchers and doctoral students who want to use Nominal Isabelle to formalise proofs from the lambda-calculus, from programming language theory or from proof theory, such as type soundness, Church Rosser, strong normalisation and so on. The tutorial is designed for people who have not necessarily used Isabelle or Nominal Isabelle before, nor have used any other proof assistant. HTML version of this announcement: http://isabelle.in.tum.de/nominal/activities/nominal-ijcar08/ ------------------------------------------------------------------------- Check out the new SourceForge.net Marketplace. It's the best place to buy or sell services for just about anything Open Source. http://ad.doubleclick.net/clk;164216239;13503038;w?http://sf.net/marketplace _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
