The Isabelle club is an informal group, which meets monthly or so to share experience in:
- Modeling in Higher-Order Logic
- Structured Interactive Proofs and Libraries
- Tactic-based Proof-Automation
- Interactive Proof-Systems as Platforms for Formal Tool Development
The scope of the Isabelle-Club is oriented, but not limited to the Isabelle/HOL system.
The Isabelle club organisation follows a Dagstuhl-Seminary-like scheme: On each meeting, out of a list of theme proposals, the participants select one (for which usually one participant feels to be sufficiently prepared). Clubs emphasize open discussions, usually NOT following a pre-fabricated slide-set or talk, at least ideally. "Clubs" are complements to formal laboratory research seminaries, not their replacement. As in Dagstuhl-Seminaries, emphasis is put on a written protocol of the discussion with screenshots, links, examples.
Prior session protocols are:
- November 24 2021 (ENS Ulm): What is a Proof in Isabelle
- September 4 2020: Isabelle Kernel Programming
- September 11 2019: Clean (Isabelle/HOL)
- March 22 2019: (Combined with Test-Club) : Isabelle/C
- November 11 2018: Bu's commented Isabelle
- June 7 2018: Overview over the ODO Project
- March 28 2018: Handling ontologies within Isabelle/PIDE
- February 22 2018: Failure-Divergence Model for CSP in Isabelle/HOL
- November 16 2017: Verified Dweyer Patterns in LTL
- October 5 2017: Verifying C Programs with Isabelle/Simpl/AutoCorres
- May 31 2017: Pearl/Technique: Cartouches in Isabelle
- November 30 2016: Theory: A Brief Summary on UTP and Lenses
- October 20 2016: Project: (Teaching Proofs) theory
- June 22 2016: Project: A state machine free model of Lustre
- May 11 2016: Problem(1): Aspect of the new Type-Classes; Pearl(2): Symbolic Exection in Monads
- April 7 2016: Pearl: The "Candidats de Réductibilité" Method in Isabelle/Nominals
- March 25 2016: Problem: Non-standard Inductions (Noetherian)(cont.)
- March 2 2016: Problem: Non-standard Inductions (Noetherian)
- February 10 2016: Pearl: Modeling State-machines via Inductive sets and via Monads
- January 27 2016: Project: Formalizing Foundations of the Isabelle Kernel
- January 13 2016: Theory: Foundations of the Isabelle Kernel
- December 16 2015: Pearl: Modeling Binders with Nominal Logics
- December 2 2015: Pearl: Modeling Computational Consistency in Lustre
- November 18 2015: Technique: Code Generation for Abstract Types
- November 4 2015:Project: Using Isabelle Meta-Programmin for a UML-Class-Diagram Package
- October 21 2015: Project: Modeling CFG's for Symbolic Execution
- October 7 2015: Problem: Modeling concurrency: Oders vs. Constructive Interleave
- September 23 2015: Pearl: Termination proofs with Multiset-Orderings
- September 9 2015: Manifest, Diverse (Numeral Classes, have vs. obtain)
Current Theme List:
- The Isabelle/PIDE Framework
- HOL-CSP : New properties
- Porting Isabelle Theories : Some Experiences
- Open Issues in TESL: Bridging the Gap to Infinity
- Integrating Efficient Parsers into the Isabelle Platform
- ...