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 modality constructors, releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i.e. via introduction, elimination, and equality rules. Using LFP , one can factor out the complexity of encoding specific features of logical systems which would otherwise be awkwardly encoded in LF, e.g. side-conditions in the application of rules in Modal Logics, and substructural rules, as in non-commutative Linear Logic. The idea of LFP is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincare ́ Principle. We investigate and characterize the metatheoretical properties of the calculus underpinning LFP : strong normalization, confluence, and subject reduction. This latter property holds under the assumption that the predicates are well- behaved, i.e. closed under weakening, permutation, substitution, and reduction in the arguments.

LFP - A Logical Framework with External Predicates

HONSELL, Furio;LENISA, Marina;SCAGNETTO, Ivan
2012-01-01

Abstract

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 modality constructors, releasing their argument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are defined using the standard pattern of constructive type theory, i.e. via introduction, elimination, and equality rules. Using LFP , one can factor out the complexity of encoding specific features of logical systems which would otherwise be awkwardly encoded in LF, e.g. side-conditions in the application of rules in Modal Logics, and substructural rules, as in non-commutative Linear Logic. The idea of LFP is that these conditions need only to be specified, while their verification can be delegated to an external proof engine, in the style of the Poincare ́ Principle. We investigate and characterize the metatheoretical properties of the calculus underpinning LFP : strong normalization, confluence, and subject reduction. This latter property holds under the assumption that the predicates are well- behaved, i.e. closed under weakening, permutation, substitution, and reduction in the arguments.
2012
9781450315784
File in questo prodotto:
File Dimensione Formato  
p13-honsell.pdf

non disponibili

Tipologia: Documento in Pre-print
Licenza: Non pubblico
Dimensione 732.25 kB
Formato Adobe PDF
732.25 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/882579
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 8
  • ???jsp.display-item.citation.isi??? ND
social impact