Category Archives: Local

Video for Isabelle/PIDE presentation at Curry Club Augsburg

Here is the video for the Isabelle/PIDE presentation at Curry Club Augsburg from 14-Jun-2018:

There are some technical challenges: missing screen recording in the first 25min, and occasional changes in the speed of screen recording later on: sometimes the computer screen is ahead of the talk. Nonetheless, this is an opportunity to learn many things about Isabelle/PIDE, how it is done, why it is done like that.

Isabelle/jEdit as Formal IDE at Curry Club Augsburg

On Thu 14-Jun-2018 I will talk about Isabelle/jEdit as Formal IDE at Curry Club Augsburg.

Start: approximately 19:00.
Duration: undefined.
Language of the talk: German
Slides: PDF

This is a spin-off from the paper that I will present at the F-IDE workshop on Sat 14-Jul-2018 in Oxford.

Jugend forscht: Hilbert meets Isabelle

A group of smart students from Bremen have been working on a formalization of Hilbert’s 10th Problem (DPRM Theorem) in Isabelle since October 2017. See also the forthcoming presentation on the Isabelle Workshop 2018 (13-Jul-2018, Oxford, UK) with the following pre-print paper.

A subgroup of particularly young students have also submitted their contribution to the project in the German science competition “Jugend forscht”, and have now won various prizes, notably the “Prize for Extraordinary Work” by Federal President of Germany, Frank-Walter Steinmeier. The catalog of winners lists the project on page 4, with the following laudatio:

Die Jury war begeistert von der Tiefe und begrifflichen Präzision, mit der sich die drei Jungforscher dem komplexen Thema des formalen Verifizierens annahmen. Formale Verifikation ist ein hochaktuelles und wichtiges Thema. Die anspruchsvolle und außergewöhnliche Forschungsarbeit leistet einen wichtigen Beitrag, die Fundamente der Mathematik noch ein Stück stabiler zu machen.

The jury was enthusiastic about the depth and conceptual precision with which the three young researchers addressed the complex topic of formal verification. Formal verification is a highly topical and important topic. The demanding and extraordinary research work makes an important contribution to making the foundations of mathematics even more stable.
(Translated with www.DeepL.com/Translator)

There are some sources and presentation materials on GitLab.

The Isabelle community is looking forward to the final completion of the formalization!

Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?

Die Internationale Kelleruni Herrenbach veranstaltet im April eine öffentliche Vorlesung über Bitcoin und Blockchain.

Thema:
Bitcoin, das Zahlungsmittel der Zukunft? Was ist dran am Bitcoin-Hype?
Referenten:
Dr. Makarius Wenzel
Autor Christoph Ulrich Mayer
Zeit:
Freitag, 13. April 2018 um 19:30
Ort:
Lebensraum Schwabencenter (“Wohnzimmer”)

Das “Wohnzimmer” im Schwabencenter ist ein umgenutztes Ladenlokal innerhalb des regulären Einkaufszentrums. Nach der Vorlesung gibt es noch etwas zu Essen.

Peter Biet von der Kelleruni schreibt hierzu:

Ich selber bin auf diese Vorlesung sehr gespannt, denn ich lese davon ständig in der Zeitung. Ich höre von vielen gerade jungen Menschen, die relativ große Summen in Bitcoins investieren und damit dann auch tatsächlich “richtig Kohle” machen. Ich höre von der Möglichkeit, Geldflüsse unabhängig von Banken zu inszenieren, aber auch von Schwarzgeldern, die da gewaschen werden. Ich höre außerdem von den riesigen Rechnerleistungen, die benötigt werden, um Bitcoins zu schürfen. Und vor allem weiß ich Eines: Ich verstehe das Ganze überhaupt nicht. Finde, obwohl ich versucht habe, mich zu informieren einfach keinen Zugang zu der Sache.
Vielleicht geht es manchen von euch ja genau so. Jedenfalls bin ich des Öfteren gebeten worden, dass wir uns mal dieses so aktuellen Themas annehmen sollten. Und so freue ich mich sehr und bin gewiss, dass Makarius und Christoph da etwas Licht in mein/unser Wissensdunkel bringen werden.

Hier das Material von Makarius.

Foundations of Higher-Order Logic at Curry Club Augsburg

On Thu 01-Dec-2016 there will be a presentation about “Foundations of Higher-Order Logic with Classical Reasoning and Hilbert-Choice” at Curry Club Augsburg.

Start: approximately 19:00
Duration: approximately 90min
Language of the talk: German

Overview:

  • History of Higher-Order Logic
  • Implementations of HOL
  • Quasi-programming in Isabelle/HOL
  • Isabelle foundations: primitive inferences, object-logic rules, rule composition, structured proofs
  • Foundations of Higher-Order Logic: actual Isabelle/HOL, Pure bootstrap of HOL
  • Isabelle theory with some exercises (for Isabelle2016-1)

Video for Isabelle presentation at Curry Club Augsburg

Another Isabelle presentation at Curry Club Augsburg (19-May-2016) has been recorded and uploaded to Youtube.

Materials from the presentation:

  • Exercise from Haskell Workshop 1 + 2 (Dec-2015).
  • Solution produced during the presentation.
  • Slides that were briefly shown towards the end.

To try it interactively (with Prover IDE markup), it is possible to open the URL of the Solution directly in Isabelle/jEdit.