Version 0.7.2

Installation instructions

See https://dominique-unruh.github.io/qrhl-tool/install.html

Changes

• Support for Isabelle2023
• Tactics squash and inline work on denotational-equivalence subgoals
• Tactic squash supports a quantum initialization and application of unitary (in addition to assignment and sampling)
• Various bugfixes

Version 0.7.1

Installation instructions

See https://dominique-unruh.github.io/qrhl-tool/install.html

Changes

• Supporting MS Windows (in addition to Linux & MacOS).
• Support for Isabelle2022.
• New tactic sp (strongest postcondition).
• Strongly extended swap tactic: Can now swap program fragments with common variables and rewrite fragments during swap.
  Note: invocation syntax has changed.
• New tactic rewrite: Substitute lines in program by other denotationally equivalent lines.
• New type of subgoal: denotational equivalence. (Supported by tactics byqrhl, inline, rewrite so far.)
• proofgeneral.sh / proofgeneral.ps1 scripts: Do not ignore .emacs file with user configuration
  (add -q to ignore it in case of trouble).
• print goal command for showing current goal in a way suitable for copy & paste to Isabelle theory.
• Proof goal shows line numbers.
• Isabelle startup script run-isabelle.sh renamed to isabelle.sh / isabelle.ps1.
• Various bugfixes.

Version 0.7

Installation instructions

See https://dominique-unruh.github.io/qrhl-tool/install.html

Changes

• Caching computations (redoing already done proof steps is fast)
• Auto-reloading changed included and .thy files
• Support for Isabelle 2021-1
• Focusing commands { } + etc.
• Syntax highlighting in ProofGeneral
• New command isabelle_cmd for arbitrary Isabelle toplevel commands
• equal tactic now gives very detailed explanation of its reasoning (for understanding failures)
• Config file .qrhl-tool.conf also found in home directory
• isabelle command allows to configure Isabelle session
• Isabelle session configured in current directory detected (ROOT/ROOTS file)
• Many bugfixes
• Improved background theory in Isabelle (more proofs, session Bounded_Operators fully proven)

Version 0.6

• Supports/requires an preexisting Isabelle installation (avoids duplication)
• Supports Linux, OS/X, Windows
• Internally uses scala-isabelle instead of libisabelle for controlling the Isabelle process
• A lot more of the background theory (parts concerning bounded operators) is formally now proven in Isabelle/HOL (not a user visible change).

See the README for updated installation instructions.

Version 0.5

For installation instructions, see the README.

arXiv paper updated (v2)

Release matching version 2 of the arXiv paper.

For installation instructions, see the README.

POPL artifact

This version accompanies the POPL 2019 paper "Quantum Relational Hoare Logic" by Dominique Unruh.

For installation instructions, see the README.

arXiv paper published

First public release, accompanying the publication of the paper on arXiv.

For installation instructions, see the README.