Decidable bounded quantification

1 January 1994

conference paper
Published by Association for Computing Machinery (ACM)

p. 151-162
https://doi.org/10.1145/174675.177844

Abstract

The standard formulation of bounded quantification, system F≤, is difficult to work with and lacks important syntactic properties, such as decidability. More tractable variants have been studied, but those studied so far either exclude significant classes of useful programs or lack a compelling semantics.We propose here a simple variant of F≤ that ameliorates these difficulties. It has a natural semantic interpretation, enjoys a number of important properties that fail in F≤, and includes all of the programming examples for which F≤ has been used in practice.

Keywords

NATURAL SEMANTIC INTERPRETATION
COMPELLING SEMANTICS
IMPORTANT PROPERTY
STANDARD FORMULATION
PROGRAMMING EXAMPLE
IMPORTANT SYNTACTIC PROPERTY
SIMPLE VARIANT
DECIDABLE BOUNDED QUANTIFICATION
SIGNIFICANT CLASS
SYSTEM F
BOUNDED QUANTIFICATION
SEMANTIC INTERPRETATION

This publication has 0 references indexed in Scilit: