Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Isabelle Hacks

Every day, you work with Isabelle, you likely learn a new trick. Sadly, you will also have forgotten as quickly as you learned them. To make it easier to rediscover them, and also to make it easier to port them across different versions of Isabelle, we build a collection of “hacks”.

These “hacks” provide additional functionality to Isabelle or showcase specific functionality. Each individual hack usually consists out of a single theory file and all documentation is contained in that theory file The plan is to keep the main branch working with the most current release of Isabelle, and to provide tags for older Isabelle releases. The hacks are available at: Currently, the following hacks are included:

  • Assert.thy provides a new top level command assert that provides a simple way for specifying assertions that Isabelle checks while processing a theory.
  • Hiding_Type_Variables.thy provides print a setup for defining default type variables of type constructors. The default type variables can be hidden in output, e.g., ('a, 'b, 'c) foo is shown as (_) foo. This shorthand notation can also be used in input (using a parse translation), which (sometimes) helps to focus on the important parts of complex type declarations.
  • Nano_JSON.thy provides support for a JSON-like data exchange for Isabelle/HOL.
  • Code_Reflection.thy provides a new top-level command for reflecting generated SML code into Isabelle’s ML environment.

New hacks will be added regularly.

If not otherwise stated, all hacks are licensed under a 2-clause BSD-style license, i.e., the license used for Isabelle itself and for most of the entries in the Archive of Formal Proofs.

Welcome to the blog of the Software Assurance & Security Research Team at the University of Exeter. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.

You can also follow us on Twitter: @logicalhacking.




academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition cordova dast devops devsecops dom dsbd efsm epsrc event extensions fixeffort floss formaldocument formalmethods funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isadof latex logic maintance malicous mbst mobile mobile apps modelinference modeling monads monitoring msc ocl ontology opensource owasp patches pet phd phdlife phishing policy protocols publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartthings softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb test&proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity


blog whole site