[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS] Z in PVS

Dear colleagues,

Is there any PVS library that for Z or schema calculus?
I've seen some work on this that was published long ago
by Jonathan Bowen on a "Shallow embedding of Z in HOL"
using PVS.

Is there anything like that or close to it available?
If not, are there any particular/known reason why not in PVS?
I mean, it should be possible as ProofPowerZ already has
an embedding of Z in HOL.

Besst wishes,