A Framework for Defining Logical Frameworks

Luigi Liquori 1, 2 Furio Honsell 3 Marina Lenisa 3
1 MASCOTTE - Algorithms, simulation, combinatorics and optimization for telecommunications
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
2 PROTHEO - Constraints, automatic deduction and software properties proofs
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : In this paper, we introduce a General Logical Framework, called GLF, for defining Logical Frameworks, based on dependent types, in the style of the well known Edinburgh Logical Framework LF. The framework GLF features a generalized form of lambda abstraction where beta-reductions fire provided the argument satisfies a logical predicate and may produce an n-ary substitution. The type system keeps track of when reductions have yet to fire. The framework GLF subsumes, by simple instantiation, LF as well as a large class of generalized constrained-based lambda calculi, ranging from well known restricted lambda calculi, such as Plotkin's call-by-value lambda calculus, to lambda calculi with patterns. But it suggests also a wide spectrum of completely new calculi which have intriguing potential as Logical Frameworks. We investigate the metatheoretical properties of the calculus underpinning GLF and illustrate its expressive power. In particular, we focus on two interesting instantiations of GLF. The first is the Pattern Logical Framework (PLF), where applications fire via pattern-matching in the style of Cirstea, Kirchner, and Liquori. The second is the Closed Logical Framework (CLF) which features, besides standard beta-reduction, also a reduction which fires only if the argument is a closed term. For both these instantiations of GLF we discuss standard metaproperties, such as subject reduction, confluence and strong normalization. The GLF framework is particularly suitable, as a metalanguage, for encoding rewriting logics and logical systems, where rules require proof terms to have special syntactic constraints, e.g. logics with rules of proof, in addition to rules of derivations, such as, e.g., modal logics, and call-by-value lambda calculus.
Type de document :
Rapport
[Research Report] RR-5963, INRIA. 2006, pp.56
Liste complète des métadonnées

https://hal.inria.fr/inria-00088809
Contributeur : Rapport de Recherche Inria <>
Soumis le : lundi 7 août 2006 - 10:56:25
Dernière modification le : mercredi 31 janvier 2018 - 10:24:04
Document(s) archivé(s) le : lundi 20 septembre 2010 - 16:42:52

Fichiers

Identifiants

  • HAL Id : inria-00088809, version 2

Citation

Luigi Liquori, Furio Honsell, Marina Lenisa. A Framework for Defining Logical Frameworks. [Research Report] RR-5963, INRIA. 2006, pp.56. 〈inria-00088809v2〉

Partager

Métriques

Consultations de la notice

428

Téléchargements de fichiers

132