New chapter: ProgLang

Makefile

@@ -2,7 +2,7 @@ MODULES_NODOC := CpdtTactics MoreSpecif DepList
 MODULES_PROSE := Intro
 MODULES_CODE  := StackMachine InductiveTypes Predicates Coinductive Subset GeneralRec \
 	MoreDep DataStruct Equality Generic Universes LogicProg Match Reflection \
-	Large
+	Large ProgLang
 MODULES_DOC   := $(MODULES_PROSE) $(MODULES_CODE)
 MODULES       := $(MODULES_NODOC) $(MODULES_DOC)
 VS            := $(MODULES:%=src/%.v)

latex/cpdt.bib

@@ -325,3 +325,38 @@
   school = {LMU M\"unchen},
   year= {1993}
 }
+
+@article{BGB,
+ author = {Geoffrey Washburn and Stephanie Weirich},
+ title = {Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism},
+ journal = {J. Funct. Program.},
+ volume = {18},
+ number = {1},
+ year = {2008},
+ pages = {87--140},
+ publisher = {Cambridge University Press},
+ address = {New York, NY, USA},
+ }
+
+@InProceedings{PhoasICFP08,
+author = {Adam Chlipala},
+title = {Parametric Higher-Order Abstract Syntax for Mechanized Semantics},
+booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming},
+year = {2008},
+pages = {143--156}
+}
+
+@article{parametricity,
+ author = {Reynolds, J.C.},
+ year = {1983},
+ title = {Types, abstraction, and parametric polymorphism},
+ journal = {Information Processing},
+ pages = {513--523}
+}
+
+@InProceedings{CompilerPOPL10,
+author = {Adam Chlipala},
+title = {A Verified Compiler for an Impure Functional Language},
+booktitle = {Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
+year = {2010},
+}

latex/cpdt.tex

@@ -51,6 +51,7 @@ The license text is available at:
 \include{Match.v}
 \include{Reflection.v}
 \include{Large.v}
+\include{ProgLang.v}
 
 \clearpage
 \addcontentsline{toc}{chapter}{Bibliography}

src/Intro.v

@@ -247,6 +247,8 @@ Proof by Reflection & \texttt{Reflection.v} \\
 \hline
 Proving in the Large & \texttt{Large.v} \\
 \hline
+A Taste of Reasoning About Programming Language Syntax & \texttt{Large.v} \\
+\hline
 \end{tabular} \end{center}
 
 % *)

src/Large.v

-(* Copyright (c) 2009-2011, Adam Chlipala
+(* Copyright (c) 2009-2012, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -16,7 +16,9 @@ Set Implicit Arguments.
 (* end hide *)
 
 
-(** %\chapter{Proving in the Large}% *)
+(** %\part{The Big Picture}
+
+   \chapter{Proving in the Large}% *)
 
 (** It is somewhat unfortunate that the term %``%#"#theorem proving#"#%''% looks so much like the word %``%#"#theory.#"#%''%  Most researchers and practitioners in software assume that mechanized theorem proving is profoundly impractical.  Indeed, until recently, most advances in theorem proving for higher-order logics have been largely theoretical.  However, starting around the beginning of the 21st century, there was a surge in the use of proof assistants in serious verification efforts.  That line of work is still quite new, but I believe it is not too soon to distill some lessons on how to work effectively with large formal proofs.
 

src/toc.html

@@ -20,5 +20,6 @@
 <li><a href="Match.html">Proof Search in Ltac</a>
 <li><a href="Reflection.html">Proof by Reflection</a>
 <li><a href="Large.html">Proving in the Large</a>
+<li><a href="ProgLang.html">A Taste of Reasoning About Programming Language Syntax</a>
 
 </body></html>

staging/updates.rss

@@ -11,6 +11,14 @@
 <webMaster>adam@chlipala.net</webMaster>
 <docs>http://blogs.law.harvard.edu/tech/rss</docs>
 
+<item>
+        <title>New Chapter: "A Taste of Reasoning About Programming Language Syntax"</title>
+        <pubDate>Sun, 1 Apr 2012 14:58:20 EDT</pubDate>
+        <link>http://adam.chlipala.net/cpdt/</link>
+        <author>adamc@csail.mit.edu</author>
+        <description>This new chapter condenses and recasts some material from the old Part IV of CPDT.  I felt the level of detail I was giving was out of proportion to my certainty that the techniques I was demonstrating would make sense to use in 5 years, so I'm opting instead for a quick tour that is mostly meant to convey the moral that encoding choices matter (but also to introduce PHOAS).</description>
+</item>
+
 <item>
         <title>Update to work with Coq 8.4 beta (and keep working with 8.3pl2)</title>
         <pubDate>Thu, 29 Mar 2012 18:10:00 EDT</pubDate>