Lash is a higher-order automated theorem prover written in OCaml and C. Much of the OCaml part came from Satallax. The C part reimplements term representation and operations in an efficient manner with perfect sharing, making Lash much faster at basic term operations than Satallax. The C code was written by Cezary Kaliszyk. The default modes and schedules were determined by Jan Jakubuv.

Latest release: lash-1.14.tgz