2009/12/30 by Emmanuel Polonowski, Polonowski, Emmanuel
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #Model-Driven Software Engineering Techniques
paper · doi:10.48550/arxiv.0912.5515
openalex publication_date 2009/12/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This document describes the implementation in SML of the LoopW language, an imperative language with higher-order procedural variables and non-local jumps equiped with a program logic. It includes the user manual along with some implementation notes and many examples of certified imperative programs. As a concluding example, we show the certification of an imperative program encoding shift/reset using callcc/throw and a global meta-continuation.