[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS] Z in PVS
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"
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.