Category Archives: Local

Isabelle, Local

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)
Isabelle, Local

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.

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
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.

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!