Who: A Verifier for Effectful Higher-order Programs

Johannes Kanig (1) , Jean-Christophe Filliâtre (2)

1 PROVAL - Proof of Programs
2 LRI - Laboratoire de Recherche en Informatique

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.

Domaines: Logique en informatique [cs.LO]

Johannes Kanig, Jean-Christophe Filliâtre. Who: A Verifier for Effectful Higher-order Programs. ACM SIGPLAN Workshop on ML, Aug 2009, Edinburgh, United Kingdom. ⟨hal-00777585⟩