LFP: a logical framework with external predicates
Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practice (LFMTP '12)
By Furio Honsell, Ivan Scagnetto, Luigi Liquori, Marina Lenisa, Petar Maksimovic
Issue Date:September 2012
The LFP Framework is an extension of the Harper-Honsell-Plotkin's Edinburgh Logical Framework LF with external predicates. This is accomplished by defining lock type constructors, which are a sort of diamond-modality constructors, releasing their argument ...