Magaud, Nicolas; Bertot, Yves (2002), "Changing data structures in type theory: a study of natural numbers", Types for proofs and programs (Durham, 2000), Lecture Notes in Comput. Sci., vol. 2277, Springer, Berlin, pp. 181–196, doi:10.1007/3-540-45842-5_12, ISBN978-3-540-43287-6, MR2044538.
Blaxell, David (1978), "Record linkage by bit pattern matching", in Hogben, David; Fife, Dennis W. (eds.), Computer Science and Statistics--Tenth Annual Symposium on the Interface, NBS Special Publication, vol. 503, U.S. Department of Commerce / National Bureau of Standards, pp. 146–156.
Magaud, Nicolas; Bertot, Yves (2002), "Changing data structures in type theory: a study of natural numbers", Types for proofs and programs (Durham, 2000), Lecture Notes in Comput. Sci., vol. 2277, Springer, Berlin, pp. 181–196, doi:10.1007/3-540-45842-5_12, ISBN978-3-540-43287-6, MR2044538.
Jansen, Jan Martin (2013), "Programming in the λ-calculus: from Church to Scott and back", The Beauty of Functional Code, Lecture Notes in Computer Science, vol. 8106, Springer-Verlag, pp. 168–180, doi:10.1007/978-3-642-40355-2_12, ISBN978-3-642-40354-5.