Lem swMATH ID: 9395 Software Authors: Mulligan, Dominic P.; Owens, Scott; Gray, Kathryn E.; Ridge, Tom; Sewell, Peter Description: Lem reusable engineering of real-world semantics. Recent years have seen remarkable successes in rigorous engineering: using mathematically rigorous semantic models (not just idealised calculi) of real-world processors, programming languages, protocols, and security mechanisms, for testing, proof, analysis, and design. Building these models is challenging, requiring experimentation, dialogue with vendors or standards bodies, and validation; their scale adds engineering issues akin to those of programming to the task of writing clear and usable mathematics. But language and tool support for specification is lacking. Proof assistants can be used but bring their own difficulties, and a model produced in one, perhaps requiring many person-years effort and maintained over an extended period, cannot be used by those familiar with another. We introduce Lem, a language for engineering reusable large-scale semantic models. The Lem design takes inspiration both from functional programming languages and from proof assistants, and Lem definitions are translatable into OCaml for testing, Coq, HOL4, and Isabelle/HOL for proof, and LaTeX and HTML for presentation. This requires a delicate balance of expressiveness, careful library design, and implementation of transformations - akin to compilation, but subject to the constraint of producing usable and human-readable code for each target. Lem’s effectiveness is demonstrated by its use in practice. Homepage: http://link.springer.com/chapter/10.1007/978-3-642-22863-6_27 Related Software: Isabelle/HOL; Coq; ACL2; HOL Light; HOL; Ott; Isabelle; TSL; K Prover; TSOTool; CompCert; CoqJVM; LaTeX; Haskabelle; CakeML; OCaml; Twelf; Nitpick Cited in: 3 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Lem: reusable engineering of real-world semantics. Zbl 1346.68123Mulligan, Dominic P.; Owens, Scott; Gray, Kathryn E.; Ridge, Tom; Sewell, Peter 2014 all top 5 Cited by 13 Authors 2 Owens, Scott 2 Sewell, Peter 1 Böhm, Peter 1 Dong, JinSong 1 Gray, Kathryn E. 1 Hoa, Koh Chuen 1 Hou, Zhe 1 Liu, Yang 1 Mulligan, Dominic P. 1 Ridge, Thomas 1 Sanán, David 1 Tiu, Alwen Fernanto 1 Zappa Nardelli, Francesco Cited in 1 Serial 1 Journal of Automated Reasoning Cited in 1 Field 3 Computer science (68-XX) Citations by Year