Lem: Reusable engineering of real-world semantics

Dominic P. Mulligan, Scott Owens, Kathryn E. Gray, Tom Ridge, Peter Sewell
[doi] [ISBN] [Google Scholar] [DBLP] [Citeseer] [url]

Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming
ICFP '14
Gothenburg, Sweden
Association for Computing Machinery
New York, NY, USA
Pages 175-188
Note(s): Coq theorem prover, Isabelle theorem prover