Simon Peyton-Jones <[EMAIL PROTECTED]> writes:
> What I have not done (any volunteers) is to export these rules, or
> the function definitions to a thm prover.
I am in the course of exporting function definitions
(and later probably also rules)
to the term graph transformation system HOPS
(
> Idea 1:
> Export Haskell declarations to a theorem prover, such as HOL
> or PVS. Then
> permit the user of the theorem prover to state and prove
> properties of the
> Haskell program, using the exported definitions.
>
> Ideas 2:
>
> There was recently a discussion about adding "rules" to
>
Idea 1:
Export Haskell declarations to a theorem prover, such as HOL or PVS. Then
permit the user of the theorem prover to state and prove properties of the
Haskell program, using the exported definitions.
Ideas 2:
There was recently a discussion about adding "rules" to Haskell, that document
t
