Incremental Recompilation for Standard ML of New Jersey

1994 ◽  
Author(s):  
Robert Harper ◽  
Frank Pfenning ◽  
Peter Lee ◽  
Eugene Rollins
Keyword(s):  
New Jersey ◽  
Standard Ml

Weak polymorphism can be sound

1996 ◽  
Vol 6 (1) ◽  
pp. 111-141 ◽  
Author(s):  
John Greiner
Keyword(s):  
New Jersey ◽  
Type System ◽  
Type Systems ◽  
Type Inference ◽  
Inference Algorithm ◽  
Standard Ml ◽  
Polymorphic Type

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.

Functional unparsing

1998 ◽  
Vol 8 (6) ◽  
pp. 621-625 ◽  
Author(s):  
OLIVIER DANVY
Keyword(s):  
New Jersey ◽  
Dependent Types ◽  
Standard Ml ◽  
Control String

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.

A Debugger for Standard ML

1995 ◽  
Vol 5 (2) ◽  
pp. 155-200 ◽  
Author(s):  
Andrew Tolmach ◽  
Andrew W. Appel
Keyword(s):  
New Jersey ◽  
Compiler Optimization ◽  
Source Code ◽  
Runtime System ◽  
Portable Instrumentation ◽  
Standard Ml ◽  
Internal Mechanism ◽  
Source Level

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.

Characterization of object behaviour in Standard ML of New Jersey

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

A theory of weak bisimulation for Core CML

1998 ◽  
Vol 8 (5) ◽  
pp. 447-491 ◽  
Author(s):  
WILLIAM FERREIRA ◽  
MATTHEW HENNESSY ◽  
ALAN JEFFREY
Keyword(s):  
New Jersey ◽  
Process Algebra ◽  
Operational Semantics ◽  
Semantic Theory ◽  
Higher Order ◽  
Order Process ◽  
First Order ◽  
Standard Ml ◽  
Weak Bisimulation ◽  
Bisimulation Equivalence

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