Lem: reusable engineering of real-world semantics

DOI10.1145/2628136.2628143MaRDI QIDQ2819676zbMATH OpenOpenAlexFDO

Authors Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, Peter Sewell

Publication date 29 September 2016

Published in Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2628136.2628143

zbMATH Keywords

Lemproof assistantsreal-world semanticsspecification languages

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Lem: a lightweight tool for heavyweight semantics
• Ott, effective tool support for the working semanticist
• Ott: Effective tool support for the working semanticist
• Semantics engineering with PLT Redex
• A Sound Semantics for OCaml light

Cited in

(8)

• An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model
• From specification to testing: semantics engineering for Lua 5.2
• Lem
• Lem: a lightweight tool for heavyweight semantics
• Semantics engineering with PLT Redex
• Ott, effective tool support for the working semanticist
• LEMA
• Verification-Led Smart Contracts

Describes a project that uses

Uses Software

• Coq
• Isabelle/HOL
• OCaml
• HOL Light
• CakeML
• Haskabelle
• LaTeX

This page was built for publication: Lem: reusable engineering of real-world semantics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2819676)