[ doc ] extra references, related work

doc/main.bib

@@ -1,3 +1,41 @@
+@incollection{kiselyov2012typed,
+  title={Typed tagless final interpreters},
+  author={Kiselyov, Oleg},
+  booktitle={Generic and Indexed Programming},
+  pages={130--174},
+  year={2012},
+  publisher={Springer}
+}
+@techreport{winiko1994deterministic,
+  title={Deterministic resource management for the linear logic programming language Lygon},
+  author={Winiko, Michael and Harland, James},
+  year={1994},
+  institution={Technical Report 94/23, Melbourne University}
+}
+@inproceedings{cervesato1996efficient,
+  title={Efficient resource management for linear logic proof search},
+  author={Cervesato, Iliano and Hodas, Joshua S and Pfenning, Frank},
+  booktitle={International Workshop on Extensions of Logic Programming},
+  pages={67--81},
+  year={1996},
+  organization={Springer}
+}
+@article{polakow2016embedding,
+  title={Embedding a full linear lambda calculus in Haskell},
+  author={Polakow, Jeff},
+  journal={ACM SIGPLAN Notices},
+  volume={50},
+  number={12},
+  pages={177--188},
+  year={2016},
+  publisher={ACM}
+}
+@inproceedings{rand17qwire,
+  title={QWIRE Practice: Formal Verification of Quantum Circuits in Coq},
+  booktitle={Quantum Physics and Logic},
+  year={2017},
+  author={Rand, Robert and Paykin, Jennifer and Zdancewic, Steve}
+}
 @book{mitchell1996foundations,
   title={Foundations for programming languages},
   author={Mitchell, John C},

doc/main.tex

@@ -1169,14 +1169,33 @@ \subsection{Completeness}
 be altered in a radical manner.
 
 
-
-
 %%%%%%%%%%%%%%%%%%
 %% RELATED WORK %%
 %%%%%%%%%%%%%%%%%%
 
 \section{Related Work}
 
+Rand, Paykin and Zdancewic's work on modelling quantum circuits in
+Coq~\cite{rand17qwire} necessarily includes a treatment of linearity
+as qbits cannot be duplicated. Their focus is mostly on the quantum
+aspect and they are happy relying on the Coq's scripting capabilities
+to cope with the traditional, extensional presentation.
+
+Polakow faced with the task of embedding a λ-linear calculus in
+Haskell~\cite{polakow2016embedding} used a typed-tagless
+approach~\cite{kiselyov2012typed} making the context of assumptions
+explicit as a parameter of the typeclass and using threading as a way
+to deal with rules which have multiple premisses.
+
+The proof search community has been confronted with the inefficiency
+of randomly splitting up the multiset of assumption when applying a
+tensor-introduction rule. In an effort to combat this non-determinism,
+they have introduced alternative sequent calculi returning
+leftovers~\cite{cervesato1996efficient, winiko1994deterministic}.
+However because they do not have to type a term living in a given
+context, they do not care about the structure of the context of
+assumptions: it is still modelled as a multiset.
+
 We have already mentioned McBride's work~\cite{mcbride2016got}
 on (as a first approximation: the setup is actually more general)
 a type theory with a \emph{dependent linear} function space as a