Some more fixes

Author: pSub

report/include/evaluation.tex

@@ -1,7 +1,7 @@
 \chapter{Evaluation}
 \label{cha:evaluation}
 In this chapter we present three type system specifications, discuss
-how the specification language effected the formulation of typing
+how the specification language affected the formulation of typing
 rules, and which optimization strategies are successful.
 \section{SytemF}
 \label{sec:sytemf}
@@ -10,7 +10,7 @@ \section{SytemF}
 ~\cite{Pierce:2002:TPL:509043}. The complete implementation can be
 found in Appendix~\ref{appendix:systemf}. There are three notable
 differences between the version in~\cite{Pierce:2002:TPL:509043} and
-our implementation, that we describe in the following.
+our implementation, which we will describe in the following.
 
 In~\cite{Pierce:2002:TPL:509043} term and type variable bindings are
 collected in a single context. We need two separate contexts, one for
@@ -24,13 +24,13 @@ \section{SytemF}
 \end{lstlisting}
 
 Context \code|TermBinding| is the term variable binding and associates
-identifier with types. \code|TypeBinding| binds type variables,
-because we have no notion of kinds in SystemF type variables are
-associated to nothing. In our implementation variable and type
-identifiers are build from the same set of identifiers.
+identifier with types. \code|TypeBinding| binds type variables. Type
+variables are associated to nothing because we have no notion of kinds
+in SystemF . In our implementation variable and type identifiers are
+build from the same set of identifiers.
 
 The typing judgment has to reflect that we have two
-contexts. Therefore our typing judgment is defined as follows.
+contexts. Therefore our typing judgment is defined as follows:
 
 \begin{lstlisting}[language=sltc]
 judgments
@@ -79,7 +79,7 @@ \section{SytemF}
 mechanism. However type substitution is implemented in the same
 fashion like in a functional programming language with pattern
 matching. Substitution is also implemented as a separate module and
-imported into the SystemF specification.
+then imported into the SystemF specification.
 
 \begin{lstlisting}[language=sltc]
 judgments
@@ -128,11 +128,13 @@ \section{Lambda-Calculus with Subtyping}
 in~\cite{Pierce:2002:TPL:509043}. The specification for this type
 system is divided into two modules. One module specifies the type
 system without subtyping and the other module extends the first module
-with subtyping. The implementation of the type system without differs
-in two aspects from the text book formalization. First, we have to
-implement the freshness condition explicitly, as in the previous
-section. Second, we have to model rules that talk about all elements
-of a record inductively. Formula~\ref{formula:record-typing} shows the
+with subtyping. The implementation of the type system without
+subtyping differs in two aspects from the text book
+formalization. First, we have to implement the freshness condition
+explicitly, as in the previous section. Second, we have to model rules
+that talk about all elements of a record inductively.
+
+Formula~\ref{formula:record-typing} shows the
 formalization of the record typing rule
 from~\cite{Pierce:2002:TPL:509043}. This rule says that a record is
 well-typed if all its elements are
@@ -147,7 +149,7 @@ \section{Lambda-Calculus with Subtyping}
 \label{formula:record-typing}
 \end{align}
 
-That quantification is not possible in our specification
+This quantification is not possible in our specification
 language. Therefore we model this condition inductively as shown in
 the following.
 
@@ -169,10 +171,10 @@ \section{Lambda-Calculus with Subtyping}
 Here we ensure with rule \code|step| that the first element is
 well-typed and the record without the first element is well
 typed. Rule \code|base| is the base case for this definition and
-assigns the empty record the empty type. Note that we support in
-contrast to~\cite{Pierce:2002:TPL:509043} the empty record. We
+assigns the empty record the empty record type. Note that we support
+in contrast to~\cite{Pierce:2002:TPL:509043} the empty record. We
 included the empty record in our definition to demonstrate a top rule
-for records in the subtyping module. We have implement the membership
+for records in the subtyping module. We have implemented the membership
 test for the projection typing rule \code|T-proj| in a similar way.
 
 The module implementing subtyping for this lambda calculus contains a
@@ -224,10 +226,10 @@ \section{Lambda-Calculus with Subtyping}
 \end{lstlisting}
 \end{minipage}
 
-The subtyping relations has further a rule that defines the empty
+The subtyping relations have a further rule that defines the empty
 record \code|{}| to be the top element of records, as well as rules
 for with and depth subtyping and permutation of record elements. In
-conclusion we could specify a variant of the simply typed lambda
+conclusion we can specify a variant of the simply typed lambda
 calculus with an intuitive subtyping relation and reduce the
 non-determinism in the type system.
 

report/include/formula-generation.tex

@@ -289,15 +289,15 @@ \section{Implementation}
 
 \section{Editor Support}
 It is possible to use automated theorem provers to type check
-conjectures from within the editor. For type checking using automated
+conjectures from within the editor. For type checking with automated
 theorem provers we transform the specification into first order
 formulas and create a file per conclusion, as described in the
 previous section. Then we call the automated theorem prover Vampire on
-for each resulting file and parse the results. For each conjecture we
-visualize in the editor whether the verification succeeded and provide
-in case of success the names of the used first-order formulas.
+each resulting file and parse the results. For each conjecture we
+visualize in the editor whether the verification succeeded and in case
+of success provide the names of the used first-order formulas.
 
-We provide also a consistency test for specifications. This check
+We contribute also a consistency test for specifications. This check
 attempts a proof of \code|1 = 0| with vampire using the first-order
 formulas generated from the specification. This method allows us to
 possibly find inconsistencies in the type system