A confluent reduction for the λ-calculus with surjective pairing and terminal object

This publication has 8 references indexed in Scilit:

• A confluent reduction for the λ-calculus with surjective pairing and terminal object
  Published by Springer Nature ,1991
• Confluence results for the pure strong categorical logic CCL. λ-calculi as subsystems of CCL
  Theoretical Computer Science, 1989
• Algebra of constructions I. The word problem for partial algebras
  Information and Computation, 1987
• On the implementation of abstract data types by programming language constructs
  Journal of Computer and System Sciences, 1987
• Strong normalization for typed terms with surjective pairing.
  Notre Dame Journal of Formal Logic, 1986
• The Church-Rosser theorem for the typed $\lambda$-calculus with surjective pairing.
  Notre Dame Journal of Formal Logic, 1981
• Characterization of normal forms possessing inverse in the λ-β-η-calculus
  Theoretical Computer Science, 1976
• Intensional interpretations of functionals of finite type I
  The Journal of Symbolic Logic, 1967