Verifying Fast and Sparse SSA-based Optimizations in Coq.

Delphine Demange; David Pichardie; Léo Stefanesco

Accueil
Déposer
Consulter tout HAL
Publications Inria
Recherche
Services
Documentation
OpenAccess
- Inria soutient la science ouverte

Verifying Fast and Sparse SSA-based Optimizations in Coq.

Delphine Demange ¹ David Pichardie ¹ Léo Stefanesco ²

1 CELTIQUE - Software certification with semantic analysis

Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL

2 ENS Lyon - École normale supérieure - Lyon

Delphine Demange ¹ AuthorId : 832925

Auteur Etablissement employeur : University of Pennsylvania [Philadelphia] IdHAL : delphinedemange

David Pichardie ¹ AuthorId : 962464

Auteur IdHAL : david-pichardie

Léo Stefanesco ² AuthorId : 1122353

Auteur Etablissement employeur : École normale supérieure - Lyon IdHAL : leo-stefanesco ORCID : https://orcid.org/0000-0002-4719-2922

1 CELTIQUE - Software certification with semantic analysis (Campus de Beaulieu 35042 Rennes cedex - France) StructId : 88187

Inria Rennes – Bretagne Atlantique (Campus de beaulieu 35042 Rennes cedex - France) StructId : 419153
- Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France) StructId : 300009
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL (France) StructId : 419365
- IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires (Avenue du général Leclerc Campus de Beaulieu 35042 RENNES CEDEX - France) StructId : 105128
  - UR1 - Université de Rennes 1 (2 rue du Thabor - CS 46510 - 35065 Rennes cedex - France) StructId : 105160
    - UNIV-RENNES - Université de Rennes (France) StructId : 528860
  - INSA Rennes - Institut National des Sciences Appliquées - Rennes (20, avenue des Buttes de Coësmes - CS 70839 - 35708 Rennes cedex 7 - France) StructId : 117606
    - INSA - Institut National des Sciences Appliquées (France) StructId : 301232
    - UNIV-RENNES - Université de Rennes (France) StructId : 528860
  - UBS - Université de Bretagne Sud (BP 92116 - 56321 Lorient cedex - France) StructId : 172265
  - ENS Rennes - École normale supérieure - Rennes (Campus de Ker Lann - avenue Robert Schuman - 35170 Bruz - France) StructId : 247362
  - Inria - Institut National de Recherche en Informatique et en Automatique (Domaine de Voluceau Rocquencourt - BP 105 78153 Le Chesnay Cedex - France) StructId : 300009
  - Télécom Bretagne (Technopôle Brest-Iroise CS 83818 29238 BREST Cedex 3 - France) StructId : 301262
  - CentraleSupélec (3, rue Joliot Curie, Plateau de Moulon, 91192 GIF-SUR-YVETTE Cedex - France) StructId : 411575
  - CNRS - Centre National de la Recherche Scientifique : UMR6074 (France) StructId : 441569

2 ENS Lyon - École normale supérieure - Lyon (15 parvis René Descartes - BP 7000 - 69342 Lyon Cedex 07 - France) StructId : 6818

Type de document :

Communication dans un congrès

24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom. 2015

Domaine :

Sciences cognitives / Informatique

Liste complète des métadonnées

https://hal.inria.fr/hal-01110779
Contributeur : Delphine Demange <>
Soumis le : mercredi 28 janvier 2015 - 21:53:28
Dernière modification le : mardi 20 novembre 2018 - 17:42:48

Identifiants

HAL Id : hal-01110779, version 1

Collections

Citation

Delphine Demange, David Pichardie, Léo Stefanesco. Verifying Fast and Sparse SSA-based Optimizations in Coq.. 24th International Conference on Compiler Construction, CC 2015, 2015, London, United Kingdom. 2015. 〈hal-01110779〉

Verifying Fast and Sparse SSA-based Optimizations in Coq.

Identifiants

Collections

Citation

Exporter

Métriques

1027

Contact

Verifying Fast and Sparse SSA-based Optimizations in Coq.

Identifiants

Collections

Citation

Exporter

Partager

Métriques

1027

Contact