SML Introduction

• Readings
• A bit of history
• Using the interpreter
• Equality types and reals
• Lazy evaluation
• Overloaded operators
• Variable declaration
• Tuples
• Lists

Readings

• Pre-recorded lecture
• An SML Tutorial
• The Definition of Standard ML Complete specification of the language’s syntax and semantics.
• LCF
• Isabelle proof assistant

A bit of history

• ML was designed by Robin Milner and others on the early seventies.

• ML has many dialects, we will be using SML, which stands for Standard ML.

• It was designed as the meta-language (ML stands for “meta-language”) for LCF (Logic for Computable Functions)

• LCF was one of the first automated theorem provers, which are tools that automate logic reasoning to prove theorems. Current automated theorem provers to use ML as meta-language include HOL4 and Isabelle.

• One of the few languages to have been completely formally specified. Link

• There is even a formally verified compiler for a substitiantial set of SML, CakeML.

• We will be using mostly interpreted ML.

Using the interpreter

TODO

Equality types and reals

TODO

Lazy evaluation

TODO

Overloaded operators

TODO

Variable declaration

TODO

Tuples

TODO

Lists