In 1987, while delivering a keynote on data abstractions and hierarchies, Barbara Liskov introduced the idea that would eventually become the Liskov substitution principle. The following is a modern (and very formal) description of the principle:
Let Φ(x) be a property provable about objects x of type T. Then