LFP - A Logical Framework with External Predicates

Abstract : The LFP Framework is an extension of the Harper-Honsell- Plotkin's Edinburgh Logical Framework LF with external pred- icates. This is accomplished by defining lock type constructors, which are a sort of ⋄-modality constructors, releasing their ar- gument under the condition that a possibly external predicate is satisfied on an appropriate typed judgement. Lock types are de- fined 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 logi- cal 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.
Type de document :
Communication dans un congrès
LFMTP - 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice - 2012, Sep 2012, Copenhagen, Denmark. ACM, pp.13-22, 2012, 〈10.1145/2364406.2364409〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00909455
Contributeur : Luigi Liquori <>
Soumis le : mardi 26 novembre 2013 - 11:49:41
Dernière modification le : jeudi 11 janvier 2018 - 16:43:52
Document(s) archivé(s) le : jeudi 27 février 2014 - 09:31:03

Fichier

LFMTP2012.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Furio Honsell, Marina Lenisa, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto. LFP - A Logical Framework with External Predicates. LFMTP - 7th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice - 2012, Sep 2012, Copenhagen, Denmark. ACM, pp.13-22, 2012, 〈10.1145/2364406.2364409〉. 〈hal-00909455〉

Partager

Métriques

Consultations de la notice

377

Téléchargements de fichiers

99