[MichaelBurge]

Anything on top of the Calculus of Constructions is usually enough. So it's not a moving target, and there are multiple implementations.