@inproceedings{71cc3428911049aabdd687c97f5301a6,
title = "Who: A verifier for effectful higher-order programs",
abstract = "We present Who, a tool for verifying effectful higher-order functions. It features Effect polymorphism, higher-order logic and the possibility to reason about state in the logic, which enable highly modular specifications of generic code. Several small examples and a larger case study demonstrate its usefulness. The Who tool is intended to be used as an intermediate language for verification tools targeting ML-like programming languages.",
keywords = "Higher-order programs, Hoare logic",
author = "Johannes Kanig and Filli{\^a}tre, \{Jean Christophe\}",
year = "2009",
month = nov,
day = "30",
language = "English",
isbn = "9781605585093",
series = "ML'09 - Proceedings of the 2009 ACM SIGPLAN Workshop on ML",
pages = "39--48",
booktitle = "ML'09 - Proceedings of the 2009 ACM SIGPLAN Workshop on ML",
note = "2009 ACM SIGPLAN Workshop on ML, ML'09 ; Conference date: 30-08-2009 Through 30-08-2009",
}