HOL: A Proof Generating System for Higher-Order Logic

This publication has 7 references indexed in Scilit:

• A theory of type polymorphism in programming
  Published by Elsevier ,2003
• A Proof of Correctness of the Viper Microprocessor: The First Level
  Published by Springer Nature ,1988
• Logic and Computation
  Published by Cambridge University Press (CUP) ,1987
• A higher-order implementation of rewriting
  Science of Computer Programming, 1983
• Edinburgh LCF
  Lecture Notes in Computer Science, 1979
• Implementation and applications of Scott's logic for computable functions
  ACM SIGPLAN Notices, 1972
• A formulation of the simple theory of types
  The Journal of Symbolic Logic, 1940