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

[PVS] Inductively defined relations in PVS?


Sorry to ask such a basic question, but I *believe* I have come across a
reference in the past which I can no longer find! I know, I should have
noted it at the time - given the relevance of it to my thesis :-((

I believe there exists a paper which discusses "inductively defined
relations" being formalised in PVS, much like the approach taken with
IMP and the Winskel paper Tobias Nipkow wrote in Isabelle/HOL.

I appreciate your time, and any & all clues will be much appreciated, I
will continue my (google) search too!


  AUTHOR = {Tobias Nipkow},
  TITLE = {Winskel is (almost) Right: Towards a Mechanized Semantics
  JOURNAL = {Formal Aspects of Computing},
  VOLUME = 10,
  YEAR = 1998,
  PAGES = {171--186}