Editing Larch Prover (section)

==Development==

LP was developed by [[Stephen Garland]] and [[John Guttag]] at the [[MIT Laboratory for Computer Science]] with assistance from [[Jim Horning|James Horning]] and [[James B. Saxe|James Saxe]] at the [[DEC Systems Research Center]], as part of the [[Larch family|Larch project on formal specifications]].<ref>John V. Guttag and James Horning with S. J. Garland, K. D. Jones, A. Modet, and J. M. Wing, [https://www.cs.cmu.edu/afs/cs/usr/wing/www/publications/LarchBook.pdf ''Larch: Languages and Tools for Formal Specification''], Springer-Verlag Texts and Monographs in Computer Science, 1993.  ISBN 978-1-4612-2704-5.</ref> It extended the REVE 2 equational term [[rewriting]] system developed by Pierre Lescanne,<ref>Pierre Lescanne and "Computer experiments with the REVE term rewriting system generator," ''Proceedings of the 10th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages'', POPL '83, Austin, Texas, Association for Computing Machinery, New York, NY, pages 99&ndash;108.</ref> Randy Forgaard<ref>Randy Forgaard and John Guttag, "REVE:  a term rewriting system generator with a failure-resistant Knuth-Bendix", ''Proceedings of a Workshop on Term Rewriting'', edited by D. Kapur and D. Musser, April 1984, pages 5&ndash;31.</ref> with assistance from David Detlefs and [[Katherine Yelick]].  It supports proofs by equational term rewriting (for terms with associative-commutative operators), cases, contradiction, induction, generalization, and specialization.

LP was written in the [[CLU (programming language)|CLU]] programming language.