Learn Shen
Community Wiki
OS Kernel 
OS Library
Shen Professional

The Shen Logic Lab: PVS

PVS is under continuos development and forms the basis of my final computer science book Program Verification in Shen. The PVS system has two components.

  1. An implementation of a logic Llambda which incorporates polytypes and 2nd order quantification.
  2. An implementation of the Omega algorithm which provides an axiomatic semantics for Shen by automatically translating Shen programs into Llambda.

The reason why there is little help on this page is that PVS is covered in the book. However I've made available here a prototype of Omega for people to play with. To use it.

  1. Choose the PVS plugin in Shen. You get


  1. Load any file f with type checking enabled. This is important, PVS needs the type information.
  2. Choose the render button.
  3. Choose the file f using the popup window that appears.
  4. You'll get a file f.axioms if the process completes successfully.

Usual disclaimers apply; I'm still working on this.