Implementing first order logic in Modula-2 using an intuitionistic approach
Wei Li · 1988
A type theory is given using extended Modula-2 constructs, and a subset of first order logic is interpreted by certain type constructors of this theory. Under this theory, given a formula of the form for all x find a y such that R(x,y) as a specification, program synthesis amounts to proving the truce of the formula. During the proof a Modula-2 program is extracted automatically which meets the specification.