P. Borras, D. Clement, T. Despeyroux, and J. Incerpi, Centaur : the system, INRIA, 1987.
DOI : 10.1145/64137.65005

URL : https://hal.archives-ouvertes.fr/inria-00075774

M. Becerril, Impl ementation en langage parall ele Pompc d'algorithmes de segmentation co, ETCA/CREA-SP, 1992.

L. Boug and J. Levaire, Control structures for data-parallel SIMD languages: semantics and implementation, FGCS, vol.8, pp.363-378, 1992.

P. Bonnin, M ethode syst ematique de conception et de r ealisation d'applications en vision par ordinateur, 1991.

L. Boug, On the semantics of languages for massively parallel architectures, 1990.

L. Boug, The Data-Parallel Programming Model : a Semantic Perspective, 1992.

S. A. Cook, Soundness and Completeness of an Axiom System for Program Veriication, SIAM J. COMPUT, vol.7, issue.1, 1978.
DOI : 10.1137/0207005

URL : http://www.cs.toronto.edu/%7Esacook/homepage/soundness.pdf

P. Cousot, Formal Models And Semantics, v olume B of Handbook of Theoretical Computer Science, c hapter 15, pp.842-993, 1990.

E. W. Dijkstra, A Discipline of Programming, 1976.

J. Gabarrr and R. Gavaldd, An approach to correctness of data parallel algorithms, 1989.

M. J. Gordon, HOL : A proof generating system for higher order logic, VLSI Speciication, 1988.
DOI : 10.1007/978-1-4613-2007-4_3

M. J. Gordon, Mechanizing programming logics in higher order logic, Current Trends in Hardware V eriication and Automated Theorem Proving. K l u wer, 1988.
DOI : 10.1007/978-1-4612-3658-0_10

URL : http://www.cl.cam.ac.uk/users/mjcg/Banffpaper.pdf

M. J. Gordon, Programming Language Theory and its Implementation, 1989.

D. Gries, The Science o f P r ogramming. T ext and Monographs in Computer Science, 1987.

Y. , L. Guyadec, and B. Virot, S emantique axiomatique et automatisation de la preuve d e s programmes data-parall eles, 1993.

W. L. Harrison, K. N. Levitt, and M. Archer, A HOL mechanization of the axiomatic semantics of a simple distributed programming language, Proc. of the HOL'92 Conference M e eting, 1992.

, High Performance Fortran language speciication (draft version). Version 1.0 Draft, CITI/CRPC, Rice Univ, 1993.

J. L. Levaire, Using the centaur system to design SIMD parallel languages and programming environments, Proc. of the ESOP'92 Conference, pp.1-9
DOI : 10.1007/3-540-55253-7_20

URL : https://link.springer.com/content/pdf/10.1007%2F3-540-55253-7_20.pdf

P. Naur, Proof of algorithms by general snapshots, BIT, vol.6, pp.310-316, 1966.
DOI : 10.1007/978-94-011-1793-7_3

A. Stewart, An axiomatic treatment of SIMD assignment. Bit, vol.30, pp.70-82, 1990.
DOI : 10.1007/bf01932133

L. Th-ery, Y. Bertot, and G. Kahn, Real theorem provers deserve real user-interfaces, INRIA, 1992.

G. Utard, Un syst eme axiomatique pour les langages massivement parall ele SIMD, 1991.