Paper Info
Title
MLOG: a strongly typed confluent functional language with logical variables
Abstract
A new programming language called MLOG is introduced. MLOG is a conservative extensions of ML with logical variables. To validate our concepts, a complier 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. 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 λ-calculus with explicit substitution on named variables is shown to be confluent. A completely formal operational semantics of MLOG is given in this paper.
Year
DOI
Venue
1994
10.1016/0304-3975(94)90207-0
FGCS'921 Selected papers of the conference on Fifth generation computer systems
Keywords
DocType
Volume
confluent functional language,logical variable,functional language
Journal
122
Issue
ISSN
ISBN
1-2
0304-3975
0-0304-3975
Citations 
PageRank 
References 
0
0.34
0
Authors
1
Name
Order
Citations
PageRank
Vincent Poirriez1897.64