TY - GEN
T1 - Who
T2 - 2009 ACM SIGPLAN Workshop on ML, ML'09
AU - Kanig, Johannes
AU - Filliâtre, Jean Christophe
PY - 2009/8/30
Y1 - 2009/8/30
N2 - 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.
AB - 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.
KW - Higher-order programs
KW - Hoare logic
UR - https://www.scopus.com/pages/publications/70450231797
U2 - 10.1145/1596627.1596634
DO - 10.1145/1596627.1596634
M3 - Conference contribution
AN - SCOPUS:70450231797
SN - 9781605585093
T3 - ML'09 - Proceedings of the 2009 ACM SIGPLAN Workshop on ML
SP - 39
EP - 48
BT - ML'09 - Proceedings of the 2009 ACM SIGPLAN Workshop on ML
PB - Association for Computing Machinery (ACM)
Y2 - 30 August 2009 through 30 August 2009
ER -