Dominic Mulligan
Title:

Lem: real-world semantic engineering

Abstract:

Recent years have seen an increased interest in `real-world semantic
engineering': the creation and use in computer-aided proof of
substantial models of artefacts such as memory models, microprocessors
and their ISAs, programming language semantics, and so on.

However, the engineering principles employed in specifying, building
and validating these models are more often than not rudimentary. Such
models are often directly developed within the logic of a theorem
prover, or a prototype is developed first in a programming language
before being hand-ported, perhaps with the aid of sed or Perl scripts,
into a theorem prover.

As a result of these practices we collectively suffer from
`theorem-prover lock-in' where models cannot be shared--without
substantial effort--amongst the different theorem prover communities,
mass repetition as the same artefacts are repeatedly specified and
modelled by different groups, and a proliferation of incomplete and
badly validated models.

As a solution to these problems, we propose Lem. Lem is a strong,
statically-typed, polymorphic language, similar to OCaml, extended
with specification-oriented features such as sets, inductive
relations, quantification, and so on. Models written in Lem may be
extracted to HOL4 , Isabelle/HOL and Coq for interactive proof, OCaml
for execution, and HTML and LaTeX for documentation.

In this talk, we discuss some of the motivation for Lem, the design
considerations in developing a pragmatic tool for `real-world
semantics engineering', and some of Lem's features.