Title: A hierarchical technique for mechanical theorem proving and its application to programming language design
First published: 1976