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.