Add CCC page w/ proofs

dbp · Jun 21, 2019 · 6bb6f3d · 6bb6f3d
1 parent 3ae7c69
commit 6bb6f3d
Show file tree

Hide file tree

Showing 7 changed files with 131 additions and 1 deletion.
diff --git a/_site/courses/verifcomp/index.html b/_site/courses/verifcomp/index.html
@@ -20,7 +20,7 @@ <h2>Verified Compilers and Multi-Language Software</h2>
 <tbody>
 <tr class="odd">
 <td align="left">Course</td>
-<td>CS4910: Verified Compilers and Multi-Language Software</td>
+<td>CS4910 (CRN 17946): Verified Compilers and Multi-Language Software</td>
 </tr>
 <tr class="even">
 <td align="left">Semester</td>

diff --git a/_site/pubs/2019/ccc.pdf b/_site/pubs/2019/ccc.pdf
diff --git a/_site/pubs/2019/ccc/index.html b/_site/pubs/2019/ccc/index.html
@@ -0,0 +1,65 @@
+<!DOCTYPE html>
+<html>
+  <head>
+    <meta charset="UTF-8">
+    <title>The Next 700 Compiler Correctness Theorems (Functional Pearl).</title>
+    <style type="text/css">
+     html,body {
+       margin: 0;
+       padding: 0;
+       font-family: sans;
+     }
+
+     h1,h2,h3,h4 {
+       text-align: center;
+       font-weight: normal;
+     }
+     h1 {
+       font-size: 1.5em;
+     }
+     p {
+       max-width: 600px;
+       margin: 10px auto;
+       line-height: 1.4em;
+     }
+     .holder {
+       margin: 0 auto;
+       margin-bottom: 100px;
+       width: 800px;
+     }
+    </style>
+  </head>
+
+  <body>
+    <div class="holder">
+      <h1>The Next 700 Compiler Correctness Theorems (Functional Pearl).</h1>
+
+      <h3>Daniel Patterson and Amal Ahmed.</h3>
+
+      <h3><a href="/pubs/2019/ccc.pdf">paper</a> and <a href="/pubs/2019/ccc/proofs.zip">mechanized proofs</a>.</h3>
+
+      <p>Compiler correctness is an old problem, with results stretching back
+        beyond the last half-century. Founding the field, John McCarthy and James
+        Painter set out to build a "completely trustworthy compiler". And yet,
+        until quite recently, even despite truly impressive verification efforts,
+        the theorems being proved were only about the compilation of whole
+        programs, a theoretically quite appealing but practically unrealistic
+        simplification. For a compiler correctness theorem to assure complete
+        trust, the theorem must reflect the reality of how the compiler will be
+        used.</p>
+      <p>There has been much recent work on more realistic "compositional"
+        compiler correctness aimed at proving correct compilation of components
+        while supporting linking with components compiled from different
+        languages using different compilers. However, the variety of theorems,
+        stated in remarkably different ways, raises questions about what
+        researchers even mean by a "compiler is correct." In this pearl, we
+        develop a new framework with which to understand compiler correctness
+        theorems in the presence of linking, and apply it to understanding and
+        comparing this diversity of results. In doing so, not only are we better
+        able to assess their relative strengths and weaknesses, but gain insight
+        into what we as a community should expect from compiler correctness
+        theorems of the future.</p>
+
+    </div>
+  </body>
+</html>
diff --git a/_site/pubs/2019/ccc/proofs.zip b/_site/pubs/2019/ccc/proofs.zip
diff --git a/pubs/2019/ccc.pdf b/pubs/2019/ccc.pdf
diff --git a/pubs/2019/ccc/index.html b/pubs/2019/ccc/index.html
@@ -0,0 +1,65 @@
+<!DOCTYPE html>
+<html>
+  <head>
+    <meta charset="UTF-8">
+    <title>The Next 700 Compiler Correctness Theorems (Functional Pearl).</title>
+    <style type="text/css">
+     html,body {
+       margin: 0;
+       padding: 0;
+       font-family: sans;
+     }
+
+     h1,h2,h3,h4 {
+       text-align: center;
+       font-weight: normal;
+     }
+     h1 {
+       font-size: 1.5em;
+     }
+     p {
+       max-width: 600px;
+       margin: 10px auto;
+       line-height: 1.4em;
+     }
+     .holder {
+       margin: 0 auto;
+       margin-bottom: 100px;
+       width: 800px;
+     }
+    </style>
+  </head>
+
+  <body>
+    <div class="holder">
+      <h1>The Next 700 Compiler Correctness Theorems (Functional Pearl).</h1>
+
+      <h3>Daniel Patterson and Amal Ahmed.</h3>
+
+      <h3><a href="/pubs/2019/ccc.pdf">paper</a> and <a href="/pubs/2019/ccc/proofs.zip">mechanized proofs</a>.</h3>
+
+      <p>Compiler correctness is an old problem, with results stretching back
+        beyond the last half-century. Founding the field, John McCarthy and James
+        Painter set out to build a "completely trustworthy compiler". And yet,
+        until quite recently, even despite truly impressive verification efforts,
+        the theorems being proved were only about the compilation of whole
+        programs, a theoretically quite appealing but practically unrealistic
+        simplification. For a compiler correctness theorem to assure complete
+        trust, the theorem must reflect the reality of how the compiler will be
+        used.</p>
+      <p>There has been much recent work on more realistic "compositional"
+        compiler correctness aimed at proving correct compilation of components
+        while supporting linking with components compiled from different
+        languages using different compilers. However, the variety of theorems,
+        stated in remarkably different ways, raises questions about what
+        researchers even mean by a "compiler is correct." In this pearl, we
+        develop a new framework with which to understand compiler correctness
+        theorems in the presence of linking, and apply it to understanding and
+        comparing this diversity of results. In doing so, not only are we better
+        able to assess their relative strengths and weaknesses, but gain insight
+        into what we as a community should expect from compiler correctness
+        theorems of the future.</p>
+
+    </div>
+  </body>
+</html>
diff --git a/pubs/2019/ccc/proofs.zip b/pubs/2019/ccc/proofs.zip