An Open Logical Framework

Résumé : 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.
Type de document :
Article dans une revue
Journal of Logic and Computation, Oxford University Press (OUP), 2013, 25 (2), 43 p. 〈10.1093/logcom/ext028〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00906391
Contributeur : Luigi Liquori <>
Soumis le : mercredi 20 novembre 2013 - 12:38:19
Dernière modification le : jeudi 11 janvier 2018 - 16:47:41
Document(s) archivé(s) le : vendredi 21 février 2014 - 04:24:01

Fichier

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

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

139