Biorthogonality

Biorthogonality, also known as \top\top-closure is a technique whereby ...

Please expand.

History

According to Andrew Pitts, the origins of biorthogonality are lost in the mists of time. Similar techniques occur in Girard's normalization proof for Linear Logic, and Krivine's work on realizability.

In programming language semantics, biorthogonality was first used for relational parametricity results in Pitts and Stark 1998.

They have since been used extensively for reasoning about higher-order stores.

References

Biorthogonality was first used to prove relational parametricity results in

Pitts, Andrew, and Ian Stark. 1998. ‘Operational Reasoning for Functions with Local State’. In Higher Order Operational Techniques in Semantics, edited by A. D. Gordon and A. M. Pitts, 227–73. Publications of the Newton Institute. Cambridge University Press. https://homepages.inf.ed.ac.uk/stark/operfl.pdf

@incollection{pitts_1998,
	series = {Publications of the {Newton} {Institute}},
	title = {Operational {Reasoning} for {Functions} with {Local} {State}},
	url = {https://homepages.inf.ed.ac.uk/stark/operfl.pdf},
	booktitle = {Higher {Order} {Operational} {Techniques} in {Semantics}},
	publisher = {Cambridge University Press},
	author = {Pitts, Andrew and Stark, Ian},
	editor = {Gordon, A. D. and Pitts, A. M.},
	year = {1998},
	pages = {227--273}
}

The notion then reappears in the context of polymorphism coupled with recursion in

Pitts, Andrew M. 2000. ‘Parametric Polymorphism and Operational Equivalence’. Mathematical Structures in Computer Science 10 (3): 321–59. https://doi.org/10.1017/S0960129500003066. pdf

@article{pitts_2000,
	title = {Parametric polymorphism and operational equivalence},
	volume = {10},
	doi = {10.1017/S0960129500003066},
	number = {3},
	journal = {Mathematical Structures in Computer Science},
	author = {Pitts, Andrew M.},
	year = {2000},
	pages = {321--359},
}

The relationship between biorthogonality and admissible relations is discussed in

Abadi, Martín. 2000. ‘⊤⊤-Closed Relations and Admissibility’. Mathematical Structures in Computer Science 10 (3): 313–20. https://doi.org/10.1017/S0960129500003054.

@article{abadi_2000,
	title = {⊤⊤-closed relations and admissibility},
	volume = {10},
	doi = {10.1017/S0960129500003054},
	number = {3},
	journal = {Mathematical Structures in Computer Science},
	author = {Abadi, Martín},
	year = {2000},
	pages = {313--320}
}

I have also seen the following references in places, but cannot work out what it is the origin of:

Nick Benton, Andrew Kennedy, Lennart Beringer, and Martin Hofmann. 2009. Relational semantics for effect-based program transformations: higher-order store. In Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming (PPDP '09). Association for Computing Machinery, New York, NY, USA, 301–312. https://doi.org/10.1145/1599410.1599447

@inproceedings{10.1145/1599410.1599447,
	author = {Benton, Nick and Kennedy, Andrew and Beringer, Lennart and Hofmann, Martin},
	title = {Relational Semantics for Effect-Based Program Transformations: Higher-Order Store},
	year = {2009},
	publisher = {Association for Computing Machinery},
	address = {New York, NY, USA},
	doi = {10.1145/1599410.1599447},
	booktitle = {Proceedings of the 11th ACM SIGPLAN Conference on Principles and Practice of Declarative Programming},
	pages = {301–312},
	numpages = {12}
}