### changeset 8:7ac7f922e78e

First cut at Intro done
author Adam Chlipala Mon, 01 Sep 2008 10:25:40 -0400 6cc7a8fd4a8c c2e8e9c20643 book/Makefile book/src/Intro.v 2 files changed, 23 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/book/Makefile	Mon Sep 01 10:00:09 2008 -0400
+++ b/book/Makefile	Mon Sep 01 10:25:40 2008 -0400
@@ -21,7 +21,7 @@
rm -f Makefile.coq .depend $(GLOBALS) \ latex/*.sty latex/cpdt.* -doc: latex/cpdt.dvi html +doc: latex/cpdt.dvi latex/cpdt.pdf html latex/cpdt.tex:$(VS)
cd src ; coqdoc --latex $(VS_DOC) \ @@ -31,6 +31,9 @@ latex/cpdt.dvi: latex/cpdt.tex cd latex ; latex cpdt ; latex cpdt +latex/cpdt.pdf: latex/cpdt.dvi + cd latex ; pdflatex cpdt + html:$(VS)
cd src ; coqdoc $(VS_DOC) -toc \ --glob-from ../$(GLOBALS) \
--- a/book/src/Intro.v	Mon Sep 01 10:00:09 2008 -0400
+++ b/book/src/Intro.v	Mon Sep 01 10:25:40 2008 -0400
@@ -138,3 +138,22 @@

A good portion of the book is about how to formalize programming languages, compilers, and proofs about them.  I depart significantly from today's most popular methodology for pencil-and-paper formalism among programming languages researchers.  There is no need to be familiar with operational semantics, preservation and progress theorems, or any of the material found in courses on programming language semantics but not in basic discrete math and logic courses.  I will use operational semantics very sparingly, and there will be no preservation or progress proofs.  Instead, I will use a style that seems to work much better in Coq, which can be given the fancy-sounding name %\textit{%#<i>#foundational type-theoretic semantics#</i>#%}% or the more populist name %\textit{%#<i>#semantics by definitional compilers#</i>#%}%.
*)
+
+
+(** * Using This Book *)
+
+(**
+This book is generated automatically from Coq source files using the wonderful coqdoc program.  The latest PDF version is available at:
+*)