archives

Encoding System Fw in predicative dependent type theory

System Fω appears impredicative, but I'm wondering if there is an easy way to embed it into predicative dependent type theory by inferring bounds on universes. Also, if anyone can provide an example of a System Fω term that would be rejected by Coq's typical ambiguity resolver, that would be helpful to me.

Any references or thought are appreciated.

Predicates, ghost predicates and higher order predicates

This short article describes how predicates are handled in Modern Eiffel.

In a similar manner as with functions(described in Functions ... ), predicates can be ghost predicates and/or higher order predicates.