An Open Logical Framework - Archive ouverte HAL Access content directly
Journal Articles Journal of Logic and Computation Year : 2013

An Open Logical Framework

(1) , (1) , (2) , (2) , (1)
1
2

Abstract

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 Star-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 sub-structural 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 Poincaré Principle or Deduction Modulo. Indeed such paradigms can be adequately formalized in LFP. We investigate and characterize the meta-theoretical 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. Moreover, we provide a canonical presentation of LFP, based on a suitable extension of the notion of βη-long normal form, allowing for smooth formulations of adequacy statements.
On présente LFP, un Cadre Logique avec Prédicats Externes, en introduisant un mécanisme pour bloquer et débloquer les types et les termes dans LF, en permettant l'utilisation d' "Oracles" qui peuvent être appelés en dehors du cadre logique principale. On démontre que LFP satisfait tous les propriétés principales méta-théorétiques et on développe un Cadre Canonique correspondant, permettant de prouver facilement la propriété d' "Adéquation". On présente diverses encodages comme, par exemple, le λ-calcul non-typé avec une stratégie de réduction Call-by-Value, le paradigme de la "Programmation-par-Contrats", un petit langage impératif avec la Logique de Hoare, des Logiques Modales dans le styles de la Déduction Naturelle et de Hilbert, et la Logique Linéaire Non-Commutative (encodée pour la première fois dans un cadre logique à la LF), en montrant aussi qu'avec LFP on peut codifier aisément des side-conditions dans l'application des règles de typage ainsi qu'on peut atteindre, si nécessaire, une séparation entre "Vérification" et "Calcul", en obtenant au final des preuves plus claires et lisibles. On pense que les résultats présentés dans cette thèse pourront servir de base pour de futures recherches fructueuses. D'une part, les preuves de correction officiels obtenus rajoutent un niveau supplémentaire de sécurité quand il s'agit de la conception de Systèmes Experts utilisant les logiques vérifiées formellement, et ouvrent une voie à la vérification formelle à d'autres logiques probabilistes. D'autre part, des améliorations et des extensions sont possibles et envisageables comme une analyse plus profonde du cadre LFP, l'implémentation d'un Prototype de Démonstrateur Interactif basé sur LFP et la découverte de sa place dans la pléthore des assistants à la preuve.
Fichier principal
Vignette du fichier
main.pdf (468.48 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00906391 , version 1 (20-11-2013)

Identifiers

Cite

Furio Honsell, Marina Lenisa, Luigi Liquori, Petar Maksimovic, Ivan Scagnetto. An Open Logical Framework. Journal of Logic and Computation, 2013, 25 (2), 43 p. ⟨10.1093/logcom/ext028⟩. ⟨hal-00906391⟩

Collections

INRIA INRIA2
83 View
140 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More