6533b86dfe1ef96bd12c96ce

RESEARCH PRODUCT

MLOG: a strongly typed confluent functional language with logical variables

subject

description

Poirriez, V., MLOG: a strongly typed confluent functional language with logical variables, Theoretical Computer Science 122 (1994) 201-223. A new programming language called MLOG is introduced. MLOG is a conservative extension of ML with logical variables. To validate our concepts, a compiler named CAML Light FLU0 was implemented. Numerous examples are presented to illustrate the possibilities of MLOG. The pattern matching of ML is kept for X-calculus bindings and an unification primitive is introduced for the logical variables bindings. A suspension mechanism allows cohabitation of pattern-matching and logical variables, Although the evaluation strategy for the application is fixed, the order for the evaluation of the parts of pairs and application remains free. MLOG programs can be evaluated in parallel with the same result obtained irrespective of the particular order of evaluation. This is guaranteed by the Church-Rosser property observed by the evaluation rules. As a corollary, a strict X-calculus with explicit substitutions on named variables is shown to be confluent. A completely formal operational semantics of MLOG is given in this paper.