Support has been obtained for this work from the following sources: from INRIA (first through the “Équipes Associées” Slimmer, and the “ADT” BATT), and from the NSF Grants CCR-0429572 (that also included support for Slimmer) and OISE-0553462.
We avoid the usual names (logic variables for existential variables and eigenvariables for universal variables) in order to clearly separate the high-level description given here from the implementation, which is not detailed here, but in which the class of a variable isn’t static.
Actually, such names exist and are accepted by the parser, but are rejected in type, constant and predicate declarations, as they are read-only names, only used for undocumented, internally defined predicates (usually experimental, non-logical, and with side-effects).
Contrary to Teyjus, Bedwyr doesn’t see two variables in the expression X/* Y*/.