Personoj -- Expressing PVS in Dedukti

Personoj allows to translate developments from the higher order, automated proof assistant PVS into the universal proof checker Dedukti. Personoj uses Lambdapi, an implementation of Dedukti with meta-variables.

This repository contains

• the encoding of PVS into the lambdaPi calculus modulo theory (written in lambdapi),
• patch for PVS that implement a translation from PVS theories to lambdapi,
• patches and programs to cross check PVS proofs in lambdapi

Main requirements

Sub projects may require finer dependencies. We list here the main ones:

• lambdapi, on the branch refiner_why3quant,
• SBCL version 1.4.16,
• PVS sources, revision pvs7.1
• Allegro PVS

More documentation is available in the docs folder.