### 4 papers:

- TLCA-2005-AbelC #algorithm #framework #logic #similarity
- Untyped Algorithmic Equality for Martin-Löf’s Logical Framework with Surjective Pairs (AA, TC), pp. 23–38.
- ICALP-1991-CurienC #reduction #λ-calculus
- A Concluent Reduction for the λ-Calculus with Surjective Pairing and Terminal Object (PLC, RDC), pp. 291–302.
- LICS-1989-Vrijer #λ-calculus
- Extending the λ Calculus with Surjective Pairing is Conservative (RCdV), pp. 204–215.
- CSL-1987-BohmP #combinator #finite #reduction #set
- Surjectivity for Finite Sets of Combinators by Weak Reduction (CB, AP), pp. 27–43.