MLOG: A strongly typed confluent functional language with logical variables. 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 FLUO was implemented. Numerous examples are presented to illustrate the possibilities of MLOG. The pattern-matching of ML is kept for λ-calculus bindings and an unification primitive is introduced for the logical variables bindings. A suspension mechanism allows cohabitation of pattern-matching and logical variables. Though the evaluation strategy for the application is fixed, the order for 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 λ-calculus with explicit substitutions on named variables is shown to be confluent. A completely formal operational semantics of MLOG is given in this paper.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element