Translating dependent type theory into higher order logic

This publication has 9 references indexed in Scilit:

• Using Nuprl for the verification and synthesis of hardware
  Philosophical Transactions A, 1992
• Encoding dependent types in an intuitionistic logic
  Published by Cambridge University Press (CUP) ,1991
• Specification and verification using dependent types
  IEEE Transactions on Software Engineering, 1990
• Automating Recursive Type Definitions in Higher Order Logic
  Published by Springer Nature ,1989
• HOL: A Proof Generating System for Higher-Order Logic
  Published by Springer Nature ,1988
• On the syntax of Martin-Löf's type theories
  Theoretical Computer Science, 1987
• Proof Theory and Meaning
  Published by Springer Nature ,1986
• Edinburgh LCF
  Lecture Notes in Computer Science, 1979
• A formulation of the simple theory of types
  The Journal of Symbolic Logic, 1940