Simpler Proof Net Quantifiers: Unification Nets (Work in Progress)

ABSTRACT. Girard formulated an approach to proof net quantifiers over a series of three papers. Since the approach uses explicit witnesses for existential quantifiers, it suffers from two problems: limited proof identification and non-local cut elimination. This paper introduces a more abstract approach, *unification nets*, which solves these problems by leaving existential witnesses *implicit*: a unification net is merely an axiom linking.