All posts by Makarius

Isabelle, Local

Isabelle presentation at Curry Club Augsburg

On Thu 17-Mar-2016 there will be a presentation about “Programs and Proofs in Isabelle/HOL” at Curry Club Augsburg.

Start: approximately 19:30–20:00
Duration: approximately 60min
Language of the talk: German

Outline:

  • Isabelle and the LCF prover family: origin of ML (Meta-Language)
  • Isabelle as framework for domain-specific formal languages
  • Isabelle document preparation: formal LaTeX + Markdown
  • Isabelle/ML: tool implementation language
  • Isabelle/Scala: system programming language
  • “Programming” in Isabelle/HOL: the main Object-Logic
  • Example: list operations and induction proofs (with code-generation to SML, OCaml, Scala, Haskell)
  • Structured proofs in Isabelle/Isar
  • Example: Cantor’s Theorem in HOL
  • Example: Run-Length Encoding in HOL
Isabelle

Release candidates for Isabelle2016

The coming Isabelle2016 release is scheduled for February 2016. This spot is continuously updated to inform about the ongoing process of testing release candidates.

  • On 01-Jan-2016 an informal snapshot Isabelle2016-RC0 was published. In this version, the website, NEWS, ANNOUNCE etc. are already mostly up-to-date. Some documentation is still lagging behind, notably the Isabelle/jEdit manual.
  • On 15-Jan-2016 the first formal release candidate Isabelle2016-RC1 was published. The main work is finished. Some documentation requires further revisions. We now need serious testing by users to expose remaining problems.
  • On 25-Jan-2016 the second release candidate Isabelle2016-RC2 was published. It includes the latest jdk-8u72 from Oracle: it is important to test this thoroughly on all platforms.
  • On 01-Feb-2016 the third release candidate Isabelle2016-RC3 was published. It includes the official Poly/ML 5.6 release. Some minor points have been polished in the Isabelle code base and documentation.
  • On 06-Feb-2016 the fourth release candidate Isabelle2016-RC4 was published. Some minor points have been improved in Sledgehammer and Isabelle/jEdit GUI reactivity.
  • On 12-Feb-2016 the fifth release candidate Isabelle2016-RC5 was published. It includes more material on Isar language updates in the isar-ref manual. Poly/ML 5.6 has been modified to use GNU bash for OS.Process.system, in order to help Debian-testing-unstable propagate the Isabelle settings environment – with shell functions, as documented in the bash man page!

As usual it is important to keep general laws of causality in mind: release candidates may still change, but the final release is final. So the best time to start testing is now!

The main forum for discussion of Isabelle2016 release candidates is on isabelle-users mailing list.

Update: The final release of Isabelle2016 (February 2016) is now available from the Isabelle website. The above release candidates will disappear eventually.

Local, Media

Freie Medien in Deutschland

Man sagt, in Zeiten des Krieges sei die Wahrheit das erste Opfer. Die Sache funktioniert aber andersherum: Zuerst wird die offiziell verlautbarte Wahrheit massiv manipuliert und danach ist das Volk bereit für den Krieg.

Der mündige und aufgeklärte Bürger muß sich heute selber im Freien Netz informieren. Große Medienkonzerne und öffentlich-rechtliche Nachrichtenkanäle können einem diese Verantwortung nicht abnehmen.

Hier eine kleine Liste von Startpunkten im Netz, von wo man mit wachem Auge und Verstand weitersuchen kann:

Achtung: Wikipedia ist für politische Fragen kaum geeignet. Man kann hier lediglich herausfinden, was die offizielle Lesart ist. Kontroverse Diskussionen verschwinden meist unbeachtet im Archiv der “Diskussion” und in der “Versionsgeschichte” von Artikeln.

Achtung: Öffentliche Beschimpfung von Nachrichtenvermittlern tut nichts zur Sache. Ein mündiger Medienkonsument lernt schnell, wo relevante Information geboten wird und wo nicht. Dabei spielt es keine Rolle, was “man” über den einen oder anderen Kanal woanders sagt oder hört.

Isabelle, Science

Intelligible semi-automatic reasoning in December 2015

A presentation on old and new aspects of Isabelle/Isar will happen 04-Dec-2015 10:00 at Univ. Bonn (Workgroup of Prof. Koepke). See also the web page of Oberseminar mathematische Logik.

Abstract:

Isabelle was introduced in 1989 (by L. Paulson) as a generic logical framework for higher-order natural deduction. Intelligible semi-automated reasoning (Isar) was introduced in 1999 (by M. Wenzel) as a structured proof language for human-readable formal proof documents. Today, in December 2015, we see large applications of Isabelle/Isar in the Isabelle/HOL object-logic, e.g. in the Archive of Formal Proofs with more than 240 entries.

After so many years, development of Isar is still not finished. Recent refinements of old concepts and additions of new concepts include: structured rule statements (Eigen-contexts), multi-branch elimination (case-splitting), structured backwards refinement. The new Eisbach language (by D. Matichuk et al) allows to define complex proof methods in their usual syntax, instead of traditional Isabelle/ML. Sledgehammer (by J. Blanchette et al) allows to generate semi-intelligible Isar proofs from machine-generated proofs (via external ATPs and SMTs).

The ultimate aim of Isabelle/Isar is to turn the results of formal proof production into mathematical documents with nice type-setting. Document source was mainly written in LaTeX in the past, but is now moving towards Markdown, with specific GUI support in the Prover IDE (Isabelle/jEdit).

The Slides are available.

Isabelle

Isabelle Tutorial at Bonn

A tutorial on Isabelle for students of mathematics will happen 03/04-Dec-2015 at Univ. Bonn (Workgroup of Prof. Koepke). The detailed schedule is available on the web page of Praktikum Mathematische Logik. The main language of the tutorial is German; materials are in English.

Notable topics

  • Isabelle/Pure as logical framework for Natural Deduction
  • Isabelle/Isar as proof language for formalized mathematics
  • Isabelle/ML as environment for developing tools for logic applications (including Prover IDE support)

Prerequisites

The tutorial uses the following snapshot of the emerging winter release: Isabelle_01-Dec-2015.

Moreover, a full installation of LaTeX is required (Linux: TeX Live via package manager, Windows: MiKTeX, Mac OS X: MacTeX).

Materials

PIDE, Science

HOL4 workshop at CADE-25

The HOL4 workshop will happen on Sunday 02-Aug-2015 and Monday 03-Aug-2015 in Berlin, as an associated event of the 25th International Conference on Automated Deduction (CADE-25). The main theme are future directions and visions on HOL4 development: both users and developers are invited to participate in the discussion.

Even though I am myself not an HOL4 person, I will give a presentation about Isabelle/PIDE/jEdit as integrated development environment for Standard ML. The abstract is as follows:

After more than 7 years of development, Isabelle/PIDE/jEdit is today the standard way to interact with that particular proof assistant. In Isabelle2015 (May 2015) the TTY-based REPL and its wrapper for Proof General / Emacs have already been dismantled. This radical move might be taken as an opportunity of the HOL4 community to attract former Isabelle users who really do want to use plain TTY interaction. Or as an opportunity to discuss possibilities for HOL4 users and developers to make their own moves towards full-scale IDE support.

As a very modest start, I would like to present various possibilities of Isabelle/PIDE to operate as IDE for Standard ML, which happens to be the underlying language platform of HOL4 as well. This touches various facilities of Poly/ML that David Matthews provides specifically to tool builders: run-time compiler invocation with IDE feedback, toplevel environment management, structured toplevel printing (with markup and hyperlinks), and potentially also run-time debugging of SML (still unused in Isabelle2015).

Beyond that it is also possible to integrate any other languages that are related or unrelated to the prover platform, using PIDE libraries either on the ML or Scala side of that IDE framework.

Isabelle, Science

Isabelle Tutorial at CADE-25

A full-day tutorial on Isabelle will happen Saturday 01-Aug-2015 in Berlin, as an associated event of the 25th International Conference on Automated Deduction (CADE-25). Here is some further organizational information about tutorials at CADE-25. Important materials for the tutorial are available at the bottom of this post.

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 get acquainted with Isabelle, using the latest release Isabelle2015 (May 2015). Topics 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 Makarius Wenzel and Christian Sternagel, with hands-on tutoring and exercises done by the participants on their own computers (at least 2 cores and 4 GB memory).

Materials

Local

Curry Club Augsburg: inaugural meeting

The inaugural meeting of the newly formed Curry Club Augsburg will happen on Thu 23-Apr-2015 19:00 at OpenLab.

The club was initiated by a group of Haskell enthusiasts, and has the potential to cover a wide perspective of Higher-order Functional Programming, Category Theory, Type Theory, Theorem Proving, and more.

After the first meeting, there will be an opportunity to consume actual Curry at an Indian restaurant in medieval downtown of Augsburg.

Very hot indeed!

Isabelle

Release candidates for Isabelle2015

The release of Isabelle2015 is scheduled for this spring, presumably the end of May, or the start of June. As usual, there are several weeks for thorough testing of release candidates that are available here:

With ever increasing size and complexity of the system and its many add-on tools, it is important to take testing of release candidates seriously. Problems can be solved before the release, not after it!

The main forum for discussion is on isabelle-users mailing list.

The convergence towards the final release happens on the following repository.

Update: The final release of Isabelle2015 (May 2015) is now available from the Isabelle website. The above release candidates will disappear eventually.