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.
Type de document :
Communication dans un congrès
ACM SIGPLAN Workshop on ML, Aug 2009, Edinburgh, United Kingdom. 2009
Liste complète des métadonnées

https://hal.inria.fr/hal-00777585
Contributeur : Claude Marché <>
Soumis le : jeudi 17 janvier 2013 - 16:47:04
Dernière modification le : jeudi 5 avril 2018 - 12:30:08
Document(s) archivé(s) le : jeudi 18 avril 2013 - 04:01:54

Fichier

wml09.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00777585, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

366

Téléchargements de fichiers

606