An open logical framework

The LFP Framework is an extension of the Harper-Honsell-Plotkin’s Edinburgh Logical Framework LF with external predicates, hence the name Open Logical Framework. This is accomplished by defining lock type constructors, which are a sort of -modality constructors, releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement.

• Type: Journal
• Year: 2016
• Where: LOGCOM
• Authors: Furio Honsell, Marina Lenisa, Ivan Scagnetto, Luigi Liquori, Petar Maksimovic
• Keywords: LOGCOM 2016, Programming Languages