This paper presents the initial results of a project to determine if the techniques of proof-
carrying code and certifying compilers can be applied to programming languages of realistic …

In 1960, EP Wigner, a joint winner of the 1963 Nobel Prize for Physics, published a paper
titled On the Unreasonable Effectiveness of Mathematics in the Natural Sciences [61]. This …

We describe a technique for automatically proving compiler optimizations sound, meaning
that their transformations are always semantics-preserving. We first present a domain …

We present an internal language with equivalent expressive power to Standard ML, and
discuss its formalization in LF and the machine-checked verification of its type safety in …

Traditional static type systems are effective for verifying basic interface specifications.
Dynamically checked contracts support more precise specifications, but these are not …

We describe the design and implementation of a compiler that automatically translates
ordinary programs written in a subset of ML into code that generates native code at run time …

A simple implementation of an SML-like module system is presented as a module
parameterized by a base language and its type-checker. This implementation is useful both …

A hierarchical module system is an effective tool for structuring large programs. Strictly
hierarchical module systems impose an acyclic ordering on import dependencies among …

We present Rhodium, a new language for writing compiler optimizations that can be
automatically proved sound. Unlike our previous work on Cobalt, Rhodium expresses …

MLJ compiles SML'97 into verifier-compliant Java byte-codes. Its features include type-
checked interlanguage working extensions which allow ML and Java code to call each …