A Conditional Logical Framework

Abstract : The Conditional Logical Framework LFK is a variant of the Harper-Honsell-Plotkin's Edinburgh Logical Framemork LF. It features a generalized form of λ-abstraction where β-reductions fire under the condition that the argument satisfies a logical predicate. The key idea is that the type system memorizes under what conditions and where reductions have yet to fire. Different notions of β-reductions corresponding to different predicates can be combined in LFK. The framework LFK subsumes, by simple instantiation, LF (in fact, it is also a sub-system of LF!), as well as a large class of new generalized conditional λ-calculi. These are appropriate to deal smoothly with the side-conditions of both Hilbert and Natural Deduction presentations of Modal Logics. We investigate and characterize the metatheoretical properties of the calculus underpinning LFK, such as subject reduction, confluence, strong normalization.
Type de document :
Communication dans un congrès
Logic for Programming, Artificial Intelligence, and Reasoning 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, Nov 2008, Doha, Qatar. Springer Verlag, pp.143-157, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-89439-1_10〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00909574
Contributeur : Luigi Liquori <>
Soumis le : mardi 26 novembre 2013 - 14:40:42
Dernière modification le : jeudi 11 janvier 2018 - 16:24:00
Document(s) archivé(s) le : jeudi 27 février 2014 - 09:55:17

Fichier

lpar-08.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Luigi Liquori, Furio Honsell, Marina Lenisa, Ivan Scagnetto. A Conditional Logical Framework. Logic for Programming, Artificial Intelligence, and Reasoning 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, Nov 2008, Doha, Qatar. Springer Verlag, pp.143-157, 2008, Lecture Notes in Computer Science. 〈10.1007/978-3-540-89439-1_10〉. 〈hal-00909574〉

Partager

Métriques

Consultations de la notice

155

Téléchargements de fichiers

69