Lem: a lightweight tool for heavyweight semantics

DOI10.1007/978-3-642-22863-6_27MaRDI QIDQ3088021zbMATH OpenOpenAlexFDO

Authors Scott Owens, Peter Böhm, Francesco Zappa Nardelli, Peter Sewell

Publication date 17 August 2011

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-22863-6_27

Mathematics Subject Classification ID

Recommendations

• Lem: reusable engineering of real-world semantics
• Ott: Effective tool support for the working semanticist
• Ott, effective tool support for the working semanticist
• A Sound Semantics for OCaml light
• Theorem-proving support in programming language semantics

Cites work

• A Sound Semantics for OCaml light
• A trustworthy monadic formalization of the ARMv7 instruction set architecture
• Mathematizing C++ concurrency
• Ott: Effective tool support for the working semanticist
• Relaxed-memory concurrency and verified compilation
• Structural analysis of narratives with the Coq proof assistant

Cited in

(4)

• Lem: reusable engineering of real-world semantics
• scientific article; zbMATH DE number 2080923 (Why is no real title available?)
• Ott, effective tool support for the working semanticist
• LEMA

Describes a project that uses

Uses Software

• ACL2
• Coq
• Isabelle
• Nitpick
• Ott
• Isabelle/HOL
• HOL
• HOL Light
• Twelf
• Lem

This page was built for publication: Lem: a lightweight tool for heavyweight semantics

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