Merge pull request #36 from clarus/master

Cosmetic: README in MarkDown

1 files changed, 29 insertions, 0 deletions

diff --git a/README.md b/README.md
new file mode 100644
index 00000000..32b419a7
--- /dev/null
+++ b/README.md
@@ -0,0 +1,29 @@
+# CompCert
+The verified C compiler.
+
+## Overview
+The CompCert C verified compiler is a compiler for a large subset of the
+C programming language that generates code for the PowerPC, ARM and x86
+processors.
+
+The distinguishing feature of CompCert is that it has been formally
+verified using the Coq proof assistant: the generated assembly code is
+formally guaranteed to behave as prescribed by the semantics of the
+source C code.
+
+CompCert is an ongoing research project.  The present release is an
+advanced prototype intended for research, educational and evaluation
+purposes.
+
+For more information on CompCert (supported platforms, supported C
+features, installation instructions, using the compiler, etc), please
+refer to the [user's manual](http://compcert.inria.fr/man/).
+
+## Copyright
+The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007,
+2008, 2009, 2010, 2011, 2012, 2013, 2014 Institut National de Recherche en
+Informatique et en Automatique (INRIA).  It is distributed under the
+conditions stated in file `LICENSE`.
+
+## Contact
+The authors can be contacted by e-mail at compcert@yquem.inria.fr.