REMS lunch

Add to your list(s) Download to your calendar using vCal

• Dominic Mulligan (University of Cambridge)
• Wednesday 20 August 2014, 13:00-14:00
• SS03.

If you have a question about this talk, please contact Peter Sewell.

nonstandard room: SS03

Lem: real-world semantic engineering

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.

This is a practice talk for ICFP 2014 .

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• SS03
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.