Michel Sintzoff. Proof-oriented and applicative valuations in definitions of algorithms. In Arvind, Jack B. Dennis, editors, Proceedings of the 1981 conference on Functional programming languages and computer architecture, FPCA 1981, Wentworth, New Hampshire, USA, October 1981. pages 155-162, ACM, 1981. [doi]