Constructing recursion operators in intuitionistic type theory

This publication has 10 references indexed in Scilit:

• Natural deduction as higher-order resolution
  The Journal of Logic Programming, 1986
• Program verification in a logical theory of constructions
  Published by Springer Nature ,1985
• Lessons learned from LCF: A Survey of Natural Deduction Proofs
  The Computer Journal, 1985
• Propositions and specifications of programs in Martin-Löf's type theory
  BIT Numerical Mathematics, 1984
• An interpretation of Martin-Löf's type theory in a type-free theory of propositions
  The Journal of Symbolic Logic, 1984
• On definition trees of ordinal recursive functionals: Reduction of the recursion orders by means of type level raising
  The Journal of Symbolic Logic, 1982
• Deductive synthesis of the unification algorithm
  Science of Computer Programming, 1981
• Proving termination with multiset orderings
  Communications of the ACM, 1979
• Functionals defined by transfinite recursion
  The Journal of Symbolic Logic, 1965
• The constructive second number class
  Bulletin of the American Mathematical Society, 1938