On the Expressivity of Minimal Generic Quantification

Abstract : We come back to the initial design of the $\nabla$ quantifier by Miller and Tiu, which we call minimal generic quantification. In the absence of fixed points, it is equivalent to seemingly stronger designs. However, several expected theorems about (co)inductive specifications can not be derived in that setting. We present a refinement of minimal generic quantification that brings the expected expressivity while keeping the minimal semantic, which we claim is useful to get natural adequate specifications. We build on the idea that generic quantification is not a logical connective but one that is defined, like negation in classical logics. This allows us to use the standard (co)induction rule, but obtain much more expressivity than before. We show classes of theorems that can now be derived in the logic, and present a few practical examples.
Type de document :
Communication dans un congrès
Andreas Abel, Christian Urban. International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jun 2008, Pittsburgh, United States. 2008
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00284186
Contributeur : David Baelde <>
Soumis le : lundi 2 juin 2008 - 13:49:42
Dernière modification le : jeudi 12 avril 2018 - 01:47:20
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 15:11:40

Fichier

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

Identifiants

  • HAL Id : inria-00284186, version 1

Collections

Citation

David Baelde. On the Expressivity of Minimal Generic Quantification. Andreas Abel, Christian Urban. International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jun 2008, Pittsburgh, United States. 2008. 〈inria-00284186〉

Partager

Métriques

Consultations de la notice

150

Téléchargements de fichiers

42