Test

text/AppendixA.tex

@@ -3,7 +3,7 @@
 \chapter{Appendix A} 
 \label{ch:appendix} 
 
-This appendix gives full typing derivations for the examplespresented in Chapter~\ref{ch:applications},
+This appendix gives full typing derivations for the examples presented in Chapter~\ref{ch:applications},
 which demonstrate simple coeffect calculi for implicit parameters, liveness and data-flow.
 
 % --------------------------------------------------------------------------------------------------

text/Chapter01.tex

@@ -285,7 +285,7 @@ \subsection{Context awareness \#3: Confidentiality and provenance}
 In the security context, such marking of values (but at run-time) is called \emph{tainting} 
 \cite{app-tainting-sql}, but the technique is a special case of more general \emph{provenance}
 tracking \cite{app-provenance-future}. This can be useful when working with data in other contexts. 
-For example, data jounralsts might want to propagate meta-data about the quality and the 
+For example, data journalists might want to propagate meta-data about the quality and the 
 information source -- is the source trustworthy? Is the data up-to-date? Such meta-data could 
 propagate to the result and tell us important information about the calculated results.
 

text/Chapter02.tex

@@ -161,7 +161,7 @@ \section{Through language semantics}
 
 Another pathway to coeffects leads through the semantics of effectful and context-dependent 
 computations. In a pioneering work, Moggi \cite{monad-notions} showed that effects (including
-partiality, exceptions, non-determinism and I/O) can be modelled uisng the category theoretic
+partiality, exceptions, non-determinism and I/O) can be modelled using the category theoretic
 notion of \emph{monad}.
 
 When using monads, we distinguish effect-free values $\tau$ from programs, or 
@@ -473,7 +473,7 @@ \subsection{Context-dependent languages and meta-languages}
 Finally, Davies and Pfenning \cite{logic-modal-staged} consider staged computations and interpret 
 $\square \tau$ as a type of unevaluated expressions of type $\tau$ (with no free variables).
 
-In Contextual Modal Type Theory, the modality $\square$ is further annotated with the free variales
+In Contextual Modal Type Theory, the modality $\square$ is further annotated with the free variables
 of the (unevaluated) expression. We write $\square^{\cclrd{\Psi}} \tau$ for a type of expressions
 that requires a context $\Psi$. The type is a comonadic counterpart to \emph{indexed monads} used by 
 Wadler and Thiemann when linking monads and effect systems and, indeed, it gives rise to a language 
@@ -744,7 +744,7 @@ \section{Summary}
 of the discussed related work -- the remaining aspects as well as important technical details are
 covered throughout the thesis.
 
-The first pathway follows as a dualization of well-known effect systems. However, this is not simply 
+The first pathway follows as a dualisation of well-known effect systems. However, this is not simply 
 a syntactic transformation. As we further discuss in the next chapter, coeffect systems treat lambda 
 abstraction differently. The second pathway follows by extending comonadic semantics of context-dependent 
 computations with indexing and building a type system analogous to effect system from the ``marriage of 

text/Chapter03.tex

@@ -22,9 +22,9 @@ \chapter{Context-aware systems}
 \paragraph{Chapter structure and contributions}
 \begin{itemize}
 \item We start with a characterization of contextual properties. The Section~\ref{sec:applications-structure}
-  explains what is a \emph{coeffect} and constrasts it with a better known notion of 
+  explains what is a \emph{coeffect} and contrasts it with a better known notion of 
   \emph{effect}. It explains what is the nature of properties that can be tracked using 
-  coeffect systems presented in this theis.
+  coeffect systems presented in this thesis.
 
 \item We describe a number of simple calculi for tracking a wide range of contextual properties. 
   The systems are adapted from diverse sources (type systems, static analyses, logics) and apply to
@@ -37,7 +37,7 @@ \chapter{Context-aware systems}
   all systems presented here lets us develop unified coeffect calculi in the upcoming three chapters.
 
 \item In addition, the coeffect systems for tracking the number of accessed past values in 
-  data-flow languagges (Sections~\ref{sec:applications-flat-dataflow} and \ref{sec:applications-structural-dataflow})
+  data-flow languages (Sections~\ref{sec:applications-flat-dataflow} and \ref{sec:applications-structural-dataflow})
   presents novel results and can be used to optimize data-flow programs.
 \end{itemize}
 
@@ -65,7 +65,7 @@ \section{Structure of coeffect systems}
 When introducing coeffect systems in Section~\ref{sec:path-effects-coeff}, we related coeffect systems
 with effect systems. Effect systems track how a program affects the environment, or, in other words 
 capture some \emph{output impurity}. In contrast, coeffect systems track what a program requires from 
-the execution environment, or \emph{input impurity}.
+the execution envionment, or \emph{input impurity}.
 
 Effect systems generally use judgements of the form $\Gamma \vdash e : \tau \;\&\; \cclrd{\sigma}$, 
 associating effects $\sigma$ with the output type. We write coeffect 
@@ -219,7 +219,7 @@ \subsection{Scalars and vectors}
 \emph{single} result. An expression with $n$ free variables of types $\tau_i$ can be modelled by a function 
 $\tau_1 \times \ldots \times \tau_n \rightarrow \tau$ with a product on the left, but a single value
 on the right. In both effect systems and coeffect systems, we \emph{write} the annotation as part of
-the function arrow. However, in the underlyng categorical model, effects are attached to the result
+the function arrow. However, in the underlying categorical model, effects are attached to the result
 $\tau$, while coeffects are attached to the context $\tau_1 \times \ldots \times \tau_n$.
 
 Structural coeffects have one coeffect annotation per each variable. Thus, the annotation consists
@@ -615,7 +615,7 @@ \subsection{Implicit parameters and type classes}
 from implicit parameters. The usual monadic semantics models fully dynamic scoping, while implicit
 parameters combine lexical and dynamic scoping.
 
-When using the usualmonadic semantics based on the reader monad, the semantics of the (\emph{abs})
+When using the usual monadic semantics based on the reader monad, the semantics of the (\emph{abs})
 rule would be modified as follows:
 %
 \begin{equation*}
@@ -691,7 +691,7 @@ \subsection{Implicit parameters and type classes}
 parts of context (implicit parameter dictionaries) that are provided by the call site and 
 declaration site. 
 
-%---------------------------------------------------------------------------------------------------
+%----------------------------------------------------------------------------------------------------
 
 \subsection{Distributed computing}
 \label{sec:applications-flat-distr}
@@ -2685,7 +2685,7 @@ \subsection{Security, tainting and provenance}
 The systems work in the same way as the examples discussed already. For example, consider the
 tainting example with the \ident{query} function calling an SQL database. To capture such 
 tainting, we annotate variables with $\cclrd{\ident{T}}$ for \emph{tainted} and with 
-$\cclrd{\ident{U}}$ for \emph{untainted}. Accessing a variable marks it as untained,
+$\cclrd{\ident{U}}$ for \emph{untainted}. Accessing a variable marks it as untainted,
 but using an expression that depends on some variable in certain dangerous contexts -- such 
 as in arguments of \ident{query} -- does introduce a taint on all the variables contributing to
 the expression. This is captured using the standard application rule (\emph{app}):
@@ -2836,7 +2836,7 @@ \section{Summary}
 languages and systems that include some notion of \emph{context}. Because there was no well-known
 abstraction capturing contextual properties, the languages use a wide range of formalisms -- including
 principled approaches based on comonads and modal S4, ad-hoc type system extensions and static analyses 
-as well as approaches based on monads. We looked at a number of applications inclding Haskell's implicit 
+as well as approaches based on monads. We looked at a number of applications including Haskell's implicit 
 parameters and type classes, data-flow languages such as Lucid, liveness analysis and also a number of 
 security properties. 
 

text/Chapter04.tex

@@ -84,7 +84,7 @@ \subsection{Related work}
 The development in this chapter can be seen as a counterpart to the well-known development of 
 \emph{effect systems} \cite{effects-gifford} and the use of \emph{monads} \cite{monad-notions}
 in programming languages. The syntax and type system of the flat coeffect calculus follows 
-asimilar style as effect systems \cite{effects-polymorphic,effects-talpin-et-al}, but differs
+a similar style as effect systems \cite{effects-polymorphic,effects-talpin-et-al}, but differs
 in the structure, as explained in the previous chapter, most importantly in lambda abstraction
 (the relationship with monads is further discussed in Section~\ref{sec:flat-related}).
 
@@ -94,7 +94,7 @@ \subsection{Related work}
 relates effectful functions $\tau_1 \xrightarrow{\sigma} \tau_2$ to monadic computations 
 $\tau_1 \rightarrow M^\sigma \tau_2$. In this chapter, we show a similar correspondence between 
 \emph{coeffect systems} and \emph{comonads}. However, due to the asymmetry of $\lambda$-calculus, 
-defining the semantics in terms of comonadic computations is not a simple mechanical dualization
+defining the semantics in terms of comonadic computations is not a simple mechanical dualisation
 of the work on effect systems and monads.
 
 The main purpose of the comonadic semantics presented in this chapter is to provide a motivation 
@@ -883,7 +883,7 @@ \subsection{Generalising to indexed comonads}
 \subsection{Flat indexed comonads}
 \label{sec:flat-semantics-monoidal}
 
-Because of the assymmetry of $\lambda$-calculus (discussed in Section~\ref{sec:applications-structure}),
+Because of the asymmetry of $\lambda$-calculus (discussed in Section~\ref{sec:applications-structure}),
 the duality between monads and comonads can no longer help us with defining the additional structure
 required to model full $\lambda$-calculus. In comonadic computations, additional information is attached
 to the context. In application and lambda abstraction, the context is propagated differently than 
@@ -928,7 +928,7 @@ \subsection{Flat indexed comonads}
 
 \noindent
 The $\ident{merge}_{\cclrd{r},\cclrd{s}}$ operation is the most interesting one. Given two comonadic
-values with additional contexts specified by $\cclrd{r}$ and $\cclrd{s}$, it combineds them into a 
+values with additional contexts specified by $\cclrd{r}$ and $\cclrd{s}$, it combines them into a 
 single value with additional context $\cclrd{r}\,\czip\,\cclrd{s}$. The $\czip$ operation often represents
 \emph{greatest lower bound}\footnote{The $\czip$ and $\cpar$ operations are the greatest and least upper 
 bounds in the liveness and data-flow examples, but not for implicit parameters. However, they remain useful 
@@ -1421,7 +1421,7 @@ \subsection{Syntactic properties}
 %
 The \kvd{glet} construct provides a way of sequentialising the context-require\-ments so
 that they can be discharged by matching constructs providing the required context. As discussed
-tfearlier, we focus on the general case and so we discuss when a flat coeffect calculus supports
+earlier, we focus on the general case and so we discuss when a flat coeffect calculus supports
 this form of evaluation (rather than looking at semantics for concrete systems).
 
 \paragraph{Local soundness and completeness.}
@@ -1567,7 +1567,7 @@ \subsection{Call-by-name evaluation}
 this affects the coeffects attached both to the function type and the overall context. 
 
 Semantically, the coeffect over-approximates the actual requirements -- at run-time, the code does not 
-actually access a previous value of the argument $x$. This cannot be caputred by a flat coeffect 
+actually access a previous value of the argument $x$. This cannot be captured by a flat coeffect 
 system, but it can be captured using the structural system discussed in Chapter~\ref{ch:structural}. 
 
 \paragraph{Implicit parameters.} In data-flow, there is no typing for the resulting expression that
@@ -1621,7 +1621,7 @@ \subsection{Call-by-name evaluation}
 
 \begin{lemma}[Top-pointed substitution]
 \label{thm:cbn-substitution-top}
-In a top-pointed flat coeffect calculus with an aglebra $(\C, \cseq, \cpar, \czip, \cunit, \czero, \cleq)$,
+In a top-pointed flat coeffect calculus with an algebra $(\C, \cseq, \cpar, \czip, \cunit, \czero, \cleq)$,
 substituting an expression $e_s$ with arbitrary coeffects $\cclrd{s}$ for a variable $x$ in $e_r$ does
 not change the coeffects of $e_r$:
 %
@@ -2011,7 +2011,7 @@ \subsection{Subtyping for coeffects}
 \paragraph{Semantics.} We follow the same approach as in Section~\ref{sec:flat-semantics} and use
 categorical semantics to explain (and confirm) the design of the sub-typing rules. The semantics
 of a judgement $\sem{\tau <: \tau'}$ is a function $\sem{\tau} \rightarrow \sem{\tau'}$. 
-As shown in Figure~\ref{fig:flat-semantics-sub}, the seamntics of the sub-typing rule (\emph{typ}) 
+As shown in Figure~\ref{fig:flat-semantics-sub}, the semantics of the sub-typing rule (\emph{typ}) 
 then just composes the semantics of the original expression with the conversion produced by the 
 semantics of the sub-typing judgement.
 
@@ -2100,7 +2100,7 @@ \subsection{Properties of lambda abstraction}
 \end{remark}
 \begin{proof}
 The following derives the conclusion of (\emph{abs}) using (\emph{idabs}), sub-coeffecting, 
-sub-typing and the fact that the algebra is \emph{stricly oriented}:
+sub-typing and the fact that the algebra is \emph{strictly oriented}:
 
 \begin{equation*}
 \tyrule{typ}
@@ -2221,7 +2221,7 @@ \subsection{Language with pairs and unit}
 \end{theorem}
 \begin{proof}
 Follows from the fact that $(\C, \cpar, \czero)$ is a monoid and \ident{assoc}, $\pi_1$ and
-$\pi_2$ are pure functions (treated as contstants in the langauge).
+$\pi_2$ are pure functions (treated as constants in the language).
 \end{proof}
 
 \noindent
@@ -2290,7 +2290,7 @@ \subsection{When is coeffect a monad}
 Implicit parameters can be captured by a monad, but \emph{just} a monad is not enough.
 Lambda abstraction in effect systems does not provide a way of splitting the context
 requirements between declaration site and call site (or, semantically, combining the implicit 
-parameters available in the scope where the function is deined and those specified by the caller).
+parameters available in the scope where the function is defined and those specified by the caller).
 
 \paragraph{Categorical relationship.}
 Before looking at the necessary extensions, consider the two ways of modelling implicit 
@@ -2313,7 +2313,7 @@ \subsection{When is coeffect a monad}
 \begin{remark}
 Computations modelled as $\ctyp{\cclrd{r}}{\tau_1}\rightarrow\tau_2$ using the product comonad
 are isomorphic to computations modelled as $\tau_1\rightarrow\mtyp{\cclrd{r}}{\tau_2}$ using the
-reader monad via currying/uncurrying isomoprhism.
+reader monad via currying/uncurrying isomorphism.
 \end{remark}
 \begin{proof}
 The isomorphism is demonstrated by the following equation:
@@ -2375,7 +2375,7 @@ \subsection{When is coeffect a monad}
 %
 The operation reveals the difference between effects and coeffects -- intuitively, given a function
 with effects $\cclrd{r \cup s}$, it should execute the effects $\cclrd{r}$ when wrapping the 
-function, \emph{before} the function actually perforsm the effectful operation with the effects.
+function, \emph{before} the function actually performs the effectful operation with the effects.
 The remaining effects $\cclrd{s}$ are delayed as usual, while effects $\cclrd{r}$ are removed
 from the effect annotation of the body.
 
@@ -2441,7 +2441,7 @@ \section{Conclusions}
 
 This chapter presented the \emph{flat coeffect calculus} -- a unified system for tracking 
 \emph{whole-context} properties of computations, that is properties related to the 
-execution environment or the enitre context in which programs are executed.
+execution environment or the entire context in which programs are executed.
 This is the first of the three \emph{coeffect calculi} developed in this thesis.
 
 The flat coeffect calculus is parameterized by a \emph{flat coeffect algebra} that captures