Re: [isabelle] How to verify properties of simple SML programs
The workflow of producing a verified program in Isabelle goes the other
way around — you define the functions in your Isabelle code, and then
instruct Isabelle to generate the corresponding code in SML, OCaml,
Haskell, or Scala, by using the export_code command (see
The SML_file command imports your definitions on the meta level — they
can be used to write automation for finding the proofs, but are
completely outside of the logic and nothing can be proved about them.
Hope this helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and