--- a/src/ProgLang.v	Thu Jul 26 16:22:57 2012 -0400
+++ b/src/ProgLang.v	Thu Jul 26 16:38:44 2012 -0400
@@ -17,7 +17,7 @@
 
 (** %\chapter{A Taste of Reasoning About Programming Language Syntax}% *)
 
-(** Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants.  Before proving the first theorem of this kind, it is necessary to choose a formal encoding of the informal notions of syntax, dealing with such issues as %\index{variable binding}%variable binding conventions.  I believe the pragmatic questions in this domain are far from settled and remain as important open research problems.  However, in this chapter, I will demonstrate two underused encoding approaches.  Note that I am not recommending either approach as a silver bullet!  Mileage will vary across concrete problems, and I expect there to be significant future advances in our knowledge of encoding techniques.  For a broader introduction to programming language formalization, using more elementary techniques, see %\emph{%#<a href="http://www.cis.upenn.edu/~bcpierce/sf/"><i>#Software Foundations#</i></a>#%}\footnote{\url{http://www.cis.upenn.edu/~bcpierce/sf/}}% by Pierce et al.
+(** Reasoning about the syntax and semantics of programming languages is a popular application of proof assistants.  Before proving the first theorem of this kind, it is necessary to choose a formal encoding of the informal notions of syntax, dealing with such issues as %\index{variable binding}%variable binding conventions.  I believe the pragmatic questions in this domain are far from settled and remain as important open research problems.  However, in this chapter, I will demonstrate two underused encoding approaches.  Note that I am not recommending either approach as a silver bullet!  Mileage will vary across concrete problems, and I expect there to be significant future advances in our knowledge of encoding techniques.  For a broader introduction to programming language formalization, using more elementary techniques, see %\emph{%{{http://www.cis.upenn.edu/~bcpierce/sf/}Software Foundations}%}% by Pierce et al.
 
    This chapter is also meant as a case study, bringing together what we have learned in the previous chapters.  We will see a concrete example of the importance of representation choices; translating mathematics from paper to Coq is not a deterministic process, and different creative choices can have big impacts.  We will also see dependent types and scripted proof automation in action, applied to solve a particular problem as well as possible, rather than to demonstrate new Coq concepts.
 
@@ -185,7 +185,7 @@
 
   (** The transformations we have tried so far have been straightforward because they do not have interesting effects on the variable binding structure of terms.  The dependent de Bruijn representation is called%\index{first-order syntax}% _first-order_ because it encodes variable identity explicitly; all such representations incur bookkeeping overheads in transformations that rearrange binding structure.
 
-     As an example of a tricky transformation, consider one that removes all uses of %``%#"#[let x = e1 in e2]#"#%''% by substituting [e1] for [x] in [e2].  We will implement the translation by pairing the %``%#"#compile-time#"#%''% typing environment with a %``%#"#run-time#"#%''% value environment or _substitution_, mapping each variable to a value to be substituted for it.  Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen.  To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation.  With dependent typing, lifting corresponds to weakening for typing judgments.
+     As an example of a tricky transformation, consider one that removes all uses of "[let x = e1 in e2]" by substituting [e1] for [x] in [e2].  We will implement the translation by pairing the "compile-time" typing environment with a "run-time" value environment or _substitution_, mapping each variable to a value to be substituted for it.  Such a substitute term may be placed within a program in a position with a larger typing environment than applied at the point where the substitute term was chosen.  To support such context transplantation, we need _lifting_, a standard de Bruijn indices operation.  With dependent typing, lifting corresponds to weakening for typing judgments.
 
      The fundamental goal of lifting is to add a new variable to a typing context, maintaining the validity of a term in the expanded context.  To express the operation of adding a type to a context, we use a helper function [insertAt]. *)
 
@@ -696,7 +696,7 @@
   
   (** ** Establishing Term Well-Formedness *)
 
-  (** Can there be values of type [Term t] that are not well-formed according to [Wf]?  We expect that Gallina satisfies key%\index{parametricity}% _parametricity_ %\cite{parametricity}% properties, which indicate how polymorphic types may only be inhabited by specific values.  We omit details of parametricity theorems here, but [forall t (E : Term t), Wf E] follows the flavor of such theorems.  One option would be to assert that fact as an axiom, %``%#"#proving#"#%''% that any output of any of our translations is well-formed.  We could even prove the soundness of the theorem on paper meta-theoretically, say by considering some particular model of CIC.
+  (** Can there be values of type [Term t] that are not well-formed according to [Wf]?  We expect that Gallina satisfies key%\index{parametricity}% _parametricity_ %\cite{parametricity}% properties, which indicate how polymorphic types may only be inhabited by specific values.  We omit details of parametricity theorems here, but [forall t (E : Term t), Wf E] follows the flavor of such theorems.  One option would be to assert that fact as an axiom, "proving" that any output of any of our translations is well-formed.  We could even prove the soundness of the theorem on paper meta-theoretically, say by considering some particular model of CIC.
 
      To be more cautious, we could prove [Wf] for every term that interests us, threading such proofs through all transformations.  Here is an example exercise of that kind, for [Unlet].