Scope

thesis.bib

@@ -331,7 +331,7 @@
 }
 
 @article{LuksicP20,
-  author    = {Ziga Luksic and
+  author    = {{\v{Z}}iga Luk{\v{s}}i{\v{c}} and
                Matija Pretnar},
   title     = {Local algebraic effect theories},
   journal   = {J. Funct. Program.},
@@ -3475,4 +3475,12 @@
   pages     = {339--363},
   publisher = {Springer},
   year      = {2017}
+}
+
+# Žiga Lukšič's PhD thesis on local effect theories
+@phdthesis{Ziga20,
+  author    = {{\v{Z}}iga Luk{\v{s}}i{\v{c}}},
+  title     = {Applications of algebraic effect theories},
+  school    = {University of Ljubljana, Slovenia},
+  year      = {2020}
 }

thesis.tex

@@ -1617,21 +1617,43 @@ function under a handler that interprets at least $\Get$ and $\Put$.
 \dhil{Mention the importance of polymorphism in effect tracking}
 
 \section{Scope}
-Since the inception of effect handlers numerous variations and
-extensions of them have been proposed.  In this dissertation I am
-concerned only with \citeauthor{PlotkinP09}'s deep handlers, their
-shallow variation, and parameterised handlers which are a slight
-variation of deep handlers.
-
-\subsection{Some pointers to elsewhere}
+Summarised in one sentence this dissertation is about practical
+programming language designs for programming with effect handlers,
+their foundational implementation techniques, and implications for the
+expressive power of their host language.
+
+Numerous variations and extensions of effect handlers have been
+proposed since their inceptions.  In this dissertation I restrict my
+attention to \citeauthor{PlotkinP09}'s deep handlers, their shallow
+variation, and parameterised handlers which are a slight variation of
+deep handlers. In particular I work with free algebraic theories,
+which is to say my designs do not incorporate equational theories for
+effects. Furthermore, I frame my study in terms of simply-typed and
+polymorphic $\lambda$-calculi for which I give computational
+interpretations in terms of contextual operational semantics and
+realise using two foundational operational techniques: continuation
+passing style and abstract machine semantics. When it comes to
+expressivity studies there are multiple complementary notions of
+expressiveness available in the literature; in this dissertation I
+work with typed macro-expressiveness and type-respecting
+expressiveness notions.
+
+\subsection{Scope extrusion}
 The literature on effect handlers is rich, and my dissertation is but
 one of many on topics related to effect handlers. In this section I
 provide a few pointers to related work involving effect handlers that
 I will not otherwise discuss in this dissertation.
 
-Readers interested in the mathematical theory and original development
-of effect handlers should consult \citeauthor{Pretnar10}'s PhD
-dissertation~\cite{Pretnar10}.
+Readers interested in the mathematical foundations and original
+development of effect handlers should consult \citeauthor{Pretnar10}'s
+PhD dissertation~\cite{Pretnar10}.
+
+Most programming language treatments of algebraic effects and their
+handlers sideline equational theories, despite equational theories
+being an important part of the original treatment of effect
+handlers. \citeauthor{Ziga20}'s PhD dissertation brings equations back
+onto the pitch as \citet{Ziga20} develops a core calculus with a novel
+local notion of effect theories.
 
 Lexical effect handlers are a variation on \citeauthor{PlotkinP09}'s
 deep handlers, which provide a form of lexical scoping for effect
@@ -1639,7 +1661,7 @@ operations, thus statically binding them to their handlers.
 %
 \citeauthor{Geron19}'s PhD dissertation develops the mathematical
 theory of scoped effect operations, whilst \citet{WuSH14} and
-\citet{BiernackiPPS20} studies them from a programming perspective.
+\citet{BiernackiPPS20} study them from a programming perspective.
 
 To get a grasp of the reasoning principles for effect handlers,
 interested readers should consult \citeauthor{McLaughlin20}'s PhD
@@ -1652,20 +1674,25 @@ techniques for deep handlers due to \citet{BiernackiPPS18}.
 \citeauthor{Ahman17}'s PhD dissertation is relevant for readers
 interested in the integration of computational effects into dependent
 type theories~\cite{Ahman17}. \citeauthor{Ahman17} develops an
-intensional \citet{MartinLof84} style effectful dependent type theory
-equipped with a novel computational dependent type.
-
-Effect handlers were conceived in the realm of category theory to give
-an algebraic treatment of exception handling~\cite{PlotkinP09}. They
-were adopted early by functional programmers, who either added
-language-level support for effect handlers~
+intensional \citet{MartinLof84} style dependent type theory equipped
+with a novel computational dependent type, which makes it possible to
+treat type-dependency in the sequential composition of effectful
+computations uniformly.
+
+% Effect handlers were conceived in the realm of category theory to give
+% an algebraic treatment of exception handling~\cite{PlotkinP09}. They
+% were adopted early by functional programmers, who either added
+% language-level support for effect handlers~
+Functional programmers were early adopters of effect handlers. They
+either added language-level support for handlers~
 \cite{Hillerstrom15,DolanWSYM15,BiernackiPPS18,Leijen17,BauerP15,BrachthauserSO20a,LindleyMM17,Chiusano20}
 or embedded them in
 libraries~\cite{KiselyovSS13,KiselyovI15,KiselyovS16,KammarLO13,BrachthauserS17,Brady13,XieL20}. Thus
 functional perspectives on effect handlers are plentiful in the
-literature. Only a few has studied effect handlers outside the realm
-of functional programming: \citet{Brachthauser20} offers an
-object-oriented perspective on effect handlers; \citet{Saleh19}
+literature. There are only a a few takes on effect handlers outside
+functional programming: \citeauthor{Brachthauser20}'s PhD dissertation
+contains an object-oriented perspective on effect handlers in
+Java~\cite{Brachthauser20}; In \citeauthor{Saleh19}'s PhD dissertation
 provides a logic programming perspective via an effect handlers
 extension to Prolog; and \citet{Leijen17b} has an imperative take on
 effect handlers in C.