Re: [isabelle] small verification task
Exactly this (and quite a lot more - ML definitions of datatypes as
well as functions) was possible in the LAMBDA prover, marketed by
Abstract Hardware Limited in the 80s and 90s.
N. Chapman, S. Finn, and Michael P. Fourman. Datatypes in L2. In T.F.
Melham and J. Camillieri, editors, Higher Order Logic Theorem Proving
and its Applications. 7th International Workshop Proceedings, pages
128-43, Valetta, Malta, September 1994. Springer-Verlag; Berlin,
Germany. Invited Paper.
Simon Finn, Michael P. Fourman, and John Longley. Partial functions
in a total setting. J. Automated Reasoning, 18(1):85-104, 1997. Zbl.
On 16 Sep 2007, at 18:46, Tobias Nipkow wrote:
You cannot (yet) verify SML code directly. But you can translate it
by hand into HOL and verify the result. See HOL/Library/GCD.thy for
Joao Marcos schrieb:
Is it possible to write a small piece of code in SML, say, to compute
the GCD of 2 given numbers, and use Isabelle and its induction tactic
to directly verify the correctness of this very code? Anyone would
kindly point to examples where this has been done?
Michael P. Fourman FBCS CITP School
Professor of Computer Systems Appleton Tower,
Head of Informatics
Edinburgh EH8 9LE
The University of
Edinburgh Scotland UK
For diary entries contact Alex.Judd at ed (etc.) +44 131 650 2690
This archive was generated by a fusion of
Pipermail (Mailman edition) and