Caliban

Program verification by symbolic execution of hyperfinite ideal machines. (Extended abstract). ... A program is verified by showing that its traces satisfy its specification. The transition systems are defined in an applicative programming language for which we have a theorem prover. This applicative language, called Caliban, is lazy, higher-order, and polymorphic. The theorem prover, called Clio, provides a meta-language for making assertions about the meanings of Caliban terms. One can write a Caliban expression whose meaning is the trace of a (sub-)program beginning in some initial state. The pre- and postconditions that the initial and final states of such a trace respectively are to satisfy are written in Clio’s meta-language. ...