From 0dc1a0c82c6f5d18f9508a9cf6b0b6a168d6ba79 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Tue, 1 Dec 2015 08:09:12 -0500
Subject: [PATCH] books/bookvolbib add Kenn13
Goal: Proving Axiom correct
@misc{Kenn13,
author = "Kennedy, Andrew and Benton, Nick and Jensen, Jonas B. and
Dagand, Pierre-Evariste",
title = "Coq: The world's best macro assembler?",
year = "2013",
url = "http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf",
paper = "Kenn13.pdf",
abstract =
"We describe a Coq formalization of a subset of the x86
architecture. One emphasis of the model is brevity: using dependent
types, type classes and notation we give the x86 semantics a makeover
that counters its reputation for baroqueness. We model bits, bytes,
and memory concretely using functions that can be computed inside Coq
itself; concrete representations are mapped across to mathematical
objects in the SSREFLECT library (naturals, and integers modulo 2n)
to prove theorems. Finally, we use notation to support conventional
assembly code syntax inside Coq, including lexically-scoped
labels. Ordinary Coq definitions serve as a powerful ``macro'' feature
for everything from simple conditionals and loops to stack-allocated
local variables and procedures with parameters. Assembly code can be
assembled within Coq, producing a sequence of hex bytes. The assembler
enjoys a correctness theorem relating machine code in memory to a
separation-logic formula suitable for program verification."
}
---
books/bookvolbib.pamphlet | 34 ++++++++++++++++++++++++++++++++++
changelog | 2 ++
patch | 31 ++++++++++++++++++++++++++++---
src/axiom-website/patches.html | 2 ++
4 files changed, 66 insertions(+), 3 deletions(-)
diff --git a/books/bookvolbib.pamphlet b/books/bookvolbib.pamphlet
index 43c4b9b..6420e1b 100644
--- a/books/bookvolbib.pamphlet
+++ b/books/bookvolbib.pamphlet
@@ -2613,6 +2613,40 @@ Kelsey, Tom; Martin, Ursula; Owre, Sam
\end{chunk}
+\index{Kennedy, Andrew}
+\index{Benton, Nick}
+\index{Jensen, Jonas B.}
+\index{Dagand, Pierre-Evariste}
+\begin{chunk}{axiom.bib}
+@misc{Kenn13,
+ author = "Kennedy, Andrew and Benton, Nick and Jensen, Jonas B. and
+ Dagand, Pierre-Evariste",
+ title = "Coq: The world's best macro assembler?",
+ year = "2013",
+ url = "http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf",
+ paper = "Kenn13.pdf",
+ abstract =
+ "We describe a Coq formalization of a subset of the x86
+ architecture. One emphasis of the model is brevity: using dependent
+ types, type classes and notation we give the x86 semantics a makeover
+ that counters its reputation for baroqueness. We model bits, bytes,
+ and memory concretely using functions that can be computed inside Coq
+ itself; concrete representations are mapped across to mathematical
+ objects in the SSREFLECT library (naturals, and integers modulo 2n)
+ to prove theorems. Finally, we use notation to support conventional
+ assembly code syntax inside Coq, including lexically-scoped
+ labels. Ordinary Coq definitions serve as a powerful ``macro'' feature
+ for everything from simple conditionals and loops to stack-allocated
+ local variables and procedures with parameters. Assembly code can be
+ assembled within Coq, producing a sequence of hex bytes. The assembler
+ enjoys a correctness theorem relating machine code in memory to a
+ separation-logic formula suitable for program verification."
+
+}
+
+\end{chunk}
+
+
\index{Krebbers, Robbert Jan}
\begin{chunk}{axiom.bib}
@phdthesis{Kreb15,
diff --git a/changelog b/changelog
index df8a9ae..76a490d 100644
--- a/changelog
+++ b/changelog
@@ -1,3 +1,5 @@
+20151201 tpd src/axiom-website/patches.html 20151201.01.tpd.patch
+20151201 tpd books/bookvolbib add Kenn13
20151130 tpd src/axiom-website/patches.html 20151130.05.tpd.patch
20151130 tpd books/bookvol11 remove aldor users guide page
20151130 tpd src/axiom-website/patches.html 20151130.04.tpd.patch
diff --git a/patch b/patch
index 6781f33..607d501 100644
--- a/patch
+++ b/patch
@@ -1,5 +1,30 @@
-books/bookvol11 remove aldor users guide page
+books/bookvolbib add Kenn13
-Goal: Axiom documentation
+Goal: Proving Axiom correct
+
+@misc{Kenn13,
+ author = "Kennedy, Andrew and Benton, Nick and Jensen, Jonas B. and
+ Dagand, Pierre-Evariste",
+ title = "Coq: The world's best macro assembler?",
+ year = "2013",
+ url = "http://research.microsoft.com/en-us/um/people/nick/coqasm.pdf",
+ paper = "Kenn13.pdf",
+ abstract =
+ "We describe a Coq formalization of a subset of the x86
+ architecture. One emphasis of the model is brevity: using dependent
+ types, type classes and notation we give the x86 semantics a makeover
+ that counters its reputation for baroqueness. We model bits, bytes,
+ and memory concretely using functions that can be computed inside Coq
+ itself; concrete representations are mapped across to mathematical
+ objects in the SSREFLECT library (naturals, and integers modulo 2n)
+ to prove theorems. Finally, we use notation to support conventional
+ assembly code syntax inside Coq, including lexically-scoped
+ labels. Ordinary Coq definitions serve as a powerful ``macro'' feature
+ for everything from simple conditionals and loops to stack-allocated
+ local variables and procedures with parameters. Assembly code can be
+ assembled within Coq, producing a sequence of hex bytes. The assembler
+ enjoys a correctness theorem relating machine code in memory to a
+ separation-logic formula suitable for program verification."
+
+}
-Axiom no longer supports Aldor.
diff --git a/src/axiom-website/patches.html b/src/axiom-website/patches.html
index 596cc70..dcb3b7c 100644
--- a/src/axiom-website/patches.html
+++ b/src/axiom-website/patches.html
@@ -5148,6 +5148,8 @@ books/Makefile add Jenks HTML to Axiom browser

books/bookvol10.4 add documentation for compiledFunction

20151130.05.tpd.patch
books/bookvol11 remove aldor users guide page

+20151201.01.tpd.patch
+books/bookvolbib add Kenn13

--
1.7.5.4