Lem: A Lightweight Tool for Heavyweight Semantics

DOI10.1007/978-3-642-22863-6_27zbMath1342.68300OpenAlexW1924116124MaRDI QIDQ3088021

Scott Owens, F. Zappa Nardelli, Peter Böhm, 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

Uses Software

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

Cites Work

• Structural Analysis of Narratives with the Coq Proof Assistant
• Ott: Effective tool support for the working semanticist
• Relaxed-memory concurrency and verified compilation
• Mathematizing C++ concurrency
• A Sound Semantics for OCaml light
• A Trustworthy Monadic Formalization of the ARMv7 Instruction Set Architecture

This page was built for publication: Lem: A Lightweight Tool for Heavyweight Semantics