Standard ML of New Jersey

Author(s):  
Andrew W. Appel ◽  
David B. MacQueen
Keyword(s):  
1994 ◽  
Author(s):  
Robert Harper ◽  
Frank Pfenning ◽  
Peter Lee ◽  
Eugene Rollins
Keyword(s):  

1996 ◽  
Vol 6 (1) ◽  
pp. 111-141 ◽  
Author(s):  
John Greiner

AbstractThe weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the implementation have been shown unsound, the concept has not been proved sound or unsound. We present an explanation of weak polymorphism and show that a formalization of this is sound. We also relate this to the SML/NJ implementation of weak polymorphism through a series of type systems that incorporate elements of the SML/NJ type inference algorithm.


1998 ◽  
Vol 8 (6) ◽  
pp. 621-625 ◽  
Author(s):  
OLIVIER DANVY

A string-formatting function such as printf in C seemingly requires dependent types, because its control string determines the rest of its arguments. Examples:formula hereWe show how changing the representation of the control string makes it possible to program printf in ML (which does not allow dependent types). The result is well typed and perceptibly more efficient than the corresponding library functions in Standard ML of New Jersey and in Caml.


1995 ◽  
Vol 5 (2) ◽  
pp. 155-200 ◽  
Author(s):  
Andrew Tolmach ◽  
Andrew W. Appel

AbstractWe have built a portable, instrumentation-based, replay debugger for the Standard ML of New Jersey compiler. Traditional ‘source-level’ debuggers for compiled languages actually operate at machine level, which makes them complex, difficult to port, and intolerant of compiler optimization. For secure languages like ML, however, debugging support can be provided without reference to the underlying machine, by adding instrumentation to program source code before compilation. Because instrumented code is (almost) ordinary source, it can be processed by the ordinary compiler. Our debugger is thus independent from the underlying hardware and runtime system, and from the optimization strategies used by the compiler. The debugger also provides reverse execution, both as a user feature and an internal mechanism. Reverse execution is implemented using a checkpoint and replay system; checkpoints are represented primarily by first-class continuations.


1994 ◽  
Vol VII (3) ◽  
pp. 43-54 ◽  
Author(s):  
Darko Stefanovic ◽  
J. Eliot B. Moss
Keyword(s):  

1998 ◽  
Vol 8 (5) ◽  
pp. 447-491 ◽  
Author(s):  
WILLIAM FERREIRA ◽  
MATTHEW HENNESSY ◽  
ALAN JEFFREY

Concurrent ML (CML) is an extension of Standard ML of New Jersey with concurrent features similar to those of process algebra. In this paper, we build upon John Reppy's reduction semantics for CML by constructing a compositional operational semantics for a fragment of CML, based on higher-order process algebra. Using the operational semantics we generalise the notion of weak bisimulation equivalence to build a semantic theory of CML. We give some small examples of proofs about CML expressions, and show that our semantics corresponds to Reppy's up to weak first-order bisimulation.


Sign in / Sign up

Export Citation Format

Share Document