Skip to Main content Skip to Navigation
New interface
Conference papers

Who: A Verifier for Effectful Higher-order Programs

Johannes Kanig 1 Jean-Christophe Filliâtre 2 
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
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.
Document type :
Conference papers
Complete list of metadata
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Thursday, January 17, 2013 - 4:47:04 PM
Last modification on : Sunday, June 26, 2022 - 11:57:50 AM
Long-term archiving on: : Thursday, April 18, 2013 - 4:01:54 AM


Files produced by the author(s)


  • HAL Id : hal-00777585, version 1



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⟩



Record views


Files downloads