BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:REMS lunch - Dominic Mulligan (University of Cambridge)
DTSTART:20140820T120000Z
DTEND:20140820T130000Z
UID:TALK53613@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:*Lem: real-world semantic engineering*\n\nRecent years have se
 en an increased interest in `real-world semantic engineering': the creatio
 n and use in computer-aided proof of substantial models of artefacts such 
 as memory models\, microprocessors and their ISAs\, programming language s
 emantics\, and so on.\n\nHowever\, 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 lan
 guage before being hand-ported\, perhaps with the aid of sed or Perl scrip
 ts\, into a theorem prover.\n\nAs a result of these practices we collectiv
 ely suffer from `theorem-prover lock-in' where models cannot be shared---w
 ithout substantial effort---amongst the different theorem prover communiti
 es\, mass repetition as the same artefacts are repeatedly specified and mo
 delled by different groups\, and a proliferation of incomplete and badly v
 alidated models.\n\nAs 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 r
 elations\, quantification\, and so on.  Models written in Lem may be extra
 cted to HOL4\, Isabelle/HOL and Coq for interactive proof\, OCaml for exec
 ution\, and HTML and LaTeX for documentation.\n\nIn 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.\n\nThis is a practice talk for ICFP 2014.
LOCATION:SS03
END:VEVENT
END:VCALENDAR