Cakeml, a verified implementation of ML. (English) Zbl 1284.68405

Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Owens, Scott

Proceedings of the 41st ACM SIGPLAN-SIGACT symposium on principles of programming languages, POPL ’14, San Diego, CA, USA, January 22–24, 2014. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-2544-8). 179-191 (2014).

MSC:

68Q60	Specification and verification (program logics, model checking, etc.)
68N30	Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)
68N20	Theory of compilers and interpreters

Keywords:

ML; compiler bootstrapping; compiler verification; machine code verification; read-eval-print loop; verified garbage collection; verified parsing; verified type checking

Software:

CakeML; HOL