sign in
english version rss feed

inria-00284186, version 1

On the Expressivity of Minimal Generic Quantification

David Baelde () 1

International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (2008)

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.

  • Domain : Computer Science/Logic in Computer Science
  • Keywords : proof theory – generic quantification – fixed points – higher-order abstract syntax
  • Internal note : Extended version of the paper at LFMTP08
 
  • inria-00284186, version 1
  • oai:hal.inria.fr:inria-00284186
  • From: 
  • Submitted on: Monday, 2 June 2008 13:49:42
  • Updated on: Monday, 2 June 2008 15:22:46
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...
all articles on CCSd database...