Email Gateway (Aug 18 2022 at 10:48): Email Gateway (Aug 18 2022 at 10:48):From: Joao Marcos <jmarcos@dimap.ufrn.br>
Dear All:
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?
Best,
JM
Email Gateway (Aug 18 2022 at 10:48):From: Tobias Nipkow <nipkow@in.tum.de>
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 an example.
Tobias
Joao Marcos schrieb:
Email Gateway (Aug 18 2022 at 10:48):From: Michael Fourman <michael.fourman@ed.ac.uk>
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.
0870.68136.
Michael
Michael P. Fourman FBCS CITP School
of Informatics
Professor of Computer Systems Appleton Tower,
Crichton Street
Head of Informatics
Edinburgh EH8 9LE
The University of
Edinburgh Scotland UK
http://www.inf.ed.ac.uk/
For diary entries contact Alex.Judd@ed (etc.) +44 131 650 2690
Last updated: May 03 2024 at 04:19 UTC