Mini-ML(ID:1239/min014)

A Simple Applicative Language

People:
Related languages
ML => Mini-ML   Implementation of
Mini-ML => DPML   Extension of
References:
  • Clément, Dominique; Despeyroux, Joëlle; Despeyroux, Th.; Kahn, Gilles "A Simple Applicative Language: Mini-ML" view details
          in Conference Record of the 1986 ACM Symposium on Lisp and Functional Programming, August 1986 view details
  • Clément, Dominique; Despeyroux, Joëlle; Despeyroux, Th.; Kahn, Gilles "A Simple Applicative Language: Mini-ML" RR-0529 Rapport de recherche de l'INRIA 20 pages - Mai 1986 view details Abstract: This paper presents a formal description of the central part of the ML language in Natural Semantics. Static semantics, dynamic semantics, and translation to an abstract machine code are covered. The description has been tested on a computer and we explain why this is feasible. Several facts that one may want to prove about the language are expressed and proved within the formalism.
    External link: Online copy Extract: Introduction
    Introduction
    ML is a programming language with very interesting characteristics from the standpoint of static and dynamic semantics.
    -  ML is a strongly typed language but there is no type declaration: expressions are typed implicitly.
    -  ML exhibits polymorphism:   it is possible to define functions that work uniformly on arguments of many types.
    -  ML allows the définition of higher-order functions: the value of an ML expression may be a closure.
    ML typechecking is the object of numerous discussions in the literature, e.g. [l], [4], {6j, [13], and the use of an inference system to describe ML typing is now widely accepted. On the other hand recent work of Curicn and Cousineau [3] has shown how to compile ML inLo code for an abstract machine, the Categorical Abstract Machine (CAM). Hence we are in a position to describe formally.and completely three aspects of ML: typechecking, dynamic semantics, and translation into CAM code.    
    Without loss of generality, we restrict ML to a central part christened Mini-ML, a simple typed Lambda-calcuIus with constants, products, conditionals, and recursive function definitions.

          in Conference Record of the 1986 ACM Symposium on Lisp and Functional Programming, August 1986 view details