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.
