Automated reasoning with a constraint-based metainterpreter

Henning Christiansen
Department of Computer Science
Roskilde University, P.O.Box 260, DK-4000 Roskilde, Denmark

A constraint-based method for deriving type declarations from program statements is described. The relation between declarations and a correctly typed program can be characterized by means of instance constraints and the present paper describes experiences using constraint solving techniques to synthesize the type declarations inherent in a given program. Such a facility may turn out to be useful from the viewpoint of programming methodology. It may suggests an integration of an experimental and ``untyped'' style with the higher degree of robustness gained with typed languages.

Extended abstract, March 1997, 7pp., Accepted for Workshop on Constraint Programming for Reasoning about Programming, Leeds, April 9-10th, 1997.
See pdf.