PVS in Dedukti

PVS is a proof system developed at SRI International, and used by
NASA.  The logic of PVS has been precisely defined by Frédéric Gilbert
in his thesis. The goal of this internship is to formalize this
definition in the lambda-Pi-calculus modulo theory, in order to
express proofs of the PVS in Dedukti.

Advisor: Gilles Dowek

Bibliography: F. Gilbert. Extending higher-order logic with
predicate subtyping: application to PVS,  2017. (chapter 4)