Powerlists in Coq: Programming and Reasoning

Frédéric Loulergue 1, * Virginia Niculescu Simon Robillard 2
* Auteur correspondant
1 PaMDA
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans
Abstract : For parallel programs, correctness by construction is an essential feature since debugging is almost impossible. Building correct programs by construction is not a simple task, and usually the methodologies used for this purpose are rather theoretical and based on a pen-and-paper style. A better approach could be based on tools and theories that allow a user to develop an efficient parallel application by easily implementing simple programs satisfying conditions, ideally automatically proved. Powerlists theory and its variants represent a good theoretical base for such an approach, and the Coq proof assistant is a tool that could be used for automatic proofs. The goal of this paper is to model the powerlist theory in Coq, and to use this modelling to program and reason about parallel programs in Coq. This represents the first step in building a framework to ease the development of correct and verifiable parallel programs.
Type de document :
Communication dans un congrès
First International Symposium on Computing and Networking (CANDAR), 2013, Fukuoka, Japan. IEEE, 2013, CANDAR
Liste complète des métadonnées

https://hal.inria.fr/hal-00864818
Contributeur : Frédéric Loulergue <>
Soumis le : lundi 23 septembre 2013 - 12:36:42
Dernière modification le : lundi 19 janvier 2015 - 17:05:47

Identifiants

  • HAL Id : hal-00864818, version 1

Collections

Citation

Frédéric Loulergue, Virginia Niculescu, Simon Robillard. Powerlists in Coq: Programming and Reasoning. First International Symposium on Computing and Networking (CANDAR), 2013, Fukuoka, Japan. IEEE, 2013, CANDAR. 〈hal-00864818〉

Partager

Métriques

Consultations de la notice

99