From 2e1eedc4d3ec36c70eb591897d1851e2a9190294 Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Wed, 27 May 2020 15:54:55 +0200 Subject: link to the HAL preprint --- doc/index-kvx.html | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/index-kvx.html b/doc/index-kvx.html index ae01d2d6..1a206014 100644 --- a/doc/index-kvx.html +++ b/doc/index-kvx.html @@ -25,14 +25,18 @@ a:active {color : Red; text-decoration : underline; }

The CompCert verified compiler

Commented Coq development

Version 3.7, 2020-03-31

 -

PATCHED for the Kalray MPPA-KVX VLIW CORE

+

PATCHED for the Kalray MPPA-KVX VLIW CORE (2020-05-27)

Introduction

This web page is a patched version of the table of contents of the official CompCert documentation, as given on the CompCert Web site. The unmodified parts of this table appear in gray. - +
+
+ A high-level view of this backend of CompCert is provided by this HAL preprint of Six, Boulmé and Monniaux (2019): + Certified Compiler Backends for VLIW Processors (Highly Modular Postpass-Scheduling in the CompCert Certified Compiler). +

Table of contents

-- cgit