(See also updated version with more details.)
A full-day tutorial on Isabelle is scheduled as associated event of the 25th International Conference on Automated Deduction (CADE-25), which will take place in Berlin at the start of August 2015.
More than 25 years ago, Isabelle was initiated by Larry Paulson as a logical framework for rapid prototyping of Natural-Deduction proof systems. Today, Isabelle is one of the major platforms for Interactive Theorem Proving (ITP), with notable support for automated reasoning tools (ATPs and SMTs). Isabelle/HOL is the main environment for applications; it is accompanied by the Archive of Formal Proofs (AFP) as repository for user-contributions. Isabelle supports logical tool development in Isabelle/ML and Isabelle/Scala, but it is also possible to connect external tools; this works routinely on Linux, Windows, and Mac OS X. The system presents itself to the end-user by an advanced Prover IDE: Isabelle/jEdit.
The purpose of the tutorial is to help participants to get acquainted with Isabelle: topics will cover specifications in HOL, proofs in Isar, use of automated provers via Sledgehammer etc. The target audience are doctoral students or researchers with an interest in formalized reasoning, application of reasoning tools for interactive and automated proof development, maybe even with an interest to develop their own tools with/for Isabelle.
There will be presentations by myself and one or two colleagues, with hands-on tutoring and exercises done by the participants on their own computers (with at least 2 cores and 4 GB memory).
Further organizational details will emerge sooner or later, as summer 2015 approaches. Watch this space, as well as the main CADE-25 website.
The Conferences on Intelligent Computer Mathematics (CICM) — with the distinctive sub-conferences Calculemus, DML, MKM — may be seen as a gathering of fringe groups, but a very interesting one. Traditionally, it may serve as a forum for experimentation and unorthodox contributions that are difficult to publish elsewhere.
I have served several times on the PC of Calculemus or MKM, and once as PC chair of MKM. For CICM 2015, I am PC member for Calculemus.
Don’t be confused by the website that is somewhat difficult to navigate! Don’t miss the start of the submission process: 16-Feb-2015 for abstracts, followed by actual papers, followed the rebuttal phase. The latter is particularly important to readjust the initial verdict by the reviewers, going upwards or downwards, depending on careful reactions of the authors to what was said about their papers.
Born 28-Mar-1928 (Berlin, Germany), died 13-Nov-2014 (Saint-Lizier, France).
In my own studies, I have occasionally encountered the famous name of Grothendieck in lectures about functional analysis and logic. From a bit later, I remember discussions with Helmut Schwichtenberg about Tarski-Grothendieck set theory as the foundation of the formal mathematical language of Mizar.
In 2010, I came again across the name of Alexander Grothendieck several times, when searching the web about my new hometown Bures-sur-Yvette, where I lived until August 2014 only a few hundred meters from the famous IHÉS institute. That was the place where Grothendieck worked for some time at the peak of his mathematical life (until 1970). Afterwards he removed himself more and more from public and scientific life.
Winfried Scharlau has started to publish material about the life of Grothendieck some years ago, with this notable article from 2006/2008. There was also some activity on the web to collect more information, but this was stopped abruptly in 2010 with this angry letter from Grothendieck himself, speaking to the world from a secret place in the Pyrenees.
Here is another blog with many more links.