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