Restructure and Cleanup Unify

Let statement and capture conversion introduction
Restructure. Add to Introduction and cleanup
2024-05-27 16:07:24 +02:00 · 2024-05-27 02:57:15 +02:00 · 2024-05-24 22:25:31 +02:00 · 2024-05-23 16:45:40 +02:00 · 2024-05-23 14:18:50 +02:00 · 2024-05-22 16:08:03 +02:00
20 changed files with 5463 additions and 3351 deletions
--- a/.gitignore
+++ b/.gitignore
@@ -0,0 +1,19 @@
 ## Core latex/pdflatex auxiliary files:
 *.aux
 *.lof
 *.log
 *.lot
 *.fls
 *.out
 *.toc
 *.fmt
 *.fot
 *.cb
 *.cb2
 .*.lb
 *.bbl
 *.bcf
 *.blg
 *-blx.aux
 *-blx.bib
 *.run.xml
--- a/TIforWildFJ.tex
+++ b/TIforWildFJ.tex
@@ -1,5 +1,5 @@
-\documentclass[a4paper,UKenglish,cleveref, autoref, thm-restate]{lipics-v2021}
+\documentclass{llncs}
 %This is a template for producing LIPIcs articles. 
 %See lipics-v2021-authors-guidelines.pdf for further information.
 %for A4 paper format use option "a4paper", for US-letter use option "letterpaper"
@@ -36,9 +36,11 @@
 \usepackage{cancel}
 \usepackage{tcolorbox}
 \usepackage{arydshln}
 \usepackage{dashbox}
 \input{prolog}
 \begin{document}
 \bibliographystyle{plainurl}% the mandatory bibstyle
 \title{Global Type Inference for Featherweight Java with Wildcards} %TODO Please add
@@ -53,16 +55,16 @@
 \authorrunning{A. Stadelmeier and M. Plümicke and P. Thiemann} %TODO mandatory. First: Use abbreviated first/middle names. Second (only in severe cases): Use first author plus 'et al.'
-\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
+%\Copyright{Andreas Stadelmeier and Martin Plümicke and Peter Thiemann} %TODO mandatory, please use full first names. LIPIcs license is "CC-BY";  http://creativecommons.org/licenses/by/3.0/
-\ccsdesc[500]{Software and its engineering~Language features}
+%\ccsdesc[500]{Software and its engineering~Language features}
 %\ccsdesc[300]{Software and its engineering~Syntax}
 \keywords{type inference, Java, subtyping, generics} %TODO mandatory; please add comma-separated list of keywords
-\category{} %optional, e.g. invited paper
+%\category{} %optional, e.g. invited paper
-\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
+%\relatedversion{} %optional, e.g. full version hosted on arXiv, HAL, or other respository/website
 %\relatedversiondetails[linktext={opt. text shown instead of the URL}, cite=DBLP:books/mk/GrayR93]{Classification (e.g. Full Version, Extended Version, Previous Version}{URL to related version} %linktext and cite are optional
 %\supplement{}%optional, e.g. related research data, source code, ... hosted on a repository like zenodo, figshare, GitHub, ...
@@ -76,21 +78,20 @@
-%Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %Editor-only macros:: begin (do not touch as author)%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\EventEditors{John Q. Open and Joan R. Access}
+% \EventEditors{John Q. Open and Joan R. Access}
-\EventNoEds{2}
+% \EventNoEds{2}
-\EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
+% \EventLongTitle{42nd Conference on Very Important Topics (CVIT 2016)}
-\EventShortTitle{CVIT 2016}
+% \EventShortTitle{CVIT 2016}
-\EventAcronym{CVIT}
+% \EventAcronym{CVIT}
-\EventYear{2016}
+% \EventYear{2016}
-\EventDate{December 24--27, 2016}
+% \EventDate{December 24--27, 2016}
-\EventLocation{Little Whinging, United Kingdom}
+% \EventLocation{Little Whinging, United Kingdom}
-\EventLogo{}
+% \EventLogo{}
-\SeriesVolume{42}
+% \SeriesVolume{42}
-\ArticleNo{23}
+% \ArticleNo{23}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{document}
 \maketitle
@@ -101,126 +102,7 @@ TODO: Abstract
 \input{introduction}
-%We could do a translation from Java to \wildFJ explaining implicit capture conversion
+%\input{letfjTransformation}
 \section{Soundness of Typing}
 We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
 A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
 \begin{figure}
 $\begin{array}{rcl}
    | \texttt{x} |
    & = & \texttt{x} \\
    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
    & = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
    & = & |\texttt{e}|.\texttt{f} \\
    | \texttt{e} \elvis{} \texttt{e} |
    & = & |\texttt{e}| \elvis{} |\texttt{e}| \\
 \end{array}$
 \caption{Erasure} \label{fig:erasure}
 \end{figure}
 % A constraint Pair<A,B> <. a, then a has infinite possibilities:
 % a =. X.Pair<X,X>
 % a =. X,Y.Pair<X,Y>
 % a =. X.Pair<Pair<X,X>,X>
 % a =. X,Y.Pair<Pair<X,Y>,X>
 % a =. X,Y.Pair<Pair<X,Y>,Y>
 % There is no way to try out every single one of them.
 Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
 We have a typed expression
 $|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
 $|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$ 
 $|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
 %TODO: write the transform rules:
 % |e.f, ret| = |e, r| let ret = r.f in
 % |x, ret| = let ret = x in
 % |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
 Erasure functions:
 $|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
 $\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
 $\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
 $\begin{array}{l}
 \texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\ 
 \hline
 \vspace*{-0.4cm}\\
 \texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
 \end{array}$
 Example:
 m(a, b) = a.m(b.f);
 let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
 % TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
 % |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e| 
 % |let xf : T = x1.f in e| = [x1.f/xf]|e|
 % |let xr : T = x in e| = [xr/x]|e|
 % |new C(x)| = new C(x)
 % | let xr : T' = x in let xf : T = xr.f | = x.f
 % let x : T' = e' in x = |e|
 % ---------------------------------
 % | let xr : T' = x in let xf : T = xr.f | = x.f
 % let x : T' = e' in x = |e|
 % -----------
 % = 
 We need a language which only has let statemnts and expressions on capture converted variables
 The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
 This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
 Free variables then can flow freely inside the method body.
 We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
 If there is a possible method type then there must exist a let configuration.
 % By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
 % TODO: Proof!
 The normal type placeholders represent denotable types.
 %TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
 % what about wildcards getting returned by untyped methods? they can also be captured
 % TODO: try soundness proof on the original type rules!
 Removing of extensive wildcards:
 $
 \wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
 \lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
 \wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
 \wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
 \wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
 \implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
 $
 %e.f leads to constraints: r <c C<x> with return type equals the field type T.
 %   T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
 %   X.C<X> <c C<x> -> then T contains X variables
 % let x1 = p1, x2 = p2 in
 %  let r1  = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
 %   in ret
 What about method invocation with no type yet. m2 :: a -> a 
 they are also encased in let expression so the return type can be capture converted.
 Those methods and the parameter types of the current method are the only things not typed.
 All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
 The return type of untyped methods has to be well-formed and cannot contain free variables.
 Therefore no free variables will flow into those types.
 \input{tRules}
@@ -228,172 +110,6 @@ Therefore no free variables will flow into those types.
 \input{constraints}
 \section{Capture Conversion}
 The input to our type inference algorithm does not contain let statements.
 Those are added after computing a type solution.
 Let statements act as capture conversion and only have to be applied in method calls involving wildcard types.
 \begin{figure} 
  \begin{minipage}{0.45\textwidth}
 \begin{lstlisting}[style=fgj]
 <X> List<X> clone(List<X> l);
 example(p){
  return clone(p);
 }
 \end{lstlisting}
    \end{minipage}%
    \hfill
    \begin{minipage}{0.5\textwidth}
 \begin{lstlisting}[style=tfgj]
 (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
  return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in
   clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
 }
 \end{lstlisting}
    \end{minipage}
 \caption{Type inference adding capture conversion}\label{fig:addingLetExample}
  \end{figure}
 Figure \ref{fig:addingLetExample} shows a let statement getting added to the typed output.
 The method \texttt{clone} cannot be called with the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
 After a capture conversion \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$ with $\rwildcard{X}$ being a free variable.
 Afterwards we have to find a supertype of $\exptype{List}{\rwildcard{X}}$, which does not contain free variables
 ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in this case).
 During the constraint generation step most types are not known yet and are represented by a type placeholder.
 During a methodcall like the one in the \texttt{example} method in figure \ref{fig:ccExample} the type of the parameter \texttt{p}
 is not known yet.
 The type \texttt{List<?>} would be one possibility as a parameter type for \texttt{p}.
 To make wildcards work for our type inference algorithm \unify{} has to apply capture conversions if necessary.
 The type placeholder $\tv{r}$ is the return type of the \texttt{example} method.
 One possible type solution is $\tv{p} \doteq \tv{r} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$,
 which leads to:
 \begin{verbatim}
 List<?> example(List<?> p){
  return clone(p);
 }
 \end{verbatim}
 But by substituting $\tv{p} \doteq \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ in the constraint
 $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ leads to
 $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{x}}$.
 To make this typing possible we have to introduce a capture conversion via a let statement:
 $\texttt{return}\ (\texttt{let}\ \texttt{x} : \wctype{\rwildcard{X}}{List}{\rwildcard{X}} = \texttt{p}\ \texttt{in} \
 \texttt{clone}\generics{\rwildcard{X}}(x) : \wctype{\rwildcard{X}}{List}{\rwildcard{X}})$
 Inside the let statement the variable \texttt{x} has the type $\exptype{List}{\rwildcard{X}}$
 $
 \begin{array}[c]{l}
 \wildcardEnv \vdash C \cup \set{\wtv{a} \doteq \rwildcard{G}}\\
                   \hline
 [\type{G}/\wtv{a}]\wildcardEnv \vdash [\type{G}/\wtv{a}]C  \cup \set{\tv{a} \doteq \type{G}} 
 \end{array}
 $
 This spawns additional problems.
 %TODO
 %we need the constraint set to be a list
 %not on every constraint CC is allowed. The unify algorithm does not know the context in which a constraint was generated
 %free type variables cannot leave the scope of the method call
 \begin{figure} 
 \begin{minipage}{0.45\textwidth}
 \begin{verbatim}
 <X> List<X> clone(List<X> l){...}
 example(p){
  return clone(p);
 }
 \end{verbatim}
  \end{minipage}%
  \hfill
  \begin{minipage}{0.35\textwidth}
 \begin{constraintset}
    \textbf{Constraints:}\\
    $
  \tv{p} \lessdot \exptype{List}{\wtv{x}}, \\
 \tv{p} \lessdot \tv{r}, \\
 \tv{p} \lessdot \type{Object}, 
 \tv{r} \lessdot \type{Object}
    $
 \end{constraintset}
  \end{minipage}
 \caption{Type inference example}\label{fig:ccExample}
 \end{figure}
 In addition with free variables this leads to unwanted behaviour.
 Take the constraint
 $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ for example.
 After a capture conversion from $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ to $\exptype{List}{\rwildcard{Y}}$ and a substitution $\wtv{a} \doteq \rwildcard{Y}$
 we get
 $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$.
 Which is correct if we apply capture conversion to the left side:
 $\exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
 If the input constraints did not intend for this constraint to undergo a capture conversion then \unify{} would produce an invalid
 type solution due to:
 $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \nless: \exptype{List}{\rwildcard{X}}$
 The reason for this is the \texttt{S-Exists} rule's premise
 $\text{dom}(\Delta') \cap \text{fv}(\exptype{List}{\rwildcard{X}}) = \emptyset$.
 Additionally free variables are not allowed to leave the scope of a capture conversion
 introduced by a let statement.
 %TODO we combat both of this with wildcard type placeholders (? flag)
 Type placeholders which are not flagged as possible free variables ($\wtv{a}$) can never hold a free variable or a type containing free variables.
 Constraint generation places these standard place holders at method return types and parameter types.
 \begin{lstlisting}[style=fgj]
 <X> List<X> clone(List<X> l);
 (*@$\red{\tv{r}}$@*) example((*@$\red{\tv{p}}$@*) p){
  return clone(p);
 }
 \end{lstlisting}
 This prevents type solutions that contain free variables in parameter and return types.
 When calling a method which already has a type annotation we have to consider adding a capture conversion in form of a let statement.
 The constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ signals the \unify{} algorithm that here a capture conversion is possible.
 $\sigma(\tv{p}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, \sigma(\tv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, $ is a possible solution.
 But only when adding a capture conversion:
 \begin{lstlisting}[style=fgj]
 <X> List<X> clone(List<X> l);
 (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) example((*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) p){
  return let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = p in clone(x) : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*);
 }
 \end{lstlisting}
 \unify{}'s type solution for constraints involving free variables only holds under special circumstances.
 Constraint $\tv{p} \lessdot \exptype{List}{\wtv{x}}$ only holds when a capture conversion is applied to the left side:
 $\Delta, \Delta' \vdash CC(\sigma(\tv{p})) <: \sigma(\exptype{List}{\wtv{x}})$
 and there is a an environment $\Delta'$ holding all type variables used inside the subtype relation.
 This is done by packing the method call inside a let statement, which performs a capture conversion on all expressions used as parameters.
 %TODO: Explain (do soundness and TYPE algorithm first)
 A type solution of the \unify{} algorithm only guarantees correct subtyping for constraints not containing free variables.
 Constraints like $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$ only guarantee
 $\Delta, \Delta' \vdash \sigma(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) <: \sigma(\exptype{List}{\wtv{a}})$ when
 adding a $\Delta'$ environment and applying a capture conversion on the left side.
 In this case the type solution would be $\tv{a} \to \rwildcard{X}$ leading to:
 $\Delta, \set{\rwildcard{X}} \vdash \exptype{List}{\rwildcard{X}} <: \exptype{List}{\rwildcard{X}}$
 This is the reason input constraints containing free variables cannot be stored in a set.
 $\wtv{a} \lessdot \wtv{b}$ is not the same as $\wtv{a} \lessdot \wtv{b}$.
 Both constraints will end up the same after a substitution for both placeholders $\tv{a}$ and $\tv{b}$.
 But afterwards a capture conversion is applied, which can generate different types on the left sides.
 \begin{itemize}
  \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Y}}$ 
  \item $\text{CC}(\wctype{\rwildcard{X}}{List}{\rwildcard{X}}) \implies \exptype{List}{\rwildcard{Z}}$ 
 \end{itemize}
 Also the subtype relation is not symmetric for types involving free type variables.
 $\type{T} \lessdot \type{S}$ and $\type{S} \lessdot \type{T}$ doesnt mean $\type{T} = \type{S}$, because we apply a capture conversion on every constraint.
 Only for constraints without free variables symmetry is given.
 % Can untyped methods also get a capture conversion? NO!
 %TODO: Explain why capture conversion is needed (also in respect to martins algorithm)
 \input{Unify}
 \section{Limitations}
@@ -430,6 +146,7 @@ class Example{
 \include{soundness}
 %\include{termination}
 \include{relatedwork}
 \bibliography{martin}
--- a/cc-by.pdf
+++ b/cc-by.pdf
--- a/conclusion.tex
+++ b/conclusion.tex
@@ -1,10 +1,132 @@
 \section{Properties of the Algorithm}
 \begin{itemize}
    \item Our algorithm is designed for extensibility with the final goal of full support for Java.
    \unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
    Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
 \end{itemize}
 %TODO: how are the challenges solved: Describe this in the last chapter with examples!
 \section{Soundness}\label{sec:soundness}
 \section{Completeness}\label{sec:completeness}
 The algorithm can find a solution to every program which the Unify by Plümicke finds
 a correct solution aswell.
 It will not infer intermediat type like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X},\rwildcard{X}}$.
 There is propably some loss of completeness when capture constraints get deleted.
 This happens because constraints of the form $\tv{a} \lessdotCC \exptype{C}{\wtv{x}}$ are kept as long as possible.
 Here the variable $\tv{a}$ maybe could hold a wildcard type,
 but it gets resolved to a $\generics{\type{A} \triangleleft \type{N}}$.
 This combined with a constraint $\type{N} \lessdot \wtv{x}$ looses a possible solution.
 This is our result:
 \begin{verbatim}
 class List<X> {
    <Y extends X> void addTo(List<Y> l){
        l.add(this.get());
    }
 }
 \end{verbatim}
 $
 \tv{l} \lessdotCC \exptype{List}{\wtv{y}},
 \type{X} \lessdot \wtv{y}
 $
 But the most general type would be:
 \begin{verbatim}
 class List<X> {
    void addTo(List<? super X> l){
        l.add(this.get());
    }
 }
 \end{verbatim}
 \subsection{Discussion Pair Example}
 \begin{verbatim}
 <X> Pair<X,X> make(List<X> l){ ... }
 <X> boolean compare(Pair<X,X> p) { ... }
 List<?> l;
 Pair<?,?> p;
 compare(make(l)); // Valid
 compare(p); // Error
 \end{verbatim}
 Our type inference algorithm is not able to solve this example.
 When we convert this to \TamedFJ{} and generate constraints we end up with:
 \begin{lstlisting}[style=tamedfj]
 let m = let x = l in make(x) in compare(m)
 \end{lstlisting}
 \begin{constraintset}$
 \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \ntv{x},
 \ntv{x} \lessdotCC \exptype{List}{\wtv{a}}
 \exptype{Pair}{\wtv{a}, \wtv{a}} \lessdot \ntv{m}, %% TODO: Mark this constraint
 \ntv{m} \lessdotCC \exptype{Pair}{\wtv{b}, \wtv{b}}
 $\end{constraintset}
 $\ntv{x}$ will get the type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ and
 from the constraint
 $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
 \unify{} deducts $\wtv{a} \doteq \rwildcard{X}$ leading to 
 $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}} \lessdot \ntv{m}$.
 Finding a supertype to $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ is the crucial part.
 The correct substition for $\ntv{m}$ would be $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$.
 But this leads to additional branching inside the \unify{} algorithm and increases runtime.
 %We refrain from using that type, because it is not denotable with Java syntax.
 %Types used for normal type placeholders should be expressable Java types. % They are not!
 The prefered way of dealing with this example in our opinion would be the addition of a multi-let statement to the syntax.
 \begin{lstlisting}[style=letfj]
 let x : (*@$\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$@*) = l, m = make(x) in compare(make(x))
 \end{lstlisting}
 We can make it work with a special rule in the \unify{}.
 But this will only help in this specific example and not generally solve the issue.
 A type $\exptype{Pair}{\rwildcard{X}, \rwildcard{X}}$ has atleast two immediate supertypes:
 $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ and
 $\wctype{\rwildcard{X}, \rwildcard{Y}}{Pair}{\rwildcard{X}, \rwildcard{Y}}$.
 Imagine a type $\exptype{Triple}{\rwildcard{X},\rwildcard{X},\rwildcard{X}}$ already has 
 % TODO: how many supertypes are there?
 %X.Triple<X,X,X> <: X,Y.Triple<X,Y,X> <: 
 %X,Y,Z.Triple<X,Y,Z>
 % TODO example:
 \begin{lstlisting}[style=java]
 <X> Triple<X,X,X> sameL(List<X> l)
 <X,Y> Triple<X,Y,Y> sameP(Pair<X,Y> l)
 <X,Y> void triple(Triple<X,Y,Y> tr){}
 Pair<?,?> p ...
 List<?> l ...
 make(t) { return t; }
 triple(make(sameP(p)));
 triple(make(sameL(l)));
 \end{lstlisting}
 \begin{constraintset}
 $
 \exptype{Triple}{\rwildcard{X}, \rwildcard{X}, \rwildcard{X}} \lessdot \ntv{t},
 \ntv{t} \lessdotCC \exptype{Triple}{\wtv{a}, \wtv{b}, \wtv{b}}, \\
 (\textit{This constraint is added later: } \exptype{Triple}{\rwildcard{X}, \rwildcard{Y}, \rwildcard{Y}} \lessdot \ntv{t})
 $
 % Triple<X,X,X> <. t
 % ( Triple<X,Y,Y> <. t ) <- this constraint is added later
 % t <. Triple<a?, b?, b?>
 % t =. x.Triple<X,X,X>
 \end{constraintset}
 \section{Conclusion and Further Work}
 % we solved the problems given in the introduction (see examples TODO give names to examples)
 The problems introduced in the openening \ref{challenges} can be solved via our \unify{} algorithm (see examples \ref{example1} and \ref{example2}).
 As you can see by the given examples our type inference algorithm can calculate
 type solutions for programs involving wildcards.
-Going further we try to proof soundness and completeness for \unify{}.
+Going further we try to prove soundness and completeness for \unify{}.
 % The tricks are:
--- a/constraints.tex
+++ b/constraints.tex
@@ -1,7 +1,71 @@
-\section{Constraint generation}\label{chapter:constraintGeneration}
+\subsection{Capture Constraints}
-% Our type inference algorithm is split into two parts.
+%TODO: General Capture Constraint explanation
 % A constraint generation step \textbf{TYPE} and a \unify{} step.
 Capture Constraints are bound to a variable.
 For example a let statement like \lstinline{let x = v in x.get()} will create the capture constraint
 $\tv{x} \lessdotCC_x \exptype{List}{\wtv{a}}$.
 This time we annotated the capture constraint with an $x$ to show its relation to the variable \texttt{x}.
 Let's do the same with the constraints generated by the \texttt{concat} method invocation in listing \ref{lst:faultyConcat},
 creating the constraints \ref{lst:sameConstraints}.
 \begin{figure}
  \begin{minipage}[t]{0.49\textwidth}
    \begin{lstlisting}[caption=Faulty Method Call,label=lst:faultyConcat]{tamedfj}
  List<?> v = ...;
  let x = v in 
      let y = v in
        concat(x, y) // Error!
    \end{lstlisting}\end{minipage}
    \hfill
    \begin{minipage}[t]{0.49\textwidth}
  \begin{lstlisting}[caption=Annotated constraints,mathescape=true,style=constraints,label=lst:sameConstraints]
  $\tv{x} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{x}$
  $\tv{y} \lessdotCC_\texttt{y} \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \tv{y}$
    \end{lstlisting}
    \end{minipage}
 \end{figure}
 During the \unify{} process it could happen that two syntactically equal capture constraints evolve,
 but they are not the same because they are each linked to a different let introduced variable.
 In this example this happens when we substitute $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\tv{x}$ and $\tv{y}$
 resulting in:
 %For example by substituting $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{x}]$ and $[\wctype{\rwildcard{X}}{List}{\rwildcard{X}}/\tv{y}]$:
 \begin{displaymath}
  \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_x \exptype{List}{\wtv{a}}, \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_y \exptype{List}{\wtv{a}}
 \end{displaymath}
 Thanks to the original annotations we can still see that those are different constraints.
 After \unify{} uses the \rulename{Capture} rule on those constraints
 it gets obvious that this constraint set is unsolvable:
 \begin{displaymath}
  \exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}},
 \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}
 \end{displaymath}
 %In this paper we do not annotate capture constraint with their source let statement.
 The rest of this paper will not annotate capture constraints with variable names.
 Instead we consider every capture constraint as distinct to other capture constraints even when syntactically the same,
 because we know that each of them originates from a different let statement.
 \textit{Hint:} An implementation of this algorithm has to consider that seemingly equal capture constraints are actually not the same
 and has to allow doubles in the constraint set.
 % %We see the equality relation on Capture constraints is not reflexive.
 % A capture constraint is never equal to another capture constraint even when structurally the same
 % ($\type{T} \lessdotCC \type{S} \neq \type{T} \lessdotCC \type{S}$).
 % This is necessary to solve challenge \ref{challenge:1}.
 % A capture constraint is bound to a specific let statement.
 \textit{Note:}
 In the special case \lstinline{let x = v in concat(x,x)} the constraints would look like
 $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}},
 \wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC_\texttt{x} \exptype{List}{\wtv{a}}$
 and we could actually delete one of them without loosing information.
 But this case will never occur in our algorithm, because the let statements for our input programs are generated by a ANF transformation (see \ref{sec:anfTransformation}).
 \section{Constraint generation}\label{chapter:constraintGeneration}
 % Method names are not unique.
 % It is possible to define the same method in multiple classes.
 % The \TYPE{} algorithm accounts for that by generating Or-Constraints.
@@ -9,8 +73,109 @@
 %\subsection{Well-Formedness}
-The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
+
-Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
+% But it can be easily adapted to Featherweight Java or Java.
 % We add T <. a for every return of an expression anyway. If anything returns a Generic like X it is not directly used in a method call like X <c T
 \begin{description}
 \item[input] \TamedFJ{} program in A-Normal form
 \item[output] Constraints
 \end{description}
 The constraint generation works on the \TamedFJ{} language.
 This step is mostly the same as in \cite{TIforFGJ} except for field access and method invocation.
 We will focus on those two parts where also the new capture constraints and wildcard type placeholders are introduced.
 %In \TamedFJ{} capture conversion is implicit.
 %To emulate Java's behaviour we assume the input program not to contain any let statements.
 %They will be added by an ANF transformation (see chapter \ref{sec:anfTransformation}).
 Before generating constraints the input is transformed by an ANF transformation (see section \ref{sec:anfTransformation}).
 %Constraints are generated on the basis of the program in A-Normal form.
 %After adding the missing type annotations the resulting program is valid under the typing rules in \cite{WildFJ}.
 %This is shown in chapter \ref{sec:soundness}
 %\section{\TamedFJ{}: Syntax and Typing}\label{sec:tifj}
 % The syntax forces every expression to undergo a capture conversion before it can be used as a method argument.
 % Even variables have to be catched by a let statement first.
 % This behaviour emulates Java's implicit capture conversion.
 \subsection{ANF transformation}\label{sec:anfTransformation}
 \newcommand{\anf}[1]{\ensuremath{\tau}(#1)}
 %https://en.wikipedia.org/wiki/A-normal_form)
 Featherweight Java's syntax involves no \texttt{let} statement
 and terms can be nested freely similar to Java's syntax.
 Our calculus \TamedFJ{} uses let statements to explicitly apply capture conversion to wildcard types,
 but we don't know which expressions will spawn wildcard types because there are no type annotations yet.
 To emulate Java's behaviour we have to preemptively add capture conversion in every suitable place.
 %To convert it to \TamedFJ{} additional let statements have to be added.
 This is done by a \textit{A-Normal Form} \cite{aNormalForm} transformation shown in figure \ref{fig:anfTransformation}.
 After this transformation every method invocation is preceded by let statements which perform capture conversion on every argument before passing them to the method.
 See the example in listings \ref{lst:anfinput} and \ref{lst:anfoutput}.
 \begin{figure}
 \begin{minipage}{0.45\textwidth}
 \begin{lstlisting}[style=fgj,caption=\TamedFJ{} example,label=lst:anfinput]
 m(l, v){
    return l.add(v);
 }
 \end{lstlisting}
    \end{minipage}%
    \hfill
    \begin{minipage}{0.5\textwidth}
 \begin{lstlisting}[style=tfgj,caption=A-Normal form,label=lst:anfoutput]
 m(l, v) = 
    let x1 = l in
        let x2 = v in x1.add(x2)
 \end{lstlisting}
 \end{minipage}
 \end{figure}
 \begin{figure}
    \begin{center}
 $\begin{array}{lrcl}
 %\text{ANF}
 & \anf{\expr{x}} & = & \expr{x} \\
 & \anf{\texttt{new} \ \type{C}(\overline{t})} & = & \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}}) \\
 & \anf{t.f} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \expr{x}.f \\
 & \anf{t.\texttt{m}(\overline{t})} & = & \texttt{let}\ \expr{x} = \anf{t} \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}} = \anf{\overline{t}} \ \texttt{in}\ \expr{x}.\texttt{m}(\overline{\expr{x}}) \\
 & \anf{t_1 \elvis{} t_2} & = & \anf{t_1} \elvis{} \anf{t_2} \\
 & \anf{\texttt{let}\ x = \expr{t}_1 \ \texttt{in}\ \expr{t}_2} & = & \texttt{let}\ x = \anf{\expr{t}_1} \ \texttt{in}\ \anf{\expr{t}_2} 
 \end{array}$
 \end{center}
 \caption{ANF Transformation}\label{fig:anfTransformation}
 \end{figure}
 \begin{figure}
  \center
 $
 \begin{array}{lrcl}
 %\hline
 \text{Terms} & t & ::= & \expr{x} \\
 & & \ \ | &  \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \texttt{new} \ \type{C}(\overline{\expr{x}_c}) \\
 & & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \expr{x}_c.f \\
 & & \ \ | & \texttt{let}\ \expr{x}_c = t \ \texttt{in}\ \texttt{let}\ \overline{\expr{x}_c} = \overline{t} \ \texttt{in}\ \expr{x}_c.\texttt{m}(\overline{\expr{x}_c}) \\
 & & \ \ | & t \elvis{} t \\
 %\hline
 \end{array}
 $
 \caption{Syntax of a \TamedFJ{} program in A-Normal Form}\label{fig:anf-syntax}
 \end{figure}
 \subsection{Constraint Generation Algorithm}
 % Generally subtype constraints for an expression mirror the subtype relations in the premise of the respective type rule introduced in section \ref{sec:tifj}.
 % Unknown types at the time of the constraint generation step are replaced with type placeholders.
 % The constraint generation step cannot determine if a capture conversion is needed for a field access or a method call.
 % Those statements produce $\lessdotCC$ constraints which signal the \unify{} algorithm that they qualify for a capture conversion.
 The parameter types given to a generic method also affect their return type.
 During constraint generation the algorithm does not know the parameter types yet.
 We generate $\lessdotCC$ constraints and let \unify{} do the capture conversion.
 $\lessdotCC$ constraints are kept until they reach the form $\type{G} \lessdotCC \type{G}$ and a capture conversion is possible.
 % TODO: Challenge examples!
 At points where a well-formed type is needed we use a normal type placeholder.
 Inside a method call expression sub expressions (receiver, parameter) wildcard placeholders are used.
@@ -19,25 +184,12 @@ A normal type placeholder cannot hold types containing free variables.
 Normal type placeholders are assigned types which are also expressible with Java syntax.
 So no types like $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ or $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
-Type variables declared in the class header are passed to \unify{}.
+It is possible to feed the \unify{} algorithm a set of free variables with predefined bounds.
 This is used for class generics see figure \ref{fig:constraints-for-classes}.
 The \fjtype{} function returns a set of constraints aswell as an initial environment $\Delta$
 containing the generics declared by this class.
 Those type variables count as regular types and can be held by normal type placeholders.
 There are two different types of constraints:
 \begin{description}
 \item[$\lessdot$] \textit{Example:}
 $\exptype{List}{String} \lessdot \tv{a}, \exptype{List}{Integer} \lessdot \tv{a}$
 \noindent
 Those two constraints imply that we have to find a type replacement for type variable $\tv{a}$,
 which is a supertype of $\exptype{List}{String}$ aswell as $\exptype{List}{Integer}$.
 This paper describes a \unify{} algorithm to solve these constraints and calculate a type solution $\sigma$.
 For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$.
 \item[$\lessdotCC$] TODO
 % The \fjtype{} algorithm assumes capture conversions for every method parameter.
 \end{description}
 %Why do we need a constraint generation step?
 %% The problem is NP-Hard
 %% a method call, does not know which type it will produce
@@ -45,48 +197,37 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
 %NO equals constraints during the constraint generation step!
 \begin{figure}[tp]
-  \begin{align*}
+  \center
-    % Type
+\begin{tabular}{lcll}
-    \type{T}, \type{U} &::= \tv{a} \mid \wtv{a} \mid \mv{X} \mid {\wcNtype{\Delta}{N}} && \text{types and type placeholders}\\
+    $C $ &$::=$ &$\overline{c}$ & Constraint set \\
-    \type{N} &::= \exptype{C}{\il{T}} && \text{class type (with type variables)} \\
+    $c $ &$::=$ & $\type{T} \lessdot \type{T} \mid \type{T} \lessdotCC \type{T} \mid \type{T} \doteq \type{T}$ & Constraint \\
-    % Constraints
+    $\type{T}, \type{U}, \type{L} $ & $::=$ & $\tv{a} \mid \gtype{G}$ & Type placeholder or Type \\
-    \simpleCons &::= \type{T} \lessdot \type{U} && \text{subtype constraint}\\
+    $\tv{a}$ & $::=$ & $\ntv{a} \mid \wtv{a}$ & Normal and wildcard type placeholder \\
-    \orCons{} &::= \set{\set{\overline{\simpleCons_1}}, \ldots, \set{\overline{\simpleCons_n}}} && \text{or-constraint}\\
+    $\gtype{G}$ & $::=$ & $\type{X} \mid \ntype{N}$ & Wildcard, or Class Type \\
-    \constraint &::= \simpleCons \mid \orCons && \text{constraint}\\
+    $\ntype{N}, \ntype{S}$ & $::=$ & $\wctype{\triangle}{C}{\ol{T}} $ & Class Type \\
-    \consSet &::= \set{\constraints} && \text{constraint set}\\
+    $\triangle$ & $::=$ & $\overline{\wtype{W}}$ & Wildcard Environment \\
-    % Method assumptions:
+    $\wtype{W}$ & $::=$ & $\wildcard{X}{U}{L}$ & Wildcard \\
-    \methodAssumption &::= \exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \exptype{}{\ol{Y}
+\end{tabular}
-                        \triangleleft \ol{P}}\ \ol{\type{T}} \to \type{T}  &&
+  \caption{Syntax of types and constraints used by \fjtype{} and \unify{}}
                                                                \text{method
                                                                type assumption}\\
    \localVarAssumption &::= \texttt{x} : \itype{T} && \text{parameter
                                                       assumption}\\
    \mtypeEnvironment & ::= \overline{\methodAssumption} &
                & \text{method type environment} \\
    \typeAssumptionsSymbol &::= ({\mtypeEnvironment} ; \overline{\localVarAssumption}) 
  \end{align*}
  \caption{Syntax of constraints and type assumptions.}
  \label{fig:syntax-constraints}
 \end{figure}
 \begin{figure}[tp]
  \begin{gather*}
    \begin{array}{@{}l@{}l}
-      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\ol{X} \triangleleft \ol{N}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, K \, \overline{M} \}}) =\\
+      \fjtype & ({\mtypeEnvironment}, \mathtt{class } \ \exptype{C}{\overline{\type{X} \triangleleft \type{N}}} \ \mathtt{ extends } \ \mathtt{N \{ \overline{T} \ \overline{f}; \, \overline{M} \}}) =\\
              & \begin{array}{ll@{}l}
-\textbf{let} & \forall \texttt{m} \in \ol{M}: \tv{a}_\texttt{m}, \ol{\tv{a}_m} \ \text{fresh} \\
+\textbf{let} & \ol{\methodAssumption} =
-             & \ol{\methodAssumption} = \begin{array}[t]{l}
+                \set{ \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \mid
-                \set{ \mv{m'} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}} \to \tv{a}) \mid
+                  \set{ \mv{m}(\ol{x}) = \expr{e} } \in \ol{M}, \, \tv{a}, \ol{\tv{a}}\ \text{fresh} } \\
-                  \mv{m'} \in \ol{M} \setminus \set{\mv{m}}, \, \tv{a}\, \ol{\tv{a}}\ \text{fresh} } \\
+              & \Delta = \set{ \overline{\wildcard{X}{\type{N}}{\bot}} } \\
-\ \cup \, \set{\mv{m} : (\exptype{C}{\ol{X} \triangleleft \ol{N}} \to \ol{\tv{a}_m} \to \tv{a}_\mv{m})}
+              & C = \begin{array}[t]{l}
-\end{array}
+                \set{ \typeExpr(\mtypeEnvironment \cup \ol{\methodAssumption} \cup \set{\mv{this} :
- \\
+              \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}} }, \texttt{e}, \tv{a})
-              & C_m = \typeExpr(\mtypeEnvironment \cup \set{\mv{this} :
+               \\ \quad \quad \quad \quad \mid \set{ \mv{m}(\ol{x}) = \expr{e} }  \in \ol{M},\, \mv{m} : (\exptype{C}{\ol{X}}, \ol{\tv{a}} \to \tv{a}) \in \ol{\methodAssumption}}
-                \exptype{C}{\ol{X}} , \, \ol{x} : \ol{\tv{a}_m} }, \texttt{e}, \tv{a}_\texttt{m}) \\
+                  \end{array} \\
-\textbf{in} 
+              \textbf{in} 
-              & { ( \mtypeEnvironment \cup \ol{\methodAssumption}, \,
+                  & (\Delta, C)
                \bigcup_{\texttt{m} \in \ol{M}} C_m )
                } 
                \end{array}
    \end{array}
  \end{gather*}
@@ -94,39 +235,6 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
  \label{fig:constraints-for-classes}
 \end{figure}
 % \textbf{Method Assumptions}
 % %$\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
 % % \begin{verbatim}
 % % class Example<X> {
 % %   <Y> Y m(Example<Y> p){ ... }
 % % }
 % % \end{verbatim}
 % In Featherweight Java a method type is bound to a specific class.
 % The class \texttt{Example} shown above contains one method \texttt{m}:
 % \begin{displaymath}
 % \textit{mtype}({\texttt{m}, \exptype{Example}{\type{X}}}) = \generics{\type{Y}} \ \exptype{Example}{\type{Y}} \to \type{Y}
 % \end{displaymath}
 % $\Pi$ is a set of method assumptions used by the $\fjtype{}$ algorithm.
 % It's a map of method types to method names.
 % Every method name has a set of possible types,
 % because there could be more than one method with the same name in a program consisting out of multiple classes.
 % To simplify the syntax of method assumptions, we add the inheriting class type to the parameter list:
 % \begin{displaymath}
 % \Pi = \set{ \texttt{m} : \generics{\type{X}, \type{Y}} \ (\exptype{Example}{\type{X}}, \exptype{Example}{\type{Y}}) \to \type{Y}}
 % \end{displaymath}
 % \begin{verbatim}
 % class Example<X> { }
 % <X, Y> Y m(Example<X> this, Example<Y> p){ ... }
 % \end{verbatim}
 \begin{displaymath}
  \begin{array}{@{}l@{}l}
    \typeExpr{} &({\mtypeEnvironment} , \texttt{e}.\texttt{f}, \tv{a}) = \\
@@ -138,7 +246,8 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
                      \orCons\set{
                      \set{ &
                      \tv{r} \lessdotCC \exptype{C}{\ol{\wtv{a}}} ,
-                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} , \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
+                      [\overline{\wtv{a}}/\ol{X}]\type{T} \lessdot \tv{a} ,
                      \ol{\wtv{a}} \lessdot [\overline{\wtv{a}}/\ol{X}]\ol{N}
                      } \\
                      & \quad \mid \mv{T}\ \mv{f} \in \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}
                        , \, \overline{\wtv{a}} \text{ fresh}
@@ -149,203 +258,134 @@ For the example above a correct solution would be $\sigma(\tv{a}) = \wctype{\rwi
  \end{array}
 \end{displaymath}
 The set of method assumptions returned by the \textit{mtypes} function is used to generate the constraints for a method call expression:
 There are two kinds of method calls.
 The ones to already typed methods and calls to untyped methods.
 LetFJ version: %TODO: or use the old version with \lessdotCC constraints. then there is no problem with \Delta'
 % or only use the \lessdotCC with X.C<X> and C<X> on both sides
 % what to do with ? <c X constraints? Just ignore them! they result in X <. X and can be ignored
 % generate a function which converts method types and parameter types to constraints of the form a <. X.C<X>, C<X> <. C<x>
 % add the free variables to \Delta' proof that they cannot escape the scope (they have to be treated differently than \Delta')
 \begin{displaymath}
  \begin{array}{@{}l@{}l}
-      \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
+    \typeExpr{} &({\mtypeEnvironment} , \texttt{let}\ \expr{x} = \expr{e}_1 \ \texttt{in} \ \expr{e}_2, \tv{a}) = \\
-      & \begin{array}{ll}
+                & \begin{array}{ll}
-      \textbf{let}
+                    \textbf{let} 
-      & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
+                    & \tv{e}_1, \tv{e}_2, \tv{x} \ \text{fresh} \\
-      & \consSet_R = \typeExpr(({\mtypeEnvironment} ;
+                    & \consSet_1 = \typeExpr({\mtypeEnvironment}, \expr{e}_1, \tv{e}_1)\\
-        \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
+                    & \consSet_2 = \typeExpr({\mtypeEnvironment} \cup \set{\expr{x} : \tv{x}}, \expr{e}_2, \tv{e}_2)\\
-      & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}})  \\
+                    & \constraint =
-      & \begin{array}{@{}l@{}l}
+                      \set{
-        \constraint = \orCons\set{ & 
+                      \tv{e}_1 \lessdot \tv{x}, \tv{e}_2 \lessdot \tv{a}
-                  \begin{array}[t]{l}
+                      }\\
-                    %TODO: add \ol{\wildcard{X}{\wtv{u}}{\wtv{l}}} to \Delta'
+                    {\mathbf{in}} & {
-                    [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\wtv{u}}{\wtv{l}}}}{C}{\ol{X}},  \exptype{C}{\ol{X}} \lessdot \exptype{C}{\ol{X}},
+                      \consSet_1 \cup \consSet_2 \cup \set{\constraint}}
-                    %[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
+                  \end{array} 
-                    \overline{\tv{r}} \lessdot \ol{T},
+  \end{array}
                    \ol{X} \lessdot \ol{N}, 
                    \ol{Y} \lessdot \ol{N'} \}
                  \end{array}\\
            & \ |\ 
            (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in 
                {\mtypeEnvironment}, \, |\ol{T}| = |\ol{e}|
            , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
        \end{array}\\
      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
      \end{array}
      \end{array}
  \end{displaymath}
 Java version:
 \begin{displaymath}
  \begin{array}{@{}l@{}l}
      \typeExpr{}' & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}})) = \\
      & \begin{array}{ll}
      \textbf{let}
      & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
      & \consSet_R = \typeExpr(({\mtypeEnvironment} ;
        \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
      & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}})  \\
      & \begin{array}{@{}l@{}l}
        \constraint = \orCons\set{ & 
                  \begin{array}[t]{l}
                    %[\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}},  \wctype{\ol{\wildcard{X}{\ntv{u}}{\ntv{l}}}}{C}{\ol{X}} \lessdotCC \exptype{C}{\ol{X}},
                    [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdotCC \exptype{C}{\ol{X}},
                    \overline{\tv{r}} \lessdotCC \ol{T},
                    \ol{X} \lessdot \ol{N}, 
                    \ol{Y} \lessdot \ol{N'} \}
                  \end{array}\\
            & \ |\ 
            (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in 
                {\mtypeEnvironment}, \, |\ol{T}| = |\ol{e}|
            , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
        \end{array}\\
      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T})
      \end{array}
      \end{array}
  \end{displaymath}
 % \begin{displaymath}
 %       \typeExpr{}' ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \
 %       \typeExpr{} ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}}
 %   \end{displaymath}
 \begin{displaymath}
  \typeExpr{}' ({\mtypeEnvironment} , \texttt{return e;}, \tv{a} ) = \
  \typeExpr{} ({\mtypeEnvironment} , \texttt{e}, \wtv{b} ) \cup \set{ \wtv{b} \lessdot \tv{a}} \quad \quad \tv{a}, \wtv{b} \ \text{fresh}
 \end{displaymath}
-% \begin{displaymath}
+
-% \begin{array}{@{}l@{}l}
+\begin{displaymath}
-%     \typeExpr{} & ({\mtypeEnvironment} , \texttt{e}.\mathtt{m}(\overline{\texttt{e}}), \tv{a} ) = \\
+  \begin{array}{@{}l@{}l}
-%     & \begin{array}{ll}
+      \typeExpr{} & ({\mtypeEnvironment} , \expr{v}.\mathtt{m}(\overline{\expr{v}}), \tv{a}) = \\
-%     \textbf{let}
+      & \begin{array}{ll}
-%     & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
+      \textbf{let}
-%     & \consSet_R = \typeExpr(({\mtypeEnvironment} ;
+      & \tv{r}, \ol{\tv{r}} \text{ fresh} \\
-%       \overline{\localVarAssumption}), \texttt{e}, \tv{r})\\
+      & \constraint = [\overline{\wtv{b}}/\ol{Y}]\set{
-%     & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \ol{e}, \ol{\tv{r}})  \\
+                    \ol{S} \lessdotCC \ol{T}, \type{T} \lessdot \tv{a}, 
-%     & \begin{array}{@{}l@{}l}
+                    \ol{Y} \lessdot \ol{N} }\\
-%       \constraint = \orCons\set{ & 
+      \mathbf{in} & (\consSet_R \cup \overline{\consSet} \cup \constraint, \type{T}) \\
-%                 \begin{array}[t]{l}
+      & \mathbf{where}\ \begin{array}[t]{l}
-%                   [\overline{\wtv{a}}/\ol{X}] [\overline{\wtv{b}}/\ol{Y}] \{ \tv{r} \lessdot \exptype{C}{\ol{X}},
+        \expr{v}, \ol{v} : \ol{S} \in \localVarAssumption \\
-%                   \overline{\tv{r}} \lessdot \ol{T},
+        \texttt{m} : \generics{\ol{Y} \triangleleft \ol{N}}\overline{\type{T}} \to \type{T} \in {\mtypeEnvironment}
-%                   \type{T} \lessdot \tv{a}, 
+      \end{array}
-%                   \ol{X} \lessdot \ol{N}, 
+                    
-%                   \ol{Y} \lessdot \ol{N'} \}
+      \end{array}
-%                 \end{array}\\
+      \end{array}
-%           & \ |\ 
+  \end{displaymath}
 %           (\exptype{C}{\ol{X} \triangleleft \ol{N}}.\texttt{m} : \generics{\ol{Y} \triangleleft \ol{N'}}\overline{\type{T}} \to \type{T}) \in 
 %               {\mtypeEnvironment}
 %           , \, \overline{\wtv{a}} \text{ fresh}, \, \overline{\wtv{b}} \text{ fresh} }
 %       \end{array}\\
 %     \mathbf{in} & \consSet_R \cup \overline{\consSet} \cup \constraint
 %     \end{array}
 %     \end{array}
 % \end{displaymath}
 \\[1em]
 \noindent
 \textbf{Example:}
 \begin{verbatim}
 class Class1{
-  <X> X m(List<X> lx, List<? extends X> lt){ ... }
+  <A> A head(List<X> l){ ... }
-  List<? extends String> wGet(){ ... }
+  List<? extends String> get() { ... }
  List<String> get() { ... }
 }
 class Class2{
  example(c1){
-    return c1.m(c1.get(), c1.wGet());
+    return c1.head(c1.get());
  }
 }
 \end{verbatim}
 %This example comes with predefined type annotations.
-We assume the class \texttt{Class1} has already been processed by our type inference algorithm,
+We assume the class \texttt{Class1} has already been processed by our type inference algorithm
-which has lead to the given type annotations for \texttt{Class1}.
+leading to the following type annotations:
-Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
+%Now we call the $\fjtype{}$ function with the class \texttt{Class2} and the method assumptions for the preceeding class:
 \begin{displaymath}
 \mtypeEnvironment =  \left\{\begin{array}{l}
-    \type{Class1}.\texttt{m}: \generics{\type{X} \triangleleft \type{Object}} \ 
+    \texttt{m}: \generics{\type{A} \triangleleft \type{Object}} \ 
-      (\exptype{List}{\type{X}}, \, \wctype{\wildcard{A}{\type{X}}{\bot}}{List}{\wildcard{A}{\type{X}}{\bot}}) \to \type{X}, \\
+      (\type{Class1},\, \exptype{List}{\type{A}}) \to \type{X}, \\
-     \type{Class1}.\texttt{wGet}: () \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\wildcard{A}{\type{Object}}{\type{String}}}, \\
+     \texttt{get}: (\type{Class1}) \to \wctype{\wildcard{A}{\type{Object}}{\type{String}}}{List}{\rwildcard{A}}
     \type{Class1}.\texttt{get}: () \to \exptype{List}{\type{String}}
 \end{array} \right\} 
 \end{displaymath}
-The result of the $\typeExpr{}$ function is the constraint set
+At first we have to convert the example method to a syntactically correct \TamedFJ{} program.
-\begin{displaymath}
+Afterwards the the \fjtype{} algorithm is able to generate constraints.
 C = \left\{ \begin{array}{l}
 \tv{c1} \lessdot \type{Class1}, \\
 \tv{p1} \lessdot \exptype{List}{\wtv{x}}, \\
 \exptype{List}{\type{String}} \lessdot \tv{p1}, \\
 \tv{p2} \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}, \\
 \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{p2} 
 \end{array} \right\}
 \end{displaymath}
 \begin{minipage}{0.45\textwidth}
  \begin{lstlisting}[style=tamedfj]
 class Class2 {
  example(c1) = let x = c1 in
    let xp = x.get() in x.m(xp);
 }
 \end{lstlisting}
      \end{minipage}%
      \hfill
      \begin{minipage}{0.5\textwidth}
 \begin{constraintset}
 $
    \begin{array}{l}
      \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
    \ntv{c1} \lessdot \ntv{x}, \ntv{x} \lessdotCC \type{Class1}, \\
    \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdot \tv{xp}, \\
    \tv{xp} \lessdotCC \exptype{List}{\wtv{a}}
    \end{array}
 $
  \end{constraintset}
 \end{minipage}
-The first parameter of a method assumption is the receiver type $\type{T}_r$.
+Following is a possible solution for the given constraint set:
 \texttt{Class1} for this example.
 Therefore the $(\tv{c1} \lessdot \type{Class1})$ constraint.
 The type variable $\tv{c1}$ is assigned to the parameter \texttt{c1} of the \texttt{example} method.
-or a simplified version:
+\begin{minipage}{0.55\textwidth}
  \begin{lstlisting}[style=letfj]
 class Class2 {
  example(c1) = let x : Class1 = c1 in
    let xp : (*@$\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$@*) = x.get()
      in x.m(xp);
 }
 \end{lstlisting}
      \end{minipage}%
      \hfill
      \begin{minipage}{0.4\textwidth}
 \begin{constraintset}
 $
    \begin{array}{l}
    \sigma(\ntv{x}) = \type{Class1} \\
    %\tv{xp} \lessdot \exptype{List}{\wtv{x}}, \\
    %\exptype{List}{\type{String}} \lessdot \tv{p1}, \\
    \sigma(\tv{xp}) = \wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \\
    \end{array}
 $
  \end{constraintset}
 \end{minipage}
-\begin{displaymath}
+For $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$ to be a correct solution for $\tv{xp}$
-C = \left\{ \begin{array}{l}
+the constraint $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{a}}$
-\tv{c1} \lessdot \type{Class1}, \\
+must be satisfied.
-\exptype{List}{\type{String}} 
+This is possible, because we deal with a capture constraint.
- \lessdot \exptype{List}{\wtv{x}}, \\
+The $\lessdotCC$ constraint allows the left side to undergo a capture conversion
-\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}
+which leads to $\exptype{List}{\rwildcard{A}} \lessdot \exptype{List}{\wtv{a}}$.
- \lessdot \wctype{\wildcard{A}{\wtv{x}}{\bot}}{List}{\rwildcard{A}}
+Now a substitution of the wildcard placeholder $\wtv{a}$ with $\rwildcard{A}$ leads to a satisfied constraint set.
 \end{array} \right\}
 \end{displaymath}
-
+The wildcard placeholders are not used as parameter or return types of methods.
-$\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as a free type variable.
+Or as types for variables introduced by let statements.
-%TODO: Do an example where wildcards are inserted and we need capture conversion
+They are only used for generic method parameters during a method invocation.
-
+Type placeholders which are not flagged as wildcard placeholders ($\wtv{a}$) can never hold a free variable or a type containing free variables.
-\unify{} returns the solution $(\sigma = \set{ \tv{x} \to \type{String} })$
+This practice hinders free variables to leave their scope.
-
+The free variable $\rwildcard{A}$ generated by the capture conversion on the type $\wctype{\wildcard{A}{\type{String}}{\bot}}{List}{\rwildcard{A}}$
-% \\[1em]
+cannot be used anywhere else then inside the constraints generated by the method call \texttt{x.m(xp)}.
 % \noindent
 % \textbf{Example:}
 % \begin{verbatim}
 % class Class1 {
 %   <X> Pair<X, X> make(List<X> l){ ... }
 %   <Y> boolean compare(Pair<Y,Y> p) { ... }
 %   example(l){
 %     return compare(make(l));
 %   }
 % }
 % \end{verbatim}
 % The method call \texttt{make(l)} generates the constraints
 % \begin{displaymath}
 %   \tv{l} \lessdot \exptype{List}{\tv{x}}, \exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}
 % \end{displaymath}
 % with $\tv{l}$ being the type placeholder for the variable \texttt{l}
 % and $\tv{m}$ is the type variable for the return type of the method call.
 % $\tv{m}$ is then used as the parameter for the \texttt{compare} method:
 % \begin{displaymath}
 %   \tv{m} \lessdot \exptype{Pair}{\tv{y}, \tv{y}}
 % \end{displaymath}
 % Note the conversion of the generic parameters \texttt{X} and \texttt{Y} to type variables $\tv{x}$ and $\tv{y}$.
 % Step 3 of the \unify{} algorithm has to look for every possible supertype of $\exptype{Pair}{\tv{x}, \tv{x}}$,
 % when processing the $\exptype{Pair}{\tv{x}, \tv{x}} \lessdot \tv{m}$ constraint.
 \begin{displaymath}
  \begin{array}{@{}l@{}l}
@@ -375,12 +415,12 @@ $\wtv{x}$ is a type variable we use for the generic $\type{X}$. It is flagged as
    \typeExpr{} &({\mtypeEnvironment} , \texttt{new}\ \type{C}(\overline{e}), \tv{a}) = \\
                & \begin{array}{ll}
                    \textbf{let} 
-                    & \ol{\tv{r}} \ \text{fresh} \\
+                    & \ol{\ntv{r}}, \ol{\ntv{a}} \ \text{fresh} \\
-                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\tv{r}}) \\
+                    & \overline{\consSet} = \typeExpr({\mtypeEnvironment}, \overline{e}, \ol{\ntv{r}}) \\
-                    & C = \set{\ol{\tv{r}} \lessdot [\ol{\tv{a}}/\ol{X}]\ol{T}, \ol{\tv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
+                    & C = \set{\ol{\ntv{r}} \lessdot [\ol{\ntv{a}}/\ol{X}]\ol{T}, \ol{\ntv{a}} \lessdot \ol{N} \mid \texttt{class}\ \exptype{C}{\ol{X} \triangleleft \ol{N}} \set{ \ol{T\ f}; \ldots}} \\
                    {\mathbf{in}} & {
                    \overline{\consSet} \cup
-                        \set{\tv{a} \doteq \exptype{C}{\ol{a}}}}
+                        \set{\tv{a} \doteq \exptype{C}{\ol{\ntv{a}}}}}
                  \end{array} 
  \end{array}
 \end{displaymath}
--- a/fig1.eps
+++ b/fig1.eps
--- a/introduction.tex
+++ b/introduction.tex
@@ -4,157 +4,201 @@
 % - Kapitel 1.2 + 1.3 ist noch zu komplex
 % - Constraints und Unifikation erklären, bevor Unifikation erwähnt wird
 %Inhalt:
 % Global type inference example (the sameList example)
 % Wildcards are needed because Java has side effects
 % Capture Conversion
 % Explain difference between local and global type inference
 % \begin{recap}\textbf{TI for FGJ without Wildcards:}
 % \TFGJ{} generates subtype constraints $(\type{T} \lessdot \type{T})$ consisting of named types and type placeholders.
 % For example the method invocation \texttt{concat(l, new Object())} generates the constraints
 % $\tv{l} \lessdot \exptype{List}{\tv{a}}, \type{Object} \lessdot \tv{a}$.
 % Subtyping without the use of wildcards is invariant \cite{FJ}:
 % Therefore the only possible solution for the type placeholder $\tv{a}$ is $\tv{a} \doteq \type{Object}$. % in Java and Featherweight Java.
 % The correct type for the variable \texttt{l} is $\exptype{List}{\type{Object}}$ (or a direct subtype).
 % %- usually the type of e must be subtypes of the method parameters
 % %- in case of a polymorphic method: type placeholders resemble type parameters
 % The type inference algorithm for Featherweight Generic Java \cite{TIforFGJ} (called \TFGJ{}) is complete and sound:
 % It is able to find a type solution for a Featherweight Generic Java program, which has no type annotations at all,
 % if there is any.
 % It's only restriction is that no polymorphic recursion is allowed.
 % \end{recap}
 \section{Type Inference for Java}
 - Type inference helps rapid development
 - used in Java already (var keyword)
 - keeps source code clean
 Java comes with a local type inference algorithm
 used for lambda expressions, method calls, and the \texttt{var} keyword.
 A type inference algorithm that is able to recreate any type annotation
 even when no type information is given at all is called a global type inference algorithm.
 The global type inference algorithm presented here is able to deal with all Java types including wildcard types.
 It can also be used for regular Java programs.
 %The goal is to find a correct typing for a given Java program.
 Type inference for Java has many use cases and could be used to help programmers by inserting correct types for them,
-Finding better type solutions for already typed Java programs (for example more generical ones),
+finding better type solutions for already typed Java programs (for example more generical ones),
-or allowing to write typeless Java code which is then type infered and thereby type checked by our algorithm.
+or allowing to write typeless Java code which is then type inferred and thereby type checked by our algorithm.
-The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in figure \ref{fig:intro-example-typeless}.
+
-Our algorithm is also capable of finding solutions involving wildcards as shown in figure \ref{fig:intro-example-typed}.
+We propose a global type inference algorithm for Java supporting Wildcards and proven sound.
 Global type inference allows input programs without any type annotations.
 A programmer could write Java code without stressing about types and type annotations which
 are infered and inserted by our algorithm.
 %This leads to better types (Poster referenz)
 %The algorithm proposed in this paper can determine a correct typing for the untyped Java source code example shown in listing \ref{lst:intro-example-typeless}.
 %In this case our algorithm would also be able to propose a solution including wildcards as shown in listing \ref{lst:intro-example-typed}.
 %This paper extends a type inference algorithm for Featherweight Java \cite{TIforFGJ} by adding wildcards.
 %The last step to create a type inference algorithm compatible to the Java type system.
 The algorithm presented in this paper is a slightly improved version of the one in \cite{TIforFGJ} including wildcard support.
 %a modified version of the \unify{} algorithm presented in \cite{plue09_1}.
 The input to the type inference algorithm is a Featherweight Java program (example in figure \ref{fig:nested-list-example-typeless}) conforming to the syntax shown in figure \ref{fig:syntax}.
 The \fjtype{} algorithm calculates constraints based on this intermediate representation,
 which are then solved by the \unify{} algorithm
 resulting in a correctly typed program (see figure \ref{fig:nested-list-example-typed}).
 \subsection{Comparision to similar Type Inference Algorithms}
 To outline the contributions in this paper we will list the advantages and improvements to smiliar type inference algorithms:
 \begin{description}
    \item[Global Type Inference for Featherweight Java] \cite{TIforFGJ} is a predecessor to our algorithm.
 The type inference algorithm presented here supports Java Wildcards.
 % Proven sound on type rules of Featherweight Java, which are also proven to produce sound programs
 % implication rules that follow the subtyping rules directly. Easy to understand soundness proof
 % capture conversion is needed
 \textit{Example:} The type inference algorithm for Generic Featherweight Java produces \texttt{Object} as the return type of the
 \texttt{genBox} method in listing \ref{lst:intro-example-typeless}
 whereas our type inference algorithm will infer the type solution shown in listing \ref{lst:intro-example-typed}
 involving a wildcard type.
 \item[Type Unification for Java with Wildcards]
 An existing unification algorithm for Java with wildcards \cite{plue09_1} states the same capabilities,
 but exposes some errors when it comes to method invocations.
 Especially the challenges shown in chapter \ref{challenges} are handled incorrectly.
 The main reasons are that Plümickes algorithm only supports types which are expressible in Java syntax
 and its soundness is proven towards a self-defined subtype ordering, but never against a complete type system.
 It appears that the subtype relation changes depending on whether a type is used as an argument to a method invocation.
 We resolve this by denoting Java wildcards as existential types
 and introducing a second kind of subtype constraint. %, the current state of the art
 %and is able to deal with types that are not directly denotable in Java. 
 Additionally the soundness of our algorithm is proven using a Featherweight Java calculus \cite{WildFJ}.
 %The algorithm presented in this paper is able to solve all those challenges correctly
 %and it's correctness is proven using a Featherweight Java calculus \cite{WildFJ}.
 %But they are all correctly solved by our new type inference algorithm presented in this paper.
 \item[Java Type Inference]
 Standard Java provides type inference in a restricted form % namely {Local Type Inference}.
 which only works for local environments where the surrounding context has known types.
 But our global type inference algorithm is able to work on input programs which do not hold any type annotations at all.
 We will show the different capabilities with an example.
 In listing \ref{lst:tiExample} the method call \texttt{emptyList} is missing
 its type parameters.
 Java is using a matching algorithm \cite{javaTIisBroken} to replace \texttt{T} with \texttt{String} 
 resulting in the correct expected type \texttt{List<String>}.
 %The invocation of \texttt{emptyList} missing type parameters can be added by Java's local type inference
 %because the expected return type is known. \texttt{List<String>} in this case.
 \begin{lstlisting}[caption=Extract of a valid Java program, label=lst:tiExample]
 <T> List<T> emptyList() { ... }
 List<String> ls = emptyList();
 \end{lstlisting}
 %\textit{Local Type Inference limitations:}
 Note that local type inference depends on the type annotation on the left side of the assignment.
 When calling the \texttt{emptyList} method without this type context its return value will be set to a \texttt{List<Object>}.
 The Java code snippet in \ref{lst:tiLimit} is incorrect, because \texttt{emptyList()} returns
 a \texttt{List<Object>} instead of the required $\exptype{List}{\exptype{List}{String}}$.
 \begin{lstlisting}[caption=Limitations of Java's Type Inference, label=lst:tiLimit]
 emptyList().add(new List<String>())
    .get(0)
    .get(0); //Typing Error
 \end{lstlisting}
 %List<String> <. A
 %List<A> <: List<B>, B <: List<C> 
 % B = A and therefore A on the left and right side of constraints.
 % this makes matching impossible
 The second call to \texttt{get} produces a type error, because Java expects \texttt{emptyList} to return
 a \texttt{List<Object>}.
 The type inference algorithm presented in this paper will correctly replace the type parameter \texttt{T} of the \texttt{emptyList}
 method with \texttt{List<List<String>>} and proof this code snippet correct.
 The local type inference algorithm based on matching cannot produce this solution.
 Here our type inference algorithm based on unification is needed.
 \end{description}
 % %motivate constraints: 
 % To solve this example our Type Inference algorithm will create constraints
 % $
 % \exptype{List}{\tv{a}} \lessdot \tv{b},
 % \tv{b} \lessdot \exptype{List}{\tv{c}},
 % \tv{c} \lessdot \exptype{List}{\tv{d}}
 % $
 %\subsection{Conclusion}
 % Additions: TODO
 % - Global Type Inference Algorithm, no type annotations are needed
 % - Soundness Proof 
 % - Easy to implement
 % - Capture Conversion support
 % - Existential Types support
 Our contributions are
 \begin{itemize}
 \item
 We introduce the language \tifj{} (chapter \ref{sec:tifj}).
 A Featherweight Java derivative including Generics, Wildcards and Type Inference.
 \item
 We support capture conversion and Java style method calls.
 This requires existential types in a form which is not denotable by Java syntax \cite{aModelForJavaWithWildcards}.
-The algorithm is able find the correct type for the method \texttt{m} in the following example:
+\item
 \begin{verbatim}
    <X> Pair<X,X> make(List<X> l)
    Boolean compare(Pair<X,X> p)
    List<?> b;
    Boolean m() = this.compare(this.make(b));
 \end{verbatim}
 We present a novel approach to deal with existential types and capture conversion during constraint unification.
-The algorithm is split in two parts. A constraint generation step and an unification step.
+\item The algorithm is split in two parts. A constraint generation step and an unification step.
-
+Input language and constraint generations can be extended without altering the unification part.
-We proof soundness and aim for a good compromise between completeness and time complexity.
+\item
-Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
+We prove soundness and aim for a good compromise between completeness and time complexity.
-\begin{verbatim}
+\end{itemize}
-class SuperPair<A,B>{
+% Our algorithm finds a correct type solution for the following example, where the Java local type inference fails:
-    A a;
+% \begin{verbatim}
-    B b;
+% class SuperPair<A,B>{
-}
+%     A a;
-class Pair<A,B> extends SuperPair<B,A>{
+%     B b;
    A a;
    B b;
    <X> X choose(X a, X b){ return b; }
    String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
        return choose(choose(a,b).value.a,b.value.b);
    }
 }
 \end{verbatim}
 \begin{figure}[tp]
      \begin{subfigure}[t]{\linewidth}
 \begin{lstlisting}[style=fgj]
 class List<A> {
    List<A> add(A v) { ... }
 }
 class Example {
    m(l, la, lb){
        return l
            .add(la.add(1))
            .add(lb.add("str"));
    }
 }
 \end{lstlisting}
        \caption{Java method with missing return type}
        \label{fig:nested-list-example-typeless}
      \end{subfigure}
      ~
 %       \begin{subfigure}[t]{\linewidth}
 % \begin{lstlisting}[style=tfgj]
 % class List<A> {
 %     List<A> add(A v) { ... }
 % }
 % class Pair<A,B> extends SuperPair<B,A>{
 %     A a;
 %     B b;
-% class Example {
+%     <X> X choose(X a, X b){ return b; }
-%     m(l, la, lb){
+
-%         return let r2 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = {
+%     String m(List<? extends Pair<Integer, String>> a, List<? extends Pair<Integer, String>> b){
-%             let r1 : (*@$\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$@*) = l in {
+%         return choose(choose(a,b).value.a,b.value.b);
 %                 let p1 : (*@$\exptype{List}{\type{Integer}}$@*) = {
 %                     let xa = la in xa.add(1)
 %                     } in x1.add(p1)    
 %             } in {
 %                 let p2 = {
 %                     let xb = lb in xb.add("str")
 %                     } in x2.add(p2)
 %             };
 %     }
 % }
-% \end{lstlisting}
+% \end{verbatim}
 %         \caption{Featherweight Java Representation}
 %         \label{fig:nested-list-example-let}
 %       \end{subfigure}
 %       ~
      \begin{subfigure}[t]{\linewidth}
 \begin{lstlisting}[style=tfgj]
 class List<A> {
    List<A> add(A v) { ... }
 }
 class Example {
    m(List<List<? extends Object>> l, List<Integer> la, List<String> lb){
        return l
            .add(la.add(1))
            .add(lb.add("str"));
    }
 }
 \end{lstlisting}
        \caption{Java Representation}
        \label{fig:nested-list-example-typed}
      \end{subfigure}
      %\caption{Example code}
      %\label{fig:intro-example-code}
 \end{figure}
-%TODO
+\begin{figure}
-% The goal is to proof soundness in respect to the type rules introduced by \cite{aModelForJavaWithWildcards}
+\begin{minipage}{0.43\textwidth}
-% and \cite{WildcardsNeedWitnessProtection}.
+\begin{lstlisting}[style=java,label=lst:intro-example-typeless,caption=Missing return type]
 \begin{figure}[tp]
      \begin{subfigure}[t]{0.49\linewidth}
    \begin{lstlisting}[style=fgj]
 genList() {
-    if( ... ) {
+  if( ... ) {
-        return new List<String>();
+    return new List(1);
-    } else {
+  } else {
-        return new List<Integer>();
+    return new List("Str");
-    }
+  }
 }
    \end{lstlisting}
-        \caption{Java method with missing return type}
+\end{minipage}%
-        \label{fig:intro-example-typeless}
+\hfill
-      \end{subfigure}
+\begin{minipage}{0.55\textwidth}
-      ~
+\begin{lstlisting}[style=tfgj,caption=Type inference solution,label=lst:intro-example-typed]
      \begin{subfigure}[t]{0.49\linewidth}
    \begin{lstlisting}[style=tfgj]
 List<?> genList() {
-    if( ... ) {
+  if( ... ) {
-        return new List<String>();
+    return new List<Integer>(1);
-    } else {
+  } else {
-        return new List<Integer>();
+    return new List<String>("Str");
-    }
+  }
 }
    \end{lstlisting}
-        \caption{Correct type}
+\end{minipage}
        \label{fig:intro-example-typed}
      \end{subfigure}
      %\caption{Example code}
      %\label{fig:intro-example-code}
 \end{figure}
 % \subsection{Wildcards}
@@ -165,224 +209,299 @@ List<?> genList() {
 % \texttt{List<Object>} is not a valid return type for the method \texttt{genList}.
 % The type inference algorithm has to find the correct type involving wildcards (\texttt{List<?>}).
-\subsection{Global Type Inference}
+\section{Java Wildcards}
 A global type inference algorithm works on an input with no type annotations at all.
 %TODO: Describe global type inference and lateron why it is so hard to 
 Global type inference means that there are no type annotations at all.
 \begin{verbatim}
 m(l) {
    return l.add(l);
 }
 \end{verbatim}
-$\tv{l} \lessdotCC \exptype{List}{\wtv{x}}, \tv{l} \lessdotCC \wtv{x}$
+Java has invariant subtyping for polymorphic types.
-
+%but it incooperates use-site variance via so called wildcard types.
-
+A \texttt{List<String>} is not a subtype of \texttt{List<Object>}
 No capture conversion for methods in the same class:
 Given two methods without type annotations like
 \begin{verbatim}
 // m :: () -> r
 m() = new List<String>() :? new List<Integer>();
 // id :: (a) -> a
 id(a) = a
 \end{verbatim}
 and a method call \texttt{id(m())} would lead to the constraints:
 $\exptype{List}{\type{String}} \lessdot \ntv{r},
 \exptype{List}{\type{Integer}} \lessdot \ntv{r},
 \ntv{r} \lessdot \ntv{a}$
 In this example capture conversion is not applicable,
 because the \texttt{id} method is not polymorphic.
 The type solution provided by \unify{} for this constraint set is:
 $\sigma(\ntv{r}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}, 
 \sigma(\ntv{a}) = \wctype{\rwildcard{X}}{List}{\rwildcard{X}}$
 \begin{verbatim}
 List<?> m() = new List<String>() :? new List<Integer>();
 List<?> id(List<?> a) = a
 \end{verbatim}
 The following example has the \texttt{id} method already typed and the method \texttt{m}
 extended by a recursive call \texttt{id(m())}:
 \begin{verbatim}
 <A> List<A> id(List<A> a) = a
 m() = new List<String>() :? new List<Integer>() :? id(m());
 \end{verbatim}
 Now the constraints make use of a $\lessdotCC$ constraint:
 $\exptype{List}{\type{String}} \lessdot \ntv{r},
 \exptype{List}{\type{Integer}} \lessdot \ntv{r},
 \ntv{r} \lessdotCC \exptype{List}{\wtv{a}}$
 After substituting $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ for $\ntv{r}$ like in the example before
 we get the constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$.
 Due to the $\lessdotCC$ \unify{} is allowed to perform a capture conversion yielding
 $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
 \textit{Note:} The wildcard placeholder $\wtv{a}$ is allowed to hold free variables whereas a normal placeholder like $\ntv{r}$
 is never assigned a type containing free variables.
 Therefore \unify{} sets $\wtv{a} \doteq \rwildcard{X}$, completing the constraint set and resulting in the type solution:
 \begin{verbatim}
 List<?> m() = new List<String>() :? new List<Integer>() :? id(m());
 \end{verbatim}
 \subsection{Java Wildcards}
 Wildcards are expressed by a \texttt{?} in Java and can be used as parameter types.
 Wildcards can be formalized as existential types \cite{WildFJ}.
 \texttt{List<? extends Object>} and \texttt{List<? super String>} are both wildcard types
 denoted in our syntax by $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$ and
 $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
 Wildcards add variance to Java type parameters.
 Generally Java has invariant subtyping for polymorphic types.
 A \texttt{List<String>} is not a subtype of \texttt{List<Object>} for example
 even though it seems intuitive with \texttt{String} being a subtype of \texttt{Object}.
 To make the type system more expressive Java incooperates use-site variance by allowing wildcards (\texttt{?}) in type annotations.
 For example a type \texttt{List<?>} (short for \texttt{List<? extends Object>}, with \texttt{?} being a placeholder for any type) %with the wildcard \texttt{?} representing a placeholder for any type
 is a supertype of \texttt{List<String>} and \texttt{List<Object>}.
 %The \texttt{?} is a wildcard type which can be replaced by any type as needed.
 %Class instances in Java are mutable and passed by reference.
 Subtyping must be invariant in Java otherwise the integrity of data classes like \texttt{List} cannot be guaranteed.
 See listing \ref{lst:invarianceExample} for example
 where an \texttt{Integer} would be added to a list of \texttt{String}
 if not for the Java type system which rejects the assignment \texttt{lo = ls}.
 Listing \ref{lst:wildcardIntro} shows the use of wildcards rendering the assignment \texttt{lo = ls} correct.
 The program still does not compile, because now the addition of an Integer to \texttt{lo} is rightfully deemed incorrect by Java.
-$\exptype{List}{String} <: \wctype{\wildcard{X}{\bot}{\type{Object}}}{List}{\rwildcard{X}}$
+\begin{figure}
-means \texttt{List<String>} is a subtype of \texttt{List<? extend Object>}.
+\begin{minipage}{0.48\textwidth}
-The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound at the same time,
+\begin{lstlisting}[caption=Java Invariance Example,label=lst:invarianceExample]{java}
 List<String> ls = ...;
 List<Object> lo = ...;
 lo = ls; // typing error!
 lo.add(new Integer(1));
 \end{lstlisting}
 \end{minipage}
 \hfill
 \begin{minipage}{0.5\textwidth}
 \begin{lstlisting}[caption=Use-Site Variance Example,label=lst:wildcardIntro]{java}
 List<String> ls = ...;
 List<? extends Object> lo = ...;
 lo = ls; // correct
 lo.add(new Integer(1)); // error!
 \end{lstlisting}
 \end{minipage}
 \end{figure}
 Wildcard types are virtual types.
 There is no instantiation of a \texttt{List<?>}.
 It is a placeholder type which can hold any kind of list like
 \texttt{List<String>} or \texttt{List<Object>}.
 This type can also change at any given time, for example when multiple threads
 share a reference to the same field.
 A wildcard \texttt{?} must be considered a different type everytime it is accessed.
 Therefore calling the method \texttt{concat} with two wildcard lists in the example in listing \ref{lst:concatError} is incorrect.
 % The \texttt{concat} method does not create a new list,
 % but adds all elements from the second argument to the list given as the first argument.
 % This is allowed in Java, because both lists are of the polymorphic type \texttt{List<X>}.
 % As shown in listing \ref{lst:concatError} this leads to a inconsistent \texttt{List<String>}
 % if Java would treat \texttt{?} as a regular type and instantiate the type variable \texttt{X}
 % of the \texttt{concat} function with \texttt{?}.
 \begin{figure}
 \begin{lstlisting}[caption=Wildcard Example with faulty call to a concat method,label=lst:concatError]{java}
 <X> List<X> concat(List<X> l1, List<X> l2){
    return l1.addAll(l2);
 }
 List<String> ls = new List<String>();
 List<?> l1 = ls;
 List<?> l2 = new List<Integer>(1); // List containing Integer
 concat(l1, l2); // Error! Would concat two different lists
 \end{lstlisting}
 \end{figure}
 To determine the correctness of method calls involving wildcard types Java's typecheck
 makes use of a concept called \textbf{Capture Conversion}.
 %  was designed to make Java wildcards useful.
 % - without capture conversion 
 % - is used to open wildcard types
 % - 
 This process was formalized for Featherweight Java \cite{FJ} by replacing existential types with wildcards and capture conversion with let statements \cite{WildcardsNeedWitnessProtection}.
 We propose our own Featherweight Java derivative called \TamedFJ{} defined in chapter \ref{sec:tifj}.
 To express the example in listing \ref{lst:wildcardIntro} with our calculus we first have to translate the wildcard types:
 \texttt{List<? extends Object>} becomes $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
 The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
 and a type they are bound to.
-In this case the name is $\rwildcard{X}$ and it's bound to the the type \texttt{List}.
+In this case the name is $\rwildcard{A}$ with the upper bound $\type{Object}$ and it's bound to the the type \texttt{List}.
 Before we can call the \texttt{add} method on this type we have to add a capture conversion via let statement:
 \begin{lstlisting}
 let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
 \end{lstlisting}
 \expr{lo} is assigned to a new variable \expr{v} bearing the type $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$,
 but inside the let statement the variable \expr{v} will be treated as $\exptype{List}{\rwildcard{A}}$.
 The idea is that every Wildcard type is backed by a concrete type.
 By assigning \expr{lo} to a immutable variable \expr{v} we unpack the concrete type $\exptype{List}{\rwildcard{A}}$
 that was concealed by \expr{lo}'s existential type.
 Here $\rwildcard{A}$ is a fresh variable or a captured wildcard so to say.
 The only information we have about $\rwildcard{A}$ is that it is any type inbetween the bounds $\bot$ and $\type{Object}$
 It is important to give the captured wildcard type $\rwildcard{A}$ an unique name which is used nowhere else.
 With this formalization it gets obvious why the method call to \texttt{concat}
 in listing \ref{lst:concatError} is irregular (see \ref{lst:concatTamedFJ}).
-Those properties are needed to formalize capture conversion.
+\begin{figure}
-Polymorphic method calls need to be wraped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
+\begin{lstlisting}[style=TamedFJ,caption=\TamedFJ{} representation of the concat call from listing \ref{lst:concatError}, label=lst:concatTamedFJ]
-In Java this is done implicitly in a process called capture conversion.
+let l1' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l1 in
-When calling a polymorphic method like \texttt{<X> List<X> m(List<X> l1, List<X> l2)} with a \texttt{List<?>}
+    let l2' : (*@$\wctype{\rwildcard{Y}}{List}{\exptype{List}{\rwildcard{Y}}}$@*) = l2 in
-it is not possible to substitute \texttt{?} for \texttt{X}.
+        concat(l1', l2') // Error!
-This would lead to the method header \texttt{List<?> m(List<?> l1, List<?> l2)}
+\end{lstlisting}
-where now a method invocation with \texttt{List<String>} and \texttt{List<Integer>} would be possible,
+\end{figure}
 because both are subtypes of \texttt{List<?>}.
 Capture conversion solves this problem by generating a fresh type variable for every wildcard.
 Calling \texttt{<X> X head(List<X> l1)} with the type \texttt{List<?>} ($\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$)
 creates a fresh type variable $\rwildcard{Y}$ resulting in 
 $\generics{\rwildcard{Y}}\texttt{head}(\exptype{List}{\rwildcard{Y}})$
 with $\rwildcard{Y}$ being used as generic parameter \texttt{X}.
 The $\rwildcard{Y}$ in $\exptype{List}{\rwildcard{Y}}$ is a free variable now.
-%TODO: Read taming wildcards and see if we solve some of the problems presented in section 5 and 6
+% % TODO intro to Featherweight Java
 % is a formal model of the Java programming language reduced to a core set of instructions.
 % - We extend this model by existential types and let expressions.
 % - We copy this from \ref{WildFJ} but make type annotations optional
 % - Our calculus is called \TamedFJ{}
 % - \TamedFJ{} binds every method argument with a let statement.
-% Additionally they can hold a upper or lower bound restriction like \texttt{List<? super String>}.
+% To enable the use of wildcards in argument types of a method invocation
-% Our representation of this type is: $\wctype{\wildcard{X}{\type{String}}{\type{Object}}}{List}{\rwildcard{X}}$
+% Java uses a process called \textit{Capture Conversion}.
-% Every wildcard has a name ($\rwildcard{X}$ in this case) and an upper and lower bound (respectively \texttt{Object} and \texttt{String}).
+% This behaviour is emulated by our language \TamedFJ{};
-
+% a Featherweight Java \cite{FJ} derivative with added wildcard support
-% \subsection{Extensibility} % NOTE: this thing is useless, because final local variables do not need to contain wildcards
+% and a global type inference feature (syntax definition in section \ref{sec:tifj}).
-% In \cite{WildcardsNeedWitnessProtection} capture converson is made explicit with \texttt{let} statements.
+% %\TamedFJ{} is basically the language described by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection} with optional type annotations.
-% We chain let statements in a way that emulates Java behaviour. Allowing the example in \cite{aModelForJavaWithWildcards}
+% Let's have a look at a representation of the \texttt{add} call from the last line in listing \ref{lst:wildcardIntro} with our calculus \TamedFJ{}:
-% % TODO: Explain the advantage of constraints and how we control the way capture conversion is executed
+% %The \texttt{add} call in listing \ref{lst:wildcardIntro} needs to be encased by a \texttt{let} statement in our calculus.
-% But it would be also possible to alter the constraint generation step to include additional features.
+% %This makes the capture converion explicit.
-% Final variables or effectively final variables could be expressed with a 
+% \begin{lstlisting}
-% \begin{verbatim}
+% let v : (*@$\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$@*) = lo in v.<A>add(new Integer(1));
-% <X> concat(List<X> l1, List<X> l2){...}
+% \end{lstlisting}
-% \end{verbatim}
+% The method call is encased in a \texttt{let} statement and
-% \begin{minipage}{0.50\textwidth}
+% \expr{lo} is assigned to a new variable \expr{v} of \linebreak[2]
-% Java:
+% \textbf{Existential Type} $\wctype{\wildcard{A}{\type{Object}}{\bot}}{List}{\rwildcard{A}}$.
-% \begin{verbatim}
+% Our calculus uses existential types \cite{WildFJ} to formalize wildcards:
-% final List<?> l = ...;
+% \texttt{List<? extends Object>} is translated to $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}}$
-% concat(l, l);
+% and \texttt{List<? super String>} is expressed as $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$.
-% \end{verbatim}
+% The syntax used here allows for wildcard parameters to have a name, an uppper and lower bound,
-% \end{minipage}%
+% and a type they are bound to.
-% \begin{minipage}{0.50\textwidth}
+% In this case the name is $\rwildcard{A}$ and it's bound to the the type \texttt{List}.
-% Featherweight Java:
+% Inside the \texttt{let} statement the variable \expr{v} has the type
-% \begin{verbatim}
+% $\exptype{List}{\rwildcard{A}}$.
-% let l : X.List<X> = ... in
+% This is an explicit version of \linebreak[2]
-%     concat(l, l)
+% \textbf{Capture Conversion},
-% \end{verbatim}
+% which makes use of the fact that a concrete type must be behind every wildcard type.
-% \end{minipage}
+% There is no instantiation of a \texttt{List<?>},
 % but there exists some unknown type $\exptype{List}{\rwildcard{A}}$, with $\rwildcard{A}$ inbetween the bounds $\bot$ (bottom type, subtype of all types) and
 % \texttt{Object}.
 % Inside the body of the let statement \expr{v} is treated as a value with the constant type $\exptype{List}{\rwildcard{A}}$.
 % Existential types enable us to formalize \textit{Capture Conversion}.
 % Polymorphic method calls need to be wrapped in a process which \textit{opens} existential types \cite{addingWildcardsToJava}.
 % In Java this is done implicitly in a process called capture conversion (as proposed in Wild FJ \cite{WildFJ}).
 \section{Global Type Inference Algorithm}
 \begin{figure}[h]
 \begin{minipage}{0.49\textwidth}
 \begin{lstlisting}[style=tfgj, caption=Valid Java program, label=lst:addExample]
 <A> List<A> add(List<A> l, A v)
 List<? super String> l = ...;
 add(l, "String");
 \end{lstlisting}
 \end{minipage}\hfill
 \begin{minipage}{0.49\textwidth}
 \begin{lstlisting}[style=tamedfj, caption=\TamedFJ{} representation, label=lst:addExampleLet]
 <A> List<A> add(List<A> l, A v)
 List<? super String> l = ...;
 let v:(*@$\tv{v}$@*) = l
    in add(v, "String");
 \end{lstlisting}
 \end{minipage}\\
 \begin{minipage}{0.49\textwidth}
 \begin{lstlisting}[style=constraints, caption=Constraints, label=lst:addExampleCons]
 (*@$\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}} \lessdot \tv{v}$@*)
 (*@$\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$@*)
 (*@$\type{String} \lessdot \wtv{a}$@*)
 \end{lstlisting}
 \end{minipage}\hfill
 \begin{minipage}{0.49\textwidth}
 \begin{lstlisting}[style=letfj, caption=Type solution, label=lst:addExampleSolution]
 <A> List<A> add(List<A> l, A v)
 List<? super String> l = ...;
 let l2:(*@$\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$@*) = l
    in <X>add(l2, "String");
 \end{lstlisting}
 \end{minipage}
 \end{figure}
 % \begin{description}
 %     \item[input] \tifj{} program
 %     \item[output] type solution
 %     \item[postcondition] the type solution applied to the input must yield a valid \letfj{} program
 % \end{description}
 %Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
 Listings \ref{lst:addExample}, \ref{lst:addExampleLet}, \ref{lst:addExampleCons}, and
 \ref{lst:addExampleSolution} showcase our global type inference algorithm step by step.
 In this example we know that the type of the variable \texttt{l} is an existential type and has to undergo a capture conversion
 before being passed to a method call.
 This is done by converting the program to A-Normal form \ref{lst:addExampleLet},
 which introduces a let statement defining a new variable \texttt{v}.
 Afterwards unknown types are replaced by type placeholders ($\tv{v}$ for the type of \texttt{v}) and constraints are generated (see \ref{lst:addExampleCons}).
 These constraints mirror the type rules of our \TamedFJ{} calculus.
 % During the constraint generation step the type of the variable \texttt{v} is unknown
 % and given the type placeholder $\tv{v}$.
 The methodcall to \texttt{add} spawns the constraint $\tv{v} \lessdotCC \exptype{List}{\wtv{a}}$.
 Here we introduce a capture constraint ($\lessdotCC$) %a new type of subtype constraint
 expressing that the left side of the constraint is subject to a capture conversion.
 Now our unification algorithm \unify{} (defined in chapter \ref{sec:unify}) is used to solve these constraints.
 In the starting set of constraints no type is assigned to $\tv{v}$ yet.
 During the course of \unify{} more and more types emerge.
 As soon as a concrete type for $\tv{v}$ is given \unify{} can conduct a capture conversion if needed.
 %The constraints where this is possible are marked as capture constraints.
 In this example $\tv{v}$ will be set to $\wctype{\wildcard{X}{\type{String}}{\bot}}{List}{\rwildcard{X}}$ leaving us with the following constraints:
 \begin{displaymath}
 \prftree[r]{Capture}{
 \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}, \, \type{String} \lessdotCC \wtv{a}
 }{
 \wildcard{Y}{\type{Object}}{\type{String}} \wcSep \exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\wtv{a}}, \, \type{String} \lessdot \wtv{a}
 }
 \end{displaymath}
 %Capture Constraints $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ allow for a capture conversion,
 %which converts a constraint of the form $(\wctype{\rwildcard{X}}{C}{\rwildcard{X}} \lessdotCC \type{T})$ to $(\exptype{C}{\rwildcard{X}} \lessdot \type{T})$
 The constraint $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}$
 allows \unify{} to do a capture conversion to $\exptype{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$.
 The captured wildcard $\rwildcard{X}$ gets a fresh name and is stored in the wildcard environment of the \unify{} algorithm.
 Leaving us with the solution $\exptype{List}{\rwildcard{Y}} \lessdot \exptype{List}{\rwildcard{Y}}$, $\type{String} \lessdot \rwildcard{Y}$
 The constraint $\type{String} \lessdot \rwildcard{Y}$ is satisfied
 because $\rwildcard{Y}$ has $\type{String}$ as lower bound.
 A correct Featherweight Java program including all type annotations and an explicit capture conversion via let statement is shown in listing \ref{lst:addExampleSolution}.
 This program can be deducted from the type solution of our \unify{} algorithm presented in chapter \ref{sec:unify}.
 In the body of the let statement the type $\wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}}$
 becomes $\exptype{List}{\rwildcard{X}}$ and the wildcard $\wildcard{X}{\type{Object}}{\type{String}}$ is free and can be used as
 a type parameter to method call \texttt{<X>add(v, "String")}.
 % The input to our type inference algorithm is a modified version of the calculus in \cite{WildcardsNeedWitnessProtection} (see chapter \ref{sec:tifj}).
 % First \fjtype{} (see section \ref{chapter:constraintGeneration}) generates constraints
 % and afterwards \unify{} (section \ref{sec:unify}) computes a solution for the given constraint set.
 % Constraints consist out of subtype constraints $(\type{T} \lessdot \type{T})$ and capture constraints $(\type{T} \lessdotCC \type{T})$.
 % \textit{Note:} a type $\type{T}$ can either be a named type, a type placeholder or a wildcard type placeholder.
 % A subtype constraint is satisfied if the left side is a subtype of the right side according to the rules in figure \ref{fig:subtyping}.
 % \textit{Example:} $\exptype{List}{\ntv{a}} \lessdot \exptype{List}{\type{String}}$ is fulfilled by replacing type placeholder $\ntv{a}$ with the type $\type{String}$.
 % Subtype constraints and type placeholders act the same as the ones used in \emph{Type Inference for Featherweight Generic Java} \cite{TIforFGJ}.
 % The novel capture constraints and wildcard placeholders are needed for method invocations involving wildcards.
 % The central piece of this type inference algorithm, the \unify{} process, is described with implication rules (chapter \ref{sec:unify}).
 % We try to keep the branching at a minimal amount to improve runtime behavior.
 % Also the transformation steps of the \unify{} algorithm are directly related to the subtyping rules of our calculus.
 % There are no informal parts in our \unify{} algorithm.
 % It solely consist out of transformation rules which are bound to simple checks.
 \subsection{Challenges}\label{challenges}
 %TODO: Wildcard subtyping is infinite see \cite{TamingWildcards}
 One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
 A wildcard in the Java syntax has no name and is bound to its enclosing type.
 \texttt{List<List<?>>} equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
 During type checking intermediate types like $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$
 or $\wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}}$ can emerge, which have no equivalent in the Java syntax.
 Our type inference algorithm uses existential types internally but spawns type solutions compatible with Java.
 The introduction of wildcards adds additional challenges.
 % we cannot replace every type variable with a wildcard
 Type variables can also be used as type parameters, for example
 $\exptype{List}{String} \lessdot \exptype{List}{\tv{a}}$.
 A problem arises when replacing type variables with wildcards.
 % Wildcards are not reflexive.
 % ( on the equals property ), every wildcard has to be capture converted when leaving its scope
 % do not substitute free type variables
-Lets have a look at two examples:
+Lets have a look at a few challenges:
 \begin{itemize}
-\item \begin{example} \label{intro-example1}
+\item \label{challenge:1}
-The first one is a valid Java program.
+One challenge is to design the algorithm in a way that it finds a correct solution for the program shown in listing \ref{lst:addExample}
-The type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
+and rejects the program in listing \ref{lst:concatError}.
-which is used as the generic method parameter \texttt{A}.
+The first one is a valid Java program,
-
+because the type \texttt{List<? super String>} is \textit{capture converted} to a fresh type variable $\rwildcard{X}$
-Java uses capture conversion to replace the generic \texttt{A} by a capture converted version of the
+which is used as the generic method parameter for the call to \texttt{add} as shown in listing \ref{lst:addExampleLet}.
-\texttt{? super String} wildcard.
+Knowing that the type \texttt{String} is a subtype of the free variable $\rwildcard{X}$
 Knowing that the type \texttt{String} is a subtype of any type the wildcard \texttt{? super String} can inherit
 it is safe to pass \texttt{"String"} for the first parameter of the function.
-\begin{verbatim}
+The second program shown in listing \ref{lst:concatError} is incorrect.
 <A> List<A> add(A a, List<A> la) {}
    List<? super String> list = ...;
    add("String", list);
 \end{verbatim}
 The constraints representing this code snippet are:
 \begin{displaymath}
    \type{String} \lessdotCC \wtv{a},\,
 \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdotCC \exptype{List}{\wtv{a}}
 \end{displaymath}
 Here $\sigma(\tv{a}) = \rwildcard{X}$ is a valid solution.
 \end{example}
 \item \begin{example}\label{intro-example2}
 This example displays an incorrect Java program.
 The method call to \texttt{concat} with two wildcard lists is unsound.
 Each list could be of a different kind and therefore the \texttt{concat} cannot succeed.
-\begin{verbatim}
+The problem gets apparent when we try to write the \texttt{concat} method call in our \TamedFJ{} calculus (listing \ref{lst:concatTamedFJ}):
-<A> List<A> concat(List<A> l1, List<A> l2) {}
+\texttt{l1'} and \texttt{l2'} are two different lists inside the body of the let statements, namely
 $\exptype{List}{\rwildcard{X}}$ and $\exptype{List}{\rwildcard{Y}}$.
 For the method call \texttt{concat(x1, x2)} no replacement for the generic \texttt{A}
 exists to satisfy
 $\exptype{List}{\type{A}} <: \exptype{List}{\type{X}},
 \exptype{List}{\type{A}} <: \exptype{List}{\type{Y}}$.
-    List<?> list = ... ;
+% \textbf{Solution:}
-    concat(list, list);
+% Capture Conversion during Unify.
 \end{verbatim}
 The constraints for this example are:
 $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}, \\
 \wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
 %$\exptype{List}{?} \lessdot \exptype{List}{\tv{a}},
 %\exptype{List}{?} \lessdot \exptype{List}{\tv{a}}$
 Remember that the given constraints cannot have a valid solution.
 %This is due to the fact that the wildcard variables cannot leave their scope.
 In this example the \unify{} algorithm should not replace $\tv{a}$ with the captured wildcard $\rwildcard{X}$.
 \end{example}
 \item 
 \unify{} can only remove wildcards, but never add wildcards to an existing type.
 Java subtyping is invariant.
 The type $\wctype{\rwildcard{X}}{List}{\rwildcard{X}}$ cannot be a subtype of $\exptype{List}{\tv{a}}$
 \unify{} morphs a constraint set into a correct type solution
 gradually assigning types to type placeholders during that process.
 Solved constraints are removed and never considered again.
 In the following example \unify{} solves the constraint generated by the expression
 \texttt{l.add(l.head())} first, which results in $\ntv{l} \lessdot \exptype{List}{\wtv{a}}$.
 \begin{verbatim}
-List<?> l = ...;
+anyList() = new List<String>() :? new List<Integer>()
-m2() {
+add(anyList(), anyList().head());
  l.add(l.head());
 }
 \end{verbatim}
 The type for \texttt{l} can be any kind of list, but it has to be a invariant one.
 Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hiding behind
@@ -390,77 +509,115 @@ Assigning a \texttt{List<?>} for \texttt{l} is unsound, because the type list hi
 An additional constraint $\wctype{\rwildcard{X}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\wtv{a}}$
 is solved by removing the wildcard $\rwildcard{X}$ if possible.
 this problem is solved by ANF transformation
 \item \textbf{Wildcards as Existential Types:}
 One problem is the divergence between denotable and expressable types in Java \cite{semanticWildcardModel}.
 A wildcard in the Java syntax has no name and is bound to its enclosing type:
 $\exptype{List}{\exptype{List}{\type{?}}}$ equates to $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
 During type checking \emph{intermediate types}
 can emerge, which have no equivalent in the Java syntax.
 \begin{lstlisting}[style=java,label=shuffleExample,caption=Intermediate Types Example]
 class List<X> extends Object {...}
 class List2D<X> extends List<List<X>> {...}
 <X> void shuffle(List<List<X>> list) {...}
 List<List<?>> l = ...;
 List2D<?> l2d = ...;
 shuffle(l); // Error
 shuffle(l2d); // Valid
 \end{lstlisting}
 Java is using local type inference to allow method invocations which are not describable with regular Java types.
 The \texttt{shuffle} method in this case is invoked with the type $\wctype{\rwildcard{X}}{List2D}{\rwildcard{X}}$
 which is a subtype of $\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$.
 After capture conversion \texttt{l2d'} has the type $\exptype{List}{\exptype{List}{\rwildcard{X}}}$
 and \texttt{shuffle} can be invoked with the type parameter $\rwildcard{X}$:
 \begin{lstlisting}[style=TamedFJ]
 let l2d' : (*@$\wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}}$@*) = l2d in <X>shuffle(l2d')
 \end{lstlisting}
 For the example shown in listing \ref{shuffleExample} the method call \texttt{shuffle(l2d)} creates the constraints:
 \begin{constraintset}
 \begin{center}
    $
    \begin{array}{l}
    \wctype{\rwildcard{X}}{List2D}{\rwildcard{X}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
    \\
    \hline
    \wctype{\rwildcard{X}}{List}{\exptype{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}
    \\
    \hline
    \textit{Capture Conversion:}\ 
    \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\wtv{x}}}
    \\
    \hline
    \textit{Solution:} \wtv{x} \doteq \rwildcard{X} \implies \exptype{List}{\exptype{List}{\rwildcard{X}}} \lessdot \exptype{List}{\exptype{List}{\rwildcard{X}}}
    \end{array}
    $
 \end{center}
 \end{constraintset}
 The method call \texttt{shuffle(l)} is invalid however,
 because \texttt{l} has the type
 $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}}$.
 There is no solution for the subtype constraint:
 $\exptype{List}{\wctype{\rwildcard{X}}{List}{\rwildcard{X}}} \lessdotCC \exptype{List}{\exptype{List}{\wtv{x}}}$
 \item \label{challenge3} \textbf{Free Variables cannot leaver their scope}:
 \begin{example}
 Take the Java program in listing \ref{lst:mapExample} for example.
 It maps every element of a list
 $\expr{l} : \exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
 to a polymorphic \texttt{id} method.
 We want to use our \unify{} algorithm to determine the correct type for the
 variable \expr{l2}.
 Although we do not specify constraint generation for language constructs like
 lambda expressions used in this example,
 we can imagine that the constraints have to look something like this:
 \begin{minipage}{0.45\textwidth}
 \begin{lstlisting}[caption=List Map Example,label=lst:mapExample]
 <X> List<X> id(List<X> l){ ... }
 List<List<?>> ls;
 l2 = l.map(x -> id(x));
 \end{lstlisting}\end{minipage}
 \hfill
 \begin{minipage}{0.45\textwidth}
 \begin{lstlisting}[style=constraints, caption=Constraints, label=lst:mapExampleCons]
 (*@$\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}}$@*)
 (*@$\exptype{List}{\wtv{x}} \lessdot \tv{z},$@*)
 (*@$\exptype{List}{\tv{z}} \lessdot \tv{l2}$@*)
 \end{lstlisting}
 \end{minipage}
 The constraints
 $\wctype{\rwildcard{A}}{List}{\rwildcard{A}} \lessdotCC \exptype{List}{\wtv{x}},
 \exptype{List}{\wtv{x}} \lessdot \tv{z}$
 stem from the body of the lambda expression
 \texttt{id(x)}.
 \textit{For clarification:} This method call would be represented as the following expression in \letfj{}:
 \texttt{let x1 :$\wctype{\rwildcard{A}}{List}{\rwildcard{A}}$ = x in id(x) :$\tv{z}$}
 The T-Let rule prevents us from using free variables created by the method call to \expr{id}
 to be used in the return type $\tv{z}$.
 But this has to be signaled to the \unify{} algorithm, which does not know about the origin and context of
 the constraints.
 If we naively substitute $\sigma(\tv{z}) = \exptype{List}{\rwildcard{A}}$
 the return type of the \texttt{map} function would be the type $\exptype{List}{\exptype{List}{\rwildcard{A}}}$.
 This type solution is unsound.
 The type of \expr{l2} is the same as the one of \expr{l}:
 $\exptype{List}{\wctype{\rwildcard{A}}{List}{\rwildcard{A}}}$
 \textbf{Solution:}
 We solve this by distinguishing between wildcard placeholders and normal placeholders.
 $\ntv{z}$ is a normal placeholder and is not allowed to contain free variables.
 \end{example}
 \end{itemize}
-The \unify{} algorithm only sees the constraints with no information about the program they originated from.
+%TODO: Move this part. or move the third challenge some underneath.
 The main challenge was to find an algorithm which computes $\sigma(\tv{a}) = \rwildcard{X}$ for example \ref{intro-example1} but not for example \ref{intro-example2}.
 % Solution: A type variable can only take one type and not a wildcard type.
    % A wildcard type is only treated like a wildcard while his definition is in scope (during the reduce rule)
 % \subsection{Capture Conversion}
 % \begin{verbatim}
 % <A> List<A> add(A a, List<A> la) {}
 % List<? super String> list = ...;
 % add("String", list);
 % \end{verbatim}
 % The constraints representig this code snippet are:
 % $\type{String} \lessdot \tv{a},
 % \wctype{\wildcard{X}{\type{Object}}{\type{String}}}{List}{\rwildcard{X}} \lessdot \exptype{List}{\tv{a}}$
 % Under the hood the typechecker has to find a replacement for the generic method parameter \texttt{A}.
 % Java allows a method \texttt{<A> List<A> add(A a, List<A> la)} to be called with
 % \texttt{String} and \texttt{List<? super String>}.
 % A naive approach would be to treat wildcards like any other type and replace \texttt{A}
 % with \texttt{? super String}.
 % Generating the method type \texttt{List<? super String> add(? super String a, List<? super String> la)}.
 % This does not work for a method like
 % \texttt{<A> void merge(List<A> l1, List<A> l2)}.
 % It is crucial for this method to be called with two lists of the same type.
 % Substituting a wildcard for the generic \texttt{A} leads to
 % \texttt{void merge(List<?> l1, List<?> l2)},
 % which is unsound.
 % Capture conversion utilizes the fact that instantiated classes always have an actual type.
 % \texttt{new List<String>()} and \texttt{new List<Object>()} are
 % valid instances.
 % \texttt{new List<? super String>()} is not.
 % Every type $\wcNtype{\Delta}{N}$ contains an underlying instance of a type $\type{N}$.
 % Knowing this fact allows to make additional assumptions.
 % \wildFJ{} type rules allow for generic parameters to be replaced by wildcard types.
 % This is possible because wildcards are split into two parts.
 % Their declaration at the environment part $\Delta$ of a type $\wcNtype{\Delta}{N}$
 % and their actual use in the body of the type $\type{N}$.
 % Replacing the generic \texttt{A} in the type \texttt{List<A>}
 % by a wildcard $\type{X}$ will not generate the type \texttt{List<?>}.
 % \texttt{List<?>} is the equivalent of $\wctype{\wildcard{X}{\type{Object}}{\bot}}{List}{\type{X}}$.
 % The generated type here is $\exptype{List}{\type{X}}$, which has different subtype properties.
 % There is no information about what the type $\exptype{List}{\type{X}}$ actually is.
 % It has itself as a subtype and for example a type like $\exptype{ArrayList}{\type{X}}$.
 % A method call for example only works with values, which are correct instances of classes.
 % Capture conversion automatically converts wildcard type to a concrete class type,
 % which then can be used as a parameter for a method call.
 % In \wildFJ{} this is done via let statements.
 % Written in FJ syntax: $\type{N}$ is a initialized type and
 % $\wcNtype{\Delta}{N}$ is a type containing wildcards $\Delta$.
 % It is crucial for the wildcard names to never be used twice.
 % Otherwise the members of a list with type $\wctype{\type{X}}{List}{\type{X}}$ and
 % a list with type $\wctype{\type{X}}{List}{\type{X}}$ would be the same. $\type{X}$ in fact.
 % The let statement adds wildcards to the environment.
 % Those wildcards are not allowed to escape the scope of the let statement.
 % Which is a problem for our type inference algorithm.
 % The capture converted version of the type $\wctype{\rwildcard{X}}{Box}{\rwildcard{X}}$ is
 % $\exptype{Box}{\rwildcard{X}}$.
 % The captured type is only used as an intermediate type during a method call.
--- a/letfjTransformation.tex
+++ b/letfjTransformation.tex
@@ -0,0 +1,121 @@
 %We could do a translation from Java to \wildFJ explaining implicit capture conversion
 \section{Soundness of Typing}
 We show soundness with the type rules statet in \cite{WildcardsNeedWitnessProtection}.
 A correct \FGJGT{} program can be converted to a correct \wildFJ{} program.
 \begin{figure}
 $\begin{array}{rcl}
    | \texttt{x} |
    & = & \texttt{x} \\
    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e},\, \ol{x} : \ol{T} = \ol{e} \ \texttt{in}\ \texttt{x}.\texttt{m}(\ol{x}) |
    & = & |\texttt{e}|.\texttt{m}(\ol{|e|}) \\
    | \texttt{let} \ \texttt{x} : \type{T} = \texttt{e}\ \texttt{in}\ \texttt{x}.\texttt{f} |
    & = & |\texttt{e}|.\texttt{f} \\
    | \texttt{e} \elvis{} \texttt{e} |
    & = & |\texttt{e}| \elvis{} |\texttt{e}| \\
 \end{array}$
 \caption{Erasure} \label{fig:erasure}
 \end{figure}
 % A constraint Pair<A,B> <. a, then a has infinite possibilities:
 % a =. X.Pair<X,X>
 % a =. X,Y.Pair<X,Y>
 % a =. X.Pair<Pair<X,X>,X>
 % a =. X,Y.Pair<Pair<X,Y>,X>
 % a =. X,Y.Pair<Pair<X,Y>,Y>
 % There is no way to try out every single one of them.
 Starting with the parameters of the method we gradually add every expression which only contains already captured expressions.
 We have a typed expression
 $|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} : \type{T} = \texttt{x in}$
 $|\texttt{e.f}, \texttt{r}| = |\texttt{e}, x| \texttt{let} r = x.\texttt{f} \ \texttt{in}$ 
 $|\texttt{x}, \texttt{r}| = \texttt{let}\ \texttt{r} = \texttt{x in}$
 %TODO: write the transform rules:
 % |e.f, ret| = |e, r| let ret = r.f in
 % |x, ret| = let ret = x in
 % |e.m(e_), ret| = |e, r| |e_, a_| let ret = r.m(a_) in
 Erasure functions:
 $|\texttt{x}| = \texttt{let r} : \wcNtype{\Delta}{N} = \texttt{x in r}$
 $\texttt{x} \longmapsto \texttt{let}\ \texttt{xx} : \type{T} = \texttt{x in xx}$
 $\texttt{x}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in xf}$
 $\begin{array}{l}
 \texttt{e} \longmapsto \texttt{let}\ \texttt{xe} : \type{T} = \texttt{e}' \ \texttt{in xe} \\ 
 \hline
 \vspace*{-0.4cm}\\
 \texttt{e}.f \longmapsto \texttt{let}\ \texttt{xf} : \type{T} = \texttt{x}.f \ \texttt{in x}.f
 \end{array}$
 Example:
 m(a, b) = a.m(b.f);
 let xa = a in let xb = b in let xf = xb.f in let xm = xa.m(xf) in xm
 % TODO: Now we have to proof that there is a LetFJ program for every TIFJ program!
 % |let xr : T = x1.m(x2) in e| = [x1.m(x2)/xr]|e| 
 % |let xf : T = x1.f in e| = [x1.f/xf]|e|
 % |let xr : T = x in e| = [xr/x]|e|
 % |new C(x)| = new C(x)
 % | let xr : T' = x in let xf : T = xr.f | = x.f
 % let x : T' = e' in x = |e|
 % ---------------------------------
 % | let xr : T' = x in let xf : T = xr.f | = x.f
 % let x : T' = e' in x = |e|
 % -----------
 % = 
 We need a language which only has let statemnts and expressions on capture converted variables
 The idea is to use wildcard placeholders inside the method. Also in the bounds of wildcards.
 This makes it possible to replace wildcards with free variables by setting upper and lower bound to that free variable.
 Free variables then can flow freely inside the method body.
 We have to show that a type solution implies that there is a possible transformation to a correct typed letFJ program.
 If there is a possible method type then there must exist a let configuration.
 % By starting with the parameter types and capturing them. Afterwards every capture creates free variables which are used inside
 % TODO: Proof!
 The normal type placeholders represent denotable types.
 %TODO: the type rules stay the same. We generate let statements in a fashion which removes all wildcard types.
 % what about wildcards getting returned by untyped methods? they can also be captured
 % TODO: try soundness proof on the original type rules!
 Removing of extensive wildcards:
 $
 \wctype{\wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{X}, \rwildcard{Y}}
 \lessdot \wctype{\rwildcard{X}}{Pair}{\rwildcard{X}, \rwildcard{X}} \\
 \wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \wtv{x}, \rwildcard{Y} \doteq \wtv{x} \\
 \wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \rwildcard{X} \doteq \rwildcard{Y} \\
 \wildcard{X}{\wtv{u}}{\wtv{l}}, \wildcard{Y}{\wtv{p}}{\wtv{m}} \vdash \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
 \implies \wctype{\wildcard{Y}{\wtv{p}}{\wtv{m}}}{Pair}{\rwildcard{Y}, \rwildcard{Y}}, \wtv{u} \doteq \rwildcard{Y}, \wtv{l} \doteq \rwildcard{Y} \\
 $
 %e.f leads to constraints: r <c C<x> with return type equals the field type T.
 %   T can contain free variables from r. but also it can be used in another constraint and get free variables from inner let statements
 %   X.C<X> <c C<x> -> then T contains X variables
 % let x1 = p1, x2 = p2 in
 %  let r1  = x1 in let r2 = p2 in let f1 = r2.f in let r3 = x1 in let m2 = r3.m2() let ret = r1.m(f1,m2)
 %   in ret
 What about method invocation with no type yet. m2 :: a -> a 
 they are also encased in let expression so the return type can be capture converted.
 Those methods and the parameter types of the current method are the only things not typed.
 All the other types cannot change their type. The captured wildcards can only flow from top to bottom.
 The return type of untyped methods has to be well-formed and cannot contain free variables.
 Therefore no free variables will flow into those types.
--- a/lipics-logo-bw.pdf
+++ b/lipics-logo-bw.pdf
--- a/lipics-v2021.cls
+++ b/lipics-v2021.cls
--- a/llncs.cls
+++ b/llncs.cls
--- a/martin.bib
+++ b/martin.bib
@@ -50,6 +50,8 @@ keywords = {subtyping, type inference, principal types}
  SERIES       = {Lecture Notes in Artificial Intelligence}
 }
@article{DM82,
    author={Luis Damas and Robin Milner},
    title={Principal type-schemes for functional programs},
@@ -65,14 +67,39 @@ keywords = {subtyping, type inference, principal types}
    pages={23-41},
    month=Jan,
    year={1965}}
@article{DBLP:journals/jcss/Milner78, 
  author    = {Robin Milner},
  title     = {A Theory of Type Polymorphism in Programming},
  journal   = {Journal of Computer and Systems Sciences},
  volume    = {17},
  number    = {3},
  pages     = {348--375},
  year      = {1978},
  url       = {https://doi.org/10.1016/0022-0000(78)90014-4},
  doi       = {10.1016/0022-0000(78)90014-4},
  timestamp = {Tue, 16 Feb 2021 14:04:22 +0100},
  biburl    = {https://dblp.org/rec/journals/jcss/Milner78.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
 }   
@article{MM82,
-    author={A. Martelli and U. Montanari},
+author = {Martelli, Alberto and Montanari, Ugo},
-    title={An Efficient Unification Algorithm},
+title = {An Efficient Unification Algorithm},
-    journal={ACM Transactions on Programming Languages and Systems},
+year = {1982},
-    volume={4},
+issue_date = {April 1982},
-    pages={258-282},
+publisher = {Association for Computing Machinery},
-    year={1982}}
+address = {New York, NY, USA},
 volume = {4},
 number = {2},
 issn = {0164-0925},
 url = {https://doi.org/10.1145/357162.357169},
 doi = {10.1145/357162.357169},
 journal = {ACM Trans. Program. Lang. Syst.},
 month = {apr},
 pages = {258–282},
 numpages = {25}
 }
@InProceedings{Plue07_3,
  author = 	 {Martin Pl{\"u}micke},
@@ -326,6 +353,14 @@ articleno = {138},
 numpages = {22},
 keywords = {Null, Java Wildcards, Existential Types}
 }
@inproceedings{AT16,
 author = {Amin, Nada and Tate, Ross},
 year = {2016},
 month = {10},
 pages = {838-848},
 title = {Java and scala's type systems are unsound: the existential crisis of null pointers},
 doi = {10.1145/2983990.2984004}
 }
@InProceedings{TIforFGJ,
  author =	{Stadelmeier, Andreas and Pl\"{u}micke, Martin and Thiemann, Peter},
  title =	{{Global Type Inference for Featherweight Generic Java}},
@@ -352,6 +387,16 @@ keywords = {Null, Java Wildcards, Existential Types}
  publisher={Addison-Wesley Professional}
 }
@Book{GoJoStBrBuSm23,
  author = {Gosling, James and Joy, Bill and Steele, Guy and Bracha, Gilad and Buckley, Alex and Smith, Daniel},
  title = "{The Java\textsuperscript{\textregistered} {L}anguage {S}pecification}",
  Optpublisher = "Addison-Wesley",
  url = {https://docs.oracle.com/javase/specs/jls/se21/jls21.pdf},
  edition = {{J}ava {S}{E} 21},
  year = 2023,
  OPtseries = {The Java series}
 }
@inproceedings{semanticWildcardModel,
  title={Towards a semantic model for Java wildcards},
  author={Summers, Alexander J and Cameron, Nicholas and Dezani-Ciancaglini, Mariangiola and Drossopoulou, Sophia},
@@ -388,4 +433,139 @@ numpages = {14},
 keywords = {existential types, joins, parametric types, single-instantiation inheritance, subtyping, type inference, wildcards}
 }
@inproceedings{javaTIisBroken,
 author = {Smith, Daniel and Cartwright, Robert},
 title = {Java type inference is broken: can we fix it?},
 year = {2008},
 isbn = {9781605582153},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 url = {https://doi.org/10.1145/1449764.1449804},
 doi = {10.1145/1449764.1449804},
 abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
 booktitle = {Proceedings of the 23rd ACM SIGPLAN Conference on Object-Oriented Programming Systems Languages and Applications},
 pages = {505–524},
 numpages = {20},
 keywords = {bounded quantification, generics, intersection types, parameterized types, polymorphic methods, subtyping, type argument inference, type inference, union types, wildcards},
 location = {Nashville, TN, USA},
 series = {OOPSLA '08}
 }
@article{JavaLocalTI,
 author = {Smith, Daniel and Cartwright, Robert},
 title = {Java type inference is broken: can we fix it?},
 year = {2008},
 issue_date = {September 2008},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 volume = {43},
 number = {10},
 issn = {0362-1340},
 url = {https://doi.org/10.1145/1449955.1449804},
 doi = {10.1145/1449955.1449804},
 abstract = {Java 5, the most recent major update to the Java Programming Language, introduced a number of sophisticated features, including a major extension to the type system. While the technical details of these new features are complex, much of this complexity is hidden from the typical Java developer by an ambitious type inference mechanism. Unfortunately, the extensions to the Java 5 type system were so novel that their technical details had not yet been thoroughly investigated in the research literature. As a result, the Java 5 compiler includes a pragmatic but flawed type inference algorithm that is, by design, neither sound nor locally complete. The language specification points out that neither of these failures is catastrophic: the correctness of potentially-unsound results must be verified during type checking; and incompleteness can usually be worked around by manually providing the method type parameter bindings for a given call site.This paper dissects the type inference algorithm of Java 5 and proposes a signficant revision that is sound and able to calculate correct results where the Java 5 algorithm fails. The new algorithm is locally complete with the exception of a difficult corner case. Moreover, the new algorithm demonstrates that several arbitrary restrictions in the Java type system---most notably the ban on lower-bounded type parameter declarations and the limited expressibility of intersection types---are unnecessary. We hope that this work will spur the evolution of a more coherent, more comprehensive generic type system for Java.},
 journal = {SIGPLAN Not.},
 month = {oct},
 pages = {505–524},
 numpages = {20},
 keywords = {wildcards, union types, type inference, type argument inference, subtyping, polymorphic methods, parameterized types, intersection types, generics, bounded quantification}
 }
@article{FJ,
 author = {Igarashi, Atsushi and Pierce, Benjamin C. and Wadler, Philip},
 title = {Featherweight Java: a minimal core calculus for Java and GJ},
 year = {2001},
 issue_date = {May 2001},
 publisher = {Association for Computing Machinery},
 address = {New York, NY, USA},
 volume = {23},
 number = {3},
 issn = {0164-0925},
 url = {https://doi.org/10.1145/503502.503505},
 doi = {10.1145/503502.503505},
 abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.},
 journal = {ACM Trans. Program. Lang. Syst.},
 month = {may},
 pages = {396–450},
 numpages = {55},
 keywords = {Compilation, Java, generic classes, language design, language semantics}
 }
@inproceedings{principalTypes,
  title={What are principal typings and what are they good for?},
  author={Jim, Trevor},
  booktitle={Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={42--53},
  year={1996}
 }
@article{aNormalForm,
  title={Reasoning about programs in continuation-passing style.},
  author={Sabry, Amr and Felleisen, Matthias},
  journal={ACM SIGPLAN Lisp Pointers},
  number={1},
  pages={288--298},
  year={1992},
  publisher={ACM New York, NY, USA}
 }
@InProceedings{PH23,
  author = 	 {Martin Pl{\"u}micke  and Daniel Holle},
  title = 	 {Principal generics in {J}ava--{T}{X}},
  crossref = {kps2023},
  pages = 	 {122--143},
  year = 	 {2023},
  Opteditor = 	 {Thomas Noll and Ira Fesefeldt},
  address = 	 {Aachen},
  Optnumber = 	 {AIB-2023-03},
  month = 	 {September},
  series = {Aachener Informatik-Berichte (AIB)},
  url = {https://publications.rwth-aachen.de/record/972197/files/972197.pdf#%5B%7B%22num%22%3A281%2C%22gen%22%3A0%7D%2C%7B%22name%22%3A%22XYZ%22%7D%2C89.292%2C740.862%2Cnull%5D},
  Optdoi = {10.18154/RWTH-2023-10034},
  Optnote = {(to appear)}
 }
@Proceedings{kps2023,
  booktitle = 	 {22. Kolloquium Programmiersprachen und Grundlagen der Programmierung},
  year = 	 {2023},
  editor = 	 {Noll, Thomas and Fesefeldt, Ira Justus},
  number = 	 {AIB-2023-03},
  series = 	 {Technical report / Department of Computer Science. - Informatik},
  month = 	 {September},
  organization = {RWTH Aachenen},
  doi = {10.18154/RWTH-2023-10034}
 }
@InProceedings{plue24_1,
  author = 	 {Martin Pl{\"u}micke},
  title = 	 {Avoiding the Capture Conversion in {J}ava--{T}{X}},
  crossref =  {HKPTW24},
  pages = 	 {109--115},
  year = 	 {2023}
 }
@proceedings{HKPTW24,
  author = 	 {Daniel Holle and Jens Knoop and Martin Pl\"umicke and Peter Thiemann and Baltasar Tranc\'{o}n y Widemann},
  booktitle = 	 {Proceedings of the 38th and 39th Annual Meeting of the GI Working Group Programming Languages and
 Computing Concepts},
  institution =  {DHBW Stuttgart},
  year = 	 {2024},
  series = 	 {INSIGHTS -- Schriftenreihe der Fakult\"at Technik},
  number = 	 {01/2024},
  ISSN =         {2193-9098},
  url =          {https://www.dhbw-stuttgart.de/forschung-transfer/technik/schriftenreihe-insights}
 }
@article{wells1999typability,
  title={Typability and type checking in System F are equivalent and undecidable},
  author={Wells, Joe B},
  journal={Annals of Pure and Applied Logic},
  volume={98},
  number={1-3},
  pages={111--156},
  year={1999},
  publisher={Elsevier}
 }
--- a/orcid.pdf
+++ b/orcid.pdf
--- a/prolog.tex
+++ b/prolog.tex
@@ -4,17 +4,31 @@
 \lstset{language=Java,
  showspaces=false,
  showtabs=false,
-  breaklines=true,
+  %breaklines=true,
  showstringspaces=false,
-  breakatwhitespace=true,
+  %breakatwhitespace=true,
  basicstyle=\ttfamily\fontsize{8}{9.6}\selectfont, %\footnotesize
  escapeinside={(*@}{@*)},
-  captionpos=b,
+  captionpos=t,float,abovecaptionskip=-\medskipamount
 }
 \lstdefinestyle{fgj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tfgj}{backgroundcolor=\color{lightgray!20}}
 \lstdefinestyle{letfj}{backgroundcolor=\color{lime!20}}
 \lstdefinestyle{tamedfj}{backgroundcolor=\color{yellow!20}}
 \lstdefinestyle{java}{backgroundcolor=\color{lightgray!20}}
 \lstdefinestyle{constraints}{
  basicstyle=\normalfont,
  backgroundcolor=\color{red!20}
 }
 \newtheorem{recap}[note]{Recap}
 \newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
 \newcommand{\tifj}{\texttt{TamedFJ}}
 \newcommand{\wcSep}{\vdash}
 \newcommand\mv[1]{{\tt #1}}
 \newcommand{\ol}[1]{\overline{\tt #1}}
 \newcommand{\exptype}[2]{\mathtt{#1 \texttt{<} #2 \texttt{>} }}
@@ -64,6 +78,9 @@
 \newcommand\subeq{\mathbin{\texttt{<:}}}
 \newcommand\extends{\ensuremath{\triangleleft}}
 \newcommand{\QMextends}[1]{\textrm{\normalshape\ttfamily ?\,extends}\linebreak[0]\,#1}
 \newcommand{\QMsuper}[1]{\textrm{\normalshape\ttfamily ?\linebreak[0]\,su\-per}\linebreak[0]\,#1}
 \newcommand\rulename[1]{\textup{\textsc{(#1)}}}
 \newcommand{\generalizeRule}{General}
@@ -90,7 +107,8 @@
 \newcommand{\constraints}{\ensuremath{\mathit{\overline{c}}}}
 \newcommand{\itype}[1]{\ensuremath{\mathit{#1}}}
 \newcommand{\il}[1]{\ensuremath{\overline{\itype{#1}}}}
-\newcommand{\type}[1]{\mathtt{#1}}
+\newcommand{\gtype}[1]{\type{#1}}
 \newcommand{\type}[1]{\ensuremath{\mathtt{#1}}}
 \newcommand{\anyType}[1]{\mathit{#1}}
 \newcommand{\gType}[1]{\texttt{#1}}
 \newcommand{\mtypeEnvironment}{\ensuremath{\Pi}}
@@ -98,8 +116,11 @@
 \newcommand{\localVarAssumption}{\ensuremath{\mathtt{\eta}}}
 \newcommand{\expandLB}{\textit{expandLB}}
 \newcommand{\letfj}{\textbf{LetFJ}}
 \newcommand{\tph}{\text{tph}}
 \newcommand{\expr}[1]{\texttt{#1}}
 \def\exptypett#1#2{\texttt{#1}\textrm{{\tt <#2}}\textrm{{\tt >}}\xspace}
 \def\exp#1#2{#1(\,#2\,)\xspace}
 \newcommand{\ldo}{, \ldots , }
@@ -112,6 +133,7 @@
 %\newcommand{\wtype}[2]{\ensuremath{[#1\ #2]}}
 \newcommand{\wtv}[1]{\ensuremath{\tv{#1}_?}}
 \newcommand{\ntv}[1]{\ensuremath{\underline{\tv{#1}}}}
 %\newcommand{\ntv}[1]{\tv{#1}}
 \newcommand{\wcstore}{\ensuremath{\Delta}}
 %\newcommand{\rwildcard}[1]{\ensuremath{\mathtt{#1}_?}}
@@ -133,7 +155,6 @@
 \newcommand{\ruleSubstWC}[0]{\rulename{Subst-WC}}
 \newcommand{\subclass}{\mathtt{\sqsubset}\mkern-5mu :}
 \newcommand{\TameFJ}{\text{TameFJ}}
 \newcommand{\TamedFJ}{\textbf{TamedFJ}}
 \newcommand{\TYPE}{\textbf{TYPE}}
--- a/relatedwork.tex
+++ b/relatedwork.tex
@@ -0,0 +1,76 @@
 \section{Related Work}
 Igarashi et al \cite{FJ} define Featherweight Java
 and its generic sibling, Featherweight Generic Java. Their language is
 a functional calculus reduced to the bare essentials, they develop the full metatheory, they
 support generics, and study the type erasing transformation used by
 the Java compiler. Stadelmeier et. al. extends this approach by global type
 inference \cite{TIforFGJ}.
 \subsection{Wildcards in formal Java models}
 Wildcards are first described in a research paper in \cite{addingWildcardsToJava}. In
 \cite{TEP05} the Featherweight Java-Calculus \textsf{Wild~ FJ} is introduced. It
 contains a formal description of wildcards. The Java Language Specification
 \cite{GoJoStBrBuSm23}  refers to \textsf{Wild~FJ} for the introduction of
 wildcards. In \cite{aModelForJavaWithWildcards} a formal model based of explicite existential types
 is introduced and proven as sound. Additionally, for a subset of Java a
 translation to the formal model is given, such that this subset is proven as
 sound. In \cite{WildcardsNeedWitnessProtection} another core calculus is
 introduced, which is proven as 
 sound, too. In this paper it is shown that the unsoundness of Java which is
 discovered in \cite{AT16} is avoidable, even in the absence of nullness-aware type
 system. In \cite{TamingWildcards} finally a framework is presented which combines
 use-site variance (wildcards as in Java) and definition-site variance (as in Scala). For
 instance, it can be used to add use-site variance to Scala and extend the Java
 type system to infer the definition-site variance.
 Our calculus is mixture ...
 \subsection{Type inference}
 Some object-oriented languages like Scala, C\#, and Java perform
 \emph{local} type inference \cite{PT98,OZZ01}. Local type
 inference means that missing type annotations are recovered using only
 information from adjacent nodes in the syntax tree without long distance
 constraints. For instance, the type of a variable initialized with a
 non-functional expression or the return type of a method can be
 inferred. However, method argument types, in particular for recursive
 methods, cannot be inferred by local type inference.
 Milner's algorithm $\mathcal{W}$ \cite{DBLP:journals/jcss/Milner78} is
 the gold standard for global type inference for languages with
 parametric polymorphism, which is used by ML-style languages. The fundamental idea
 of the algorithm is to enforce type equality by many-sorted type
 unification \cite{Rob65,MM82}. This approach is effective and results
 in so-called principal types because many-sorted unification is
 unitary, which means that there is at most one most general result.
 Pl\"umicke \cite{Plue07_3} presents a first attempt to adopt Milner's
 approach to Java. However, the presence of subtyping means that type
 unification is no longer unitary, but still finitary. Thus, there is
 no longer a single most general type, but any type is an instance of a
 finite set of maximal types (for more details see Section
 \ref{sec:unification}). Further work by the same author
 \cite{plue15_2,plue17_2},
 refines this approach by moving to a constraint-based algorithm and by
 considering lambda expressions and Scale-like function types.
 Pluemicke has a different approach to introduce wildcards in \cite{plue09_1}. He
 allows wildcards as any subsitution for type variables and disclaim the
 capture conversion. Instead he extended
 the subtyping ordering such that for $\theta \sub \theta' \sub \theta''$ holds
 indeed the transitiv closure of $\QMextends{\theta} \sub \theta'$ and $\theta' \sub
 \QMsuper{\theta''}$ but not the reflexive closure. He gave a type unification
 algorithm for this type system, which he proved as sound and complete. 
 The problem of his type system is in the lossing reflexivity as shown in
 example \ref{intro-example1}. First approaches to solve this problem he gave in
 \cite{plue24_1}, where he fixes that no pairwise different nodes in the
 abstract syntax gets the same type variable and that no pairwise different type
 variables are equalized. In \cite{PH23} he showed how his type inference
 algorithm suffices theese properties.
 In Pl\"umicke's work there is indeed a formal definition of the subtying
 ordering and a correctness proof of the type unification algorithms but no
 soundness proof of the type system, itself. Therefore we choose for our type
 inference algorithms with wildcars the approach of ???????
--- a/soundness.tex
+++ b/soundness.tex
@@ -1,7 +1,5 @@
 \section{Soundness}
 \newcommand{\CC}{\text{CC}}
 \begin{lemma}
 A sound TypelessFJ program is also sound under LetFJ type rules.
 \begin{description}
@@ -154,7 +152,7 @@ By structural induction over the expression $\texttt{e}$.
    % $\sigma(\ol{\tv{r}}) = \overline{\wcNtype{\Delta}{N}}$,
    % $\ol{N} <: [\ol{S}/\ol{X}]\ol{U}$,
    % TODO: S ok? We could proof $\Delta, \Delta' \overline{\Delta} \vdash \ol{S} \ \ok$
-    % by proofing every substitution in Unify is ok aslong as every type in the inputs is ok
+    % by proving every substitution in Unify is ok aslong as every type in the inputs is ok
    % S ok when all variables are in the environment and every L <: U and U <: Class-bound
    % This can be given by the constraints generated. We can proof if T ok and S <: T and T <: S' then S ok and S' ok
@@ -329,18 +327,17 @@ If there is a solution for a constraint set $C$, then there is also a solution f
 % does this really work. We have to show that the algorithm never gets stuck as long as there is a solution
 % maybe there are substitutions with types containing free variables that make additional solutions possible. Check!
-\begin{lemma}\label{lemma:unifySoundness}
+\begin{lemma}{\unify{} Soundness:}\label{lemma:unifySoundness}
-The \unify{} algorithm only produces correct output.
+\unify{}'s type solutions are correct respective to the subtyping rules defined in figure \ref{fig:subtyping}.
 \begin{description}
 \item[If] $(\sigma, \Delta) = \unify{}( \Delta', \, \overline{ \type{S} \lessdot \type{T} } \cup \overline{ \type{S'} \lessdotCC \type{T'} } )$ %\cup \overline{ \type{S} \doteq \type{S'} })$
-%\item[and] $fv(\overline{ \type{S} }) = \emptyset$, $fv(\overline{ \type{T} }) = \emptyset$
+\item[Then] there exists a substitution $\sigma'$ and a set of types $\overline{\wcNtype{\Delta}{N}}$ with:
-\item[Then] there exists a $\sigma'$ with:
+\begin{itemize}
-$\sigma \subseteq \sigma'$ and
+\item $\sigma \subseteq \sigma'$
-$\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S}) <: \sigma'(\type{T})}$
-and $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$ where $\overline{\sigma(\type{S'}) = \wcNtype{\Delta}{N}}$,
+\item $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \wcNtype{\Delta}{N}}$ 
-otherwise $\Delta, \Delta' \vdash \overline{\sigma'(\type{S'}) <: \sigma'(\type{T'})}$
+\item $\Delta, \Delta', \overline{\Delta} \vdash \overline{\type{N} <: \sigma'(\type{T'})}$
-% and $\sigma(\type{T'}) = \sigma(\type{T'})$.
+\end{itemize}
 \end{description}
 \end{lemma}
@@ -378,6 +375,7 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \begin{description}
 \item[AddDelta] $C$ is not changed
 \item[GenDelta] by definition, S-Var-Left, and S-Trans %The generated type variable is unique due to the solved form property. %and the solved form property (no $\tv{a}$ in $C$)
 \item[GenDelta'] same as GenDelta by setting $\sigma'(\wtv{b}) = \rwildcard{B}$
 \item[GenSigma] by definition and S-Refl.
 % holds for $\set{\tv{a} \doteq \type{G}}$ by definition.
 % Holds for $C$ by assumption and because $\tv{a} \notin C$ by solved form definition ($[\type{G}/\tv{a}]C = C$).
@@ -388,6 +386,8 @@ $\Delta \vdash  \sigma(C') \implies \Delta \vdash \sigma(C)$
 \item[Settle] Assumption, S-Trans
 \item[Super] S-Extends ($\vdash \wctype{\Delta}{C}{\ol{T}} <: \wctype{\Delta}{D}{[\ol{T}/\ol{X}]\ol{N}}$), S-Trans
 \item[\generalizeRule{}] by Assumption, because $C \subset C'$
 \item[Same] by S-Exists
 \item[SameW] %TODO
 \item[Adapt] Assumption, S-Extends, S-Trans
 \item[Adopt] Assumption, because $C \subset C'$
 %\item[Capture, Reduce] are always applied together. We have to destinct between two cases:
@@ -424,7 +424,7 @@ Therefore we can say that $\Delta, \Delta', \overline{\Delta} \vdash \sigma'(\ex
 % List<X> <. Y.List<Y>, free variables are either in 
 If $\text{fv}(\exptype{C}{\ol{S}}) = \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) = \emptyset$ the preposition holds by Assumption and S-Exists.
 Otherwise 
-$\Delta' \vdash \CC{}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
+$\Delta' \vdash \text{CC}(\sigma(\exptype{C}{\ol{S}})) <: \sigma(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}})$
 holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}(\wctype{\overline{\wildcard{A}{\type{U}}{\type{L}}}}{C}{\ol{T}}) ) \subseteq \text{dom}(\Delta') $.
 \item[Match] Assumption, S-Trans
 \item[Trim] Assumption and S-Exists
@@ -432,7 +432,8 @@ holds with any $\Delta'$ so that $(\text{fv}(\exptype{C}{\ol{S}}) \cup \text{fv}
 \item[Circle] S-Refl
 \item[Swap] by definition
 \item[Erase] S-Refl
-\item[Equals] %by definition
+\item[Equals] by definition \ref{def:equal}
 %by definition
 %TODO
 % Unify does never contain wildcard environments with unused wildcards. Therefore after N <: N' and N' <: N, both types have the same wildcard environment
--- a/splncs04.bst
+++ b/splncs04.bst
--- a/tRules.tex
+++ b/tRules.tex
@@ -1,20 +1,43 @@
 \section{Syntax and Typing}
-The input syntax for our algorithm is shown in figure \ref{fig:syntax}
+\section{\TamedFJ{}}\label{sec:tifj}
 %LetFJ -> Output language!
 %TamedFJ -> ANF transformed input langauge
 %Input language only described here. It is standard Featherweight Java
 % we use the transformation to proof soundness. this could also be moved to the end. 
 % the constraint generation step assumes every method argument to be encapsulated in a let statement. This is the way Java is doing capture conversion
 The input to our algorithm is a typeless version of Featherweight Java.
 The syntax is shown in figure \ref{fig:syntax}
 and the respective type rules in figure \ref{fig:expressionTyping} and \ref{fig:typing}.
 Method parameters and return types are optional.
 We still require type annotations for fields and generic class parameters.
 This is a design choice by us,
 as we consider them as data declarations which are given by the programmer.
 % They are inferred in for example \cite{plue14_3b}
 Note the \texttt{new} expression not requiring generic parameters,
 which are also inferred by our algorithm.
 The method call naturally has type inferred generic parameters aswell.
 We add the elvis operator ($\elvis{}$) to the syntax mainly to showcase applications involving wildcard types.
 The syntax is described in figure \ref{fig:syntax} with optional type annotations highlighted in yellow.
 It is possible to exclude all optional types.
 \TamedFJ{} is a subset of the calculus defined by \textit{Bierhoff} \cite{WildcardsNeedWitnessProtection}.
 %The language is designed to showcase type inference involving existential types.
 The idea is for our type inference algorithm to calculate all missing types and output a fully and correctly typed \TamedFJ{} program,
 which by default is also a correct Featherweight Java program (see chapter \ref{sec:soundness}).
-Our algorithm is an extension of the \emph{Global Type Inference for Featherweight Generic Java}\cite{TIforFGJ} algorithm.
+\noindent
-The input language is designed to showcase type inference involving existential types.
+\textit{Notes:}
-Method call rule T-Call is the most interesting part, because it emulates the behaviour of a Java method call,
+\begin{itemize}
-where existential types are implicitly \textit{opened} and \textit{closed}.
+\item The calculus does not include method overriding for simplicity reasons.
 %The T-Elvis rule mimics the type judgement of a branch expression like \texttt{if-else}.
 %and is solely used for examples.
 The calculus does not include method overriding for simplicity reasons.
 Type inference for that is described in \cite{TIforFGJ} and can be added to this algorithm accordingly.
-Our algorithm is designed for extensibility with the final goal of full support for Java.
+%\textit{Note:}
-\unify{} is the core of the algorithm and can be used for any calculus sharing the same subtype relations as depicted in \ref{fig:subtyping}.
+\item The typing rules for expressions shown in figure \ref{fig:expressionTyping} refrain from restricting polymorphic recursion.
-Additional language constructs can be added by implementing the respective constraint generation functions in the same fashion as described in chapter \ref{chapter:constraintGeneration}.
+Type inference for polymorphic recursion is undecidable \cite{wells1999typability} and when proving completeness like in \cite{TIforFGJ} the calculus
 needs to be restricted in that regard.
 Our algorithm is not complete (see discussion in chapter \ref{sec:completeness}) and without the respective proof we can keep the \TamedFJ{} calculus as simple as possible
 and as close to it's Featherweight Java correspondent \cite{WildcardsNeedWitnessProtection} as possible.
 Our soundness proof works either way.
 \end{itemize}
 %Additional features like overriding methods and method overloading can be added by copying the respective parts from there.
 %Additional features can be easily added by generating the respective constraints (Plümicke hier zitieren)
@@ -26,32 +49,37 @@ Additional language constructs can be added by implementing the respective const
 % on overriding methods, because their type is already determined.
 % Allowing overriding therefore has no implication on our type inference algorithm.
 % The output is a valid Featherweight Java program.
 % We use the syntax of the version introduced in \cite{WildcardsNeedWitnessProtection}
 % calling it \letfj{} for that it is a Featherweight Java variant including \texttt{let} statements.
 \newcommand{\highlight}[1]{\begingroup\fboxsep=0pt\colorbox{yellow}{$\displaystyle #1$}\endgroup}
 \begin{figure}
 \par\noindent\rule{\textwidth}{0.4pt}
 \center
 $
 \begin{array}{lrcl}
-\hline
+%\hline
 \text{Parameterized classes} & \mv N & ::= & \exptype{C}{\ol{T}} \\
 \text{Types} & \type{S}, \type{T}, \type{U} & ::= & \type{X} \mid \wcNtype{\Delta}{N} \\
 \text{Lower bounds} & \type{K}, \type{L} & ::= & \type{T} \mid \bot \\
 \text{Type variable contexts} &  \Delta & ::= & \overline{\wildcard{X}{T}{L}} \\
 \text{Class declarations} &  D & ::= & \texttt{class}\ \exptype{C}{\ol{X \triangleleft T}} \triangleleft \type{N} \set{\overline{\type{T}\ f}; \ol{M}} \\
-\text{Method declarations} &  \texttt{M} & ::= & \generics{\ol{X \triangleleft T}} \type{T} \ \texttt{m}(\overline{\type{T}\ x}) = t \\
+\text{Method declarations} &  \texttt{M} & ::= & \highlight{\generics{\overline{\type{X} \triangleleft \type{N}}}}\ \highlight{\type{T}}\ \texttt{m}(\overline{\highlight{\type{T}}\ \expr{x}}) \{ \texttt{return} \ \expr{e}; \} \\
-\text{Terms} & t & ::= & x \\
+\text{Terms} & \expr{e} & ::= & \expr{x} \\
-& & \ \ | & \texttt{new} \ \exptype{C}{\ol{T}}(\overline{t})\\
+& & \ \ | & \texttt{new} \ \type{C}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
-& & \ \ | & t.f\\
+& & \ \ | & \expr{e}.f\\
-& & \ \ | & t.\generics{\ol{T}}\texttt{m}(\overline{t})\\
+& & \ \ | & \expr{e}.\texttt{m}\highlight{\generics{\ol{T}}}(\overline{\expr{e}})\\
-& & \ \ | & t \elvis{} t\\
+& & \ \ | & \texttt{let}\ \expr{x} \highlight{: \wcNtype{\Delta}{N}} = \expr{e} \ \texttt{in} \ \expr{e}\\
-\text{Variable contexts} & \Gamma & ::= & \overline{x:\type{T}}\\
+& & \ \ | & \expr{e} \elvis{} \expr{e}\\
-\hline
+\text{Variable contexts} & \Gamma & ::= & \overline{\expr{x}:\type{T}}\\
 %\hline
 \end{array}
 $
-\caption{Input Syntax}\label{fig:syntax}
+\par\noindent\rule{\textwidth}{0.4pt}
 \caption{Input Syntax with optional type annotations}\label{fig:syntax}
 \end{figure}
 % Each class type has a set of wildcard types $\overline{\Delta}$ attached to it.
 % The type $\wctype{\overline{\Delta}}{C}{\ol{T}}$ defines a set of wildcards $\overline{\Delta}$,
 % which can be used inside the type parameters $\ol{T}$.
 \begin{figure}[tp]
 \begin{center}
 $\begin{array}{l}
@@ -109,7 +137,7 @@ $\begin{array}{l}
        \Delta', \Delta \vdash [\ol{T}/\ol{\type{X}}]\ol{L} <: \ol{T} \quad \quad
        \Delta', \Delta \vdash \ol{T} <: [\ol{T}/\ol{\type{X}}]\ol{U} \\
        \text{fv}(\ol{T}) \subseteq \text{dom}(\Delta, \Delta') \quad
-        \text{dom}(\Delta') \cap \text{fv}(\wctype{\ol{\wildcard{X}{U}{L}}}{C}{\ol{S}}) = \emptyset
+        \text{dom}(\Delta') \cap \text{fv}(\wcNtype{\ol{\wildcard{X}{U}{L}}}{N}) = \emptyset
        \\
        \hline
    \vspace*{-0.3cm}\\
@@ -184,125 +212,115 @@ $\begin{array}{l}
 $\begin{array}{l}
    \typerule{T-Field}\\
    \begin{array}{@{}c}
-        \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
+        \Delta | \Gamma \vdash \expr{v} : \type{T} \quad \quad 
-        \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
+        \Delta \vdash \type{T} <: \wcNtype{}{N} \quad \quad
        \textit{fields}(\type{N}) = \ol{U\ f} \\
 \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
 \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
 \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
+        \Delta | \Gamma \vdash \expr{v}.\texttt{f}_i : \type{U}_i
    \end{array}
 \end{array}$
 \\[1em]
 % $\begin{array}{l}
 %     \typerule{T-Field}\\
 %     \begin{array}{@{}c}
 %         \Delta | \Gamma \vdash \texttt{e} : \type{T} \quad \quad 
 %         \Delta \vdash \type{T} <: \wcNtype{\Delta'}{N} \quad \quad
 %         \textit{fields}(\type{N}) = \ol{U\ f} \\
 % \Delta, \Delta' \vdash \type{U}_i <: \type{S} \quad \quad
 % \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
 % \Delta \vdash \type{S}, \wcNtype{\Delta'}{N} \ \ok
 %         \\
 %         \hline
 %     \vspace*{-0.3cm}\\
 %         \Delta | \Gamma \vdash \texttt{e}.\texttt{f}_i : \type{S}
 %     \end{array}
 % \end{array}$
 % \\[1em]
 % $\begin{array}{l}
 %     \typerule{T-New}\\
 %     \begin{array}{@{}c}
 %         \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
 %         \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
 %         \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
 %         \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
 %         \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
 %         \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
 %         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
 %         \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
 %         \\
 %         \hline
 %     \vspace*{-0.3cm}\\
 %         \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
 %     \end{array}
 % \end{array}$
 % \\[1em] 
 $\begin{array}{l}
    \typerule{T-New}\\
    \begin{array}{@{}c}
        \Delta, \overline{\Delta} \vdash  \exptype{C}{\ol{T}} \ \ok \quad \quad
-        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} \quad \quad
+        \Delta \vdash  \overline{\type{S}} <: \overline{\type{U}} \\
-        \Delta | \Gamma \vdash \overline{t : \type{S}} \quad \quad
+        \Delta | \Gamma \vdash \overline{\expr{v} : \type{S}} \quad \quad
-        \Delta \vdash  \overline{\type{S}} <: \overline{\wcNtype{\Delta}{N}} \\
+        \text{fields}(\exptype{C}{\ol{T}}) = \overline{\type{U}\ f} 
        \Delta, \overline{\Delta} \vdash  \overline{\type{N}} <: \overline{\type{U}} \quad \quad
        \Delta, \overline{\Delta} \vdash \exptype{C}{\ol{T}} <: \type{T} \quad \quad
        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})} \quad \quad
        \Delta \vdash \type{T},  \overline{\wcNtype{\Delta}{N}} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{t}) : \exptype{C}{\ol{T}}
+        \triangle | \Gamma \vdash \texttt{new}\ \type{C}(\ol{v}) : \exptype{C}{\ol{T}}
    \end{array}
 \end{array}$
-\\[1em] % TODO: we need subtyping for FJ without let statements. Problem is \Delta \vdash T witnessed. The \Delta here contains all the let statements beforehand.
+\hfill
-% TODO: maybe do a rule which adds let statements at any place! Goal: a program which Unify calculates a type for is also correct under our type laws and can be converted to LefFJ
+% $\begin{array}{l}
-% motivation: do not use normal types as intermediate types. Keep a Pair<X,X> as that and not convert to X,Y.Pair<X,Y>
+%     \typerule{T-Call}\\
-% it is possible because the parameters of the method are normal types. we can start capture converting them
+%     \begin{array}{@{}c}
-% is it possible to say there exists any \Delta which makes the method body possible?
+%         \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
 %         \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
 %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
 %         \\
 %         \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
 %         \Delta | \Gamma \vdash  \texttt{e}, \ol{e} : \ol{T} \quad \quad
 %         \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
 %         \\
 %         \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
 %         \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
 %         \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
 %         \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
 %         \\
 %         \hline
 %     \vspace*{-0.3cm}\\
 %         \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
 %     \end{array}
 % \end{array}$
 % \\[1em]
 $\begin{array}{l}
    \typerule{T-Call}\\
    \begin{array}{@{}c}
-        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\type{T}} \ \ok \quad \quad
+        \generics{\ol{X \triangleleft U'}} \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
        \Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
        \generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
        \\
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
        \Delta | \Gamma \vdash \texttt{e} : \type{T}_r \mid \Delta_G \quad \quad
        \Delta | \Gamma \vdash \ol{e} : \ol{T} \mid \overline{\Delta_G} \quad \quad
        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
        \\
        \overline{\Delta_G}, \Delta_G, \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \Delta', \overline{\Delta}
    \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
    \typerule{T-Call}\\
    \begin{array}{@{}c}
        \Delta \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
        \generics{\ol{X \triangleleft U'}}\ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
        \Delta \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
        \\
        \Delta \vdash \ol{S} \ \ok \quad \quad
-        \Delta | \Gamma \vdash \texttt{e}, \ol{e} : \ol{T} \mid \overline{\Delta'} \quad \quad
+        \Delta | \Gamma \vdash  \expr{v}, \ol{v} : \ol{T} \quad \quad
-        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad
+        \Delta \vdash \ol{T} <: [\ol{S}/\ol{X}]\ol{U} 
        \Delta \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T}
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T} \mid \overline{\Delta}, \overline{\Delta'}
+        \Delta | \Gamma \vdash \expr{v}.\texttt{m}(\ol{v}) : \type{T}
    \end{array}
 \end{array}$
 % \Delta is not allowed to have wildcards depending on eachother. X^Y, Y^T for example
 \\[1em]
 $\begin{array}{l}
-    \typerule{T-Call}\\
+    \typerule{T-Let}\\
    \begin{array}{@{}c}
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
+        \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
-        \generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
+        \Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'}
        \\
-        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok \quad \quad
+        \Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
-        \Delta | \Gamma \vdash \texttt{e} : \type{T}_r \quad \quad
+        \Delta, \Delta' \vdash  \type{T}_2 <: \type{T} \quad \quad
        \Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
        \Delta \vdash \type{T}_r <: \wcNtype{\Delta'}{N} \quad \quad
        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}}
        \\
        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
        \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
        \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
-        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
+        \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \Delta | \Gamma \vdash \texttt{e}.\texttt{m}(\ol{e}) : \type{T}
+        \Delta | \Gamma \vdash \texttt{let}\ \expr{x} = \expr{t}_1 \ \texttt{in} \ \expr{t}_2 : \type{T}
    \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
    \typerule{T-Call}\\
    \begin{array}{@{}c}
        \Delta, \Delta', \overline{\Delta} \vdash \ol{\type{N}} <: [\ol{S}/\ol{X}]\ol{U} \quad \quad
        \generics{\ol{X \triangleleft U'}} \type{N} \to \ol{U} \to \type{U} \in \Pi(\texttt{m}) \quad \quad
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} <: [\ol{S}/\ol{X}]\ol{U'} \quad \quad
        \Delta, \Delta', \overline{\Delta} \vdash \ol{S} \ \ok 
        \\
        \Delta | \Gamma \vdash \ol{e} : \ol{T} \quad \quad
        \Delta \vdash \ol{T} <: \overline{\wcNtype{\Delta}{N}} \quad \quad 
        \Delta \vdash \type{T}, \overline{\wcNtype{\Delta}{N}} \ \ok \quad \quad
        \Delta, \Delta', \overline{\Delta} \vdash [\ol{S}/\ol{X}]\type{U} <: \type{T} \quad \quad
        \overline{\text{dom}(\Delta) \subseteq \text{fv}(\type{N})}
        \\
        \hline
    \vspace*{-0.3cm}\\
        \Delta | \Gamma \vdash \texttt{m}(\ol{e}) : \type{T}
    \end{array}
 \end{array}$
 \\[1em]
@@ -325,30 +343,13 @@ $\begin{array}{l}
 \begin{figure}
 \begin{center}
    $\begin{array}{l}
        \typerule{T-Method}\\
 % TODO: do a rule that forbids variables in Delta which are not introduced by a capture conversion
        \begin{array}{@{}c}
            \exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
            \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
            \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
            \text{dom}(\triangle) = \ol{X} \quad \quad
            %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
            \mathtt{\Pi} | \triangle, \triangle', \overline{\triangle} | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \mid \overline{\Delta} \quad \quad 
            \triangle \vdash \type{S} <: \type{T}
            \\
            \hline
        \vspace*{-0.3cm}\\
            \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
        \end{array}
    \end{array}$
    \\[1em]
 $\begin{array}{l}
    \typerule{T-Method}\\
    \begin{array}{@{}c}
-        \exptype{C}{\ol{X}} \to \ol{T} \to \type{T} \in \mathtt{\Pi}(\texttt{m})\quad \quad
+        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \set{\ldots} \quad \quad 
-        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \quad \quad
+        \generics{\ol{Y \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T}) \to \type{T} \in \mathtt{\Pi}(\texttt{m}) \quad \quad
-        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \\
+        \triangle' =  \overline{\type{Y} : \bot .. \type{P}} \\
        \triangle, \triangle' \vdash \ol{P}, \type{T}, \ol{T} \ \ok \quad \quad
        \text{dom}(\triangle) = \ol{X} \quad \quad
        %\texttt{class}\ \exptype{C}{\ol{X \triangleleft \_ }} \triangleleft \type{N} \ \{ \ldots \} \\
        \mathtt{\Pi} | \triangle, \triangle' | \ol{x : T}, \texttt{this} : \exptype{C}{\ol{X}} \vdash \texttt{e} : \type{S} \quad \quad 
@@ -356,37 +357,33 @@ $\begin{array}{l}
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) = \texttt{e} \ \ok \text{ in C with } \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \texttt{m}(\ol{x}) \set{ \texttt{return}\ \texttt{e}; } \ \ok \ \text{in C}
    \end{array}
 \end{array}$
 \\[1em]
 $\begin{array}{l}
    \typerule{T-Class}\\
    \begin{array}{@{}c}
-        \mathtt{\Pi}' = \mathtt{\Pi} \cup \set{ \exptype{C}{\ol{X}}.\texttt{m} : \ol{T}_\texttt{m} \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M}} \\
+        %\forall \texttt{m} \in \ol{M} : \mathtt{\Pi}(\texttt{m}) = \generics{\ol{X \triangleleft \type{N}}}(\exptype{C}{\ol{X}},\ol{T_\texttt{m}}) \to \type{T}_\texttt{m} \\
        \mathtt{\Pi}'' = \mathtt{\Pi} \cup \set{ \exptype{C}{\ol{X}}.\texttt{m} :
            \generics{\ol{X \triangleleft \type{N}}, \ol{Y \triangleleft P}}\ol{T}_\texttt{m} \to \type{T}_\texttt{m} \mid \texttt{m} \in \ol{M} } \\
        \triangle = \overline{\type{X} : \bot .. \type{U}} \quad \quad
        \triangle \vdash \ol{U}, \ol{T}, \type{N} \ \ok \quad \quad
-        \mathtt{\Pi}' | \triangle \vdash \ol{M} \ \ok \text{ in C with} \ \generics{\ol{Y \triangleleft P}}
+        \mathtt{\Pi} | \triangle \vdash \ol{M} \ \ok \text{ in C}
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \}  : \mathtt{\Pi}''
+        \mathtt{\Pi} \vdash \texttt{class}\ \exptype{C}{\ol{X \triangleleft U}} \triangleleft \type{N} \{ \ol{T\ f}; \ol{M} \} 
    \end{array}
 \end{array}$
-\\[1em]
+%\\[1em]
 \hfill
 $\begin{array}{l}
    \typerule{T-Program}\\
    \begin{array}{@{}c}
-        \emptyset \vdash \texttt{L}_1 : \mathtt{\Pi}_1 \quad \quad 
+        \mathtt{\Pi} = \overline{\texttt{m} : \generics{\ol{X \triangleleft \type{N}}}\ol{T} \to \type{T}}
        \mathtt{\Pi}_1 \vdash \texttt{L}_2 : \mathtt{\Pi}_1 \quad \quad 
        \ldots \quad \quad 
        \mathtt{\Pi}_{n-1} \vdash \texttt{L}_n : \mathtt{\Pi}_n \quad \quad 
        \\
        \hline
    \vspace*{-0.3cm}\\
-        \vdash \ol{L} : \mathtt{\Pi}_n
+    \mathtt{\Pi} \vdash \overline{D}
    \end{array}
 \end{array}$
 \end{center}
@@ -409,4 +406,5 @@ $\begin{array}{l}
        \text{fields}(\exptype{C}{\ol{T}}) = \ol{U\ g}, [\ol{T}/\ol{X}]\ol{S\ f}
    \end{array}
 \end{array}$
 \caption{Field access}
 \end{figure}
--- a/todo-11.4.24
+++ b/todo-11.4.24
@@ -0,0 +1,16 @@
 - Eingangsbeispiel
 - Motivation (gibt es ein nicht funktionierendes Beispiel für lokale Typinferenz was mit unserem algorithmus funktioniert)
 - Zeile 52 steht LetFJ, muss eingeführt werden
 	- Operatoren motivieren. Denotable expressable types
 	Java macht CC implizit. Wir machen es mit let statements. Dadurch LetFJ einführen
 	- Java macht es anders. es gibt keine let statements
 	- In java kann ich die lets nur in bestimmter Weise einbauen. Die ANF Transformation macht aus TamedFJ das letFJ
 - constraints nicht zu früh erwähnen
 	- informal erwähnen. um capture conversion zu behandeln braucht es neue constraints
 	- ganz vorne auflisten. Capture Conversion ist eine Neuheit
 Figure 4 und 5 in ein Bild
 - man könnte die syntax unterlegen und sagen die unterlegten elemente fallen weg
 - in beiden Syntaxen die Methodendeklarationen sollen gleich sein. beides return benutzen
 	- anschließend bei der convertierung zu TamedFJ nur die Änderungen beschreiben (Änderungen nur in Expressions)
--- a/unify.tex
+++ b/unify.tex
Author	SHA1	Message	Date
JanUlrich	42d8afce35	Restructure and Cleanup Unify	2024-05-27 16:07:24 +02:00
JanUlrich	0f1e7d0199	Let statement and capture conversion introduction	2024-05-27 02:57:15 +02:00
JanUlrich	4c67504ba1	Restructure. Add to Introduction and cleanup	2024-05-24 22:25:31 +02:00
JanUlrich	9f088eb29d	Global Type Inference Intro	2024-05-23 16:45:40 +02:00
Andreas Stadelmeier	b2ca8e49df	Restructure	2024-05-23 14:18:50 +02:00
JanUlrich	2f5aa753e0	Add 4 steps of TI introduction	2024-05-22 16:08:03 +02:00
JanUlrich	95636f3379	Match example	2024-05-22 12:06:51 +02:00
Andreas Stadelmeier	a74e20802c	Cleanup. Explain \Ðelta_in	2024-05-21 20:53:15 +02:00
Andreas Stadelmeier	04fc640903	Rework Capture COnstraints chapter	2024-05-21 19:16:13 +02:00
JanUlrich	6a679f8ab0	Cleanup. Change intro example	2024-05-17 20:28:15 +02:00
JanUlrich	11dd427c3f	Add Prepare explanation. Restructure	2024-05-17 19:18:53 +02:00
JanUlrich	4890fa79c2	Change to LLNCS style	2024-05-17 13:30:21 +02:00
Andreas Stadelmeier	724f9ab328	Restructure, Add Explanation für Wildcard Reduce Rules and Unify Intro	2024-05-17 11:56:35 +02:00
Andreas Stadelmeier	ed8895f0b5	Fix	2024-05-16 10:44:36 +02:00
Andreas Stadelmeier	1fd7c56391	Add Capture Constraint are not reflexive explanation	2024-05-15 23:59:04 +02:00
Andreas Stadelmeier	9e0d9ddd18	Fixes and TODO	2024-05-14 16:35:30 +02:00
JanUlrich	bdfacdf3dd	Add Syntax for Constraints	2024-05-14 15:15:02 +02:00
Andreas Stadelmeier	81f44caac1	WIP	2024-05-14 14:57:16 +02:00
Andreas Stadelmeier	b1d3c4d525	Restructure challenges	2024-05-14 13:32:06 +02:00
Andreas Stadelmeier	8c6085f3b1	Fix	2024-05-14 13:31:54 +02:00
Andreas Stadelmeier	77f3fbedfa	Cleanup and Restructure. Remove polymorphic recursion exclusion from Type Rules	2024-05-13 23:58:42 +02:00
Andreas Stadelmeier	5f33fa4711	Cleanup and intro to Type INference	2024-05-13 00:17:49 +02:00
JanUlrich	fc508cf331	Local vs Global TI	2024-05-11 09:48:04 +02:00
JanUlrich	3a7c862fd2	Change Introductin Layout	2024-05-08 16:57:58 +02:00
JanUlrich	2dae79053c	Explain let	2024-05-07 23:49:07 +02:00
Andreas Stadelmeier	6c8b78914f	Intro Wildcards	2024-05-07 16:14:48 +02:00
Andreas Stadelmeier	38589f804c	Typo	2024-05-07 15:29:15 +02:00
JanUlrich	b5f7345e51	Rephrase Wildcard Intro	2024-05-07 11:30:45 +02:00
JanUlrich	b432c5b091	Add Wildcard introduction	2024-05-06 18:15:24 +02:00
Andreas Stadelmeier	5cd90a9593	Start Wildcard elimination example	2024-05-06 12:11:57 +02:00
Andreas Stadelmeier	72dff3fa36	Finish someList example	2024-05-04 13:56:55 +02:00
JanUlrich	4a3e39ad9e	Same rule example	2024-05-03 17:37:43 +02:00
JanUlrich	3f490f9b6e	Fix New Constraint generation	2024-05-03 17:37:26 +02:00
Andreas Stadelmeier	883969c067	Example	2024-05-02 16:42:15 +02:00
JanUlrich	b9ef35526f	Unify example	2024-05-02 16:14:35 +02:00
JanUlrich	4ec030d731	Fix Syntax def	2024-05-02 16:14:00 +02:00
JanUlrich	85fd47eb6a	Start Wildcard creation example	2024-05-01 21:37:27 +02:00
JanUlrich	52f1cf631f	Add Challenge 4. Wildcards are not allowed to leave their scope	2024-04-30 16:21:20 +02:00
Andreas Stadelmeier	76b800d953	Add rulenameAfter command	2024-04-24 17:30:15 +02:00
Andreas Stadelmeier	585254d814	WIP	2024-04-24 08:33:58 +02:00
Andreas Stadelmeier	295f1ee567	Cleanup CC command	2024-04-23 21:32:41 +02:00
Andreas Stadelmeier	c42477bf8a	Fix	2024-04-21 13:09:13 +02:00
JanUlrich	9035c5faf1	Cleanup motivation	2024-04-19 11:47:21 +02:00
Andreas Stadelmeier	df22ed5cce	Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ	2024-04-17 17:13:38 +02:00
Andreas Stadelmeier	6d594b056b	Change Method declaration syntax	2024-04-17 17:13:35 +02:00
JanUlrich	0c51692936	Intro	2024-04-17 16:45:24 +02:00
Andreas Stadelmeier	6702d9b0cb	Java local Type inference intro	2024-04-17 12:59:31 +02:00
Andreas Stadelmeier	bbe5d4f065	Fix Input/Output syntax	2024-04-17 00:11:16 +02:00
JanUlrich	91f42d26f6	Motivation example	2024-04-16 19:27:56 +02:00
JanUlrich	ed988fdacf	Motivation: comparision to local type inference	2024-04-15 15:45:16 +02:00
pl@gohorb.ba-horb.de	4c9e639c71	modified: martin.bib	2024-04-12 19:49:41 +02:00
pl@gohorb.ba-horb.de	2825f120ea	modified: martin.bib modified: relatedwork.tex	2024-04-12 19:42:11 +02:00
pl@gohorb.ba-horb.de	4ef46f3273	modified: martin.bib	2024-04-12 01:09:40 +02:00
pl@gohorb.ba-horb.de	75dc20366d	modified: TIforWildFJ.tex modified: martin.bib modified: prolog.tex new file: relatedwork.tex	2024-04-12 00:25:47 +02:00
JanUlrich	f5ddc65497	Motivationsbeispiel	2024-04-11 18:02:25 +02:00
Andreas Stadelmeier	5bcffb7d70	Add TODO. Fix introduction example (WIP). Add explanation to UNify (WIP)	2024-04-11 13:18:54 +02:00
Andreas Stadelmeier	24cfd8cb75	Rephrase Triple example	2024-04-10 17:43:04 +02:00
JanUlrich	b78594cf39	Triple example	2024-04-10 15:35:27 +02:00
Andreas Stadelmeier	9285f7b394	example Pair and Triple	2024-04-10 12:59:43 +02:00
JanUlrich	b577881d92	Pair example	2024-04-10 11:27:53 +02:00
Andreas Stadelmeier	3a9f2d3e16	Remove Same rule. SameW rule is for both constraints	2024-04-10 01:16:24 +02:00
JanUlrich	4b183937f5	Comments	2024-04-08 22:51:06 +02:00
JanUlrich	079bb914e4	Explain let scoping in unify	2024-04-08 21:45:54 +02:00
JanUlrich	5718c42e28	Change principal type problem in introduction	2024-04-08 21:45:29 +02:00
Andreas Stadelmeier	2b41b56498	COmments and Flatten rule. Description for step 3	2024-04-07 19:52:39 +02:00
JanUlrich	2273acadad	FIx	2024-04-05 12:24:42 +02:00
JanUlrich	ed58017551	Wildcard placeholders	2024-04-04 14:38:16 +02:00
JanUlrich	0c89f28b18	Comments	2024-04-03 21:01:32 +02:00
JanUlrich	41a01d3abc	Fix S-Exists	2024-04-03 21:01:21 +02:00
JanUlrich	e562c65774	Merge branch 'master' of ssh://gitea.hb.dhbw-stuttgart.de:2222/stan/Ecoop2024_TIforWildFJ	2024-04-03 15:54:24 +02:00
JanUlrich	21328a3d05	Unify	2024-04-03 15:54:08 +02:00
Andreas Stadelmeier	a151415950	SameW rule soundness	2024-04-03 00:45:51 +02:00
Andreas Stadelmeier	87f413241a	Add ANF transformation. Define LetFJ. Change Constraint generation. Cleanup old explanation of Capture conversion. Add example to Constraint generation	2024-03-30 00:07:26 +01:00
Andreas Stadelmeier	7b86dc0cf3	Add ANF transformation. Change syntax of TamedFJ. Restructure Unify description. Some fixes in Unify	2024-03-28 03:40:39 +01:00
Andreas Stadelmeier	495e37b370	Fix Type Substitution	2024-03-27 14:12:50 +01:00
Andreas Stadelmeier	cec613b875	Fix	2024-03-27 01:55:19 +01:00
Andreas Stadelmeier	032baaacb8	Cleanup Unify. Add explanation to adopt rule and add lessdot markers	2024-03-27 01:54:08 +01:00
Andreas Stadelmeier	e93a762441	Add Wildcard Environment to intro Unify example	2024-03-27 01:53:23 +01:00
Andreas Stadelmeier	9556f1521e	Cleanup. Define mutual subtyping as equality	2024-03-26 15:41:48 +01:00
Andreas Stadelmeier	e40693a7de	Remove comments (cleanup). Add Clear and Exclude rules. Change Unify Soundness premise	2024-03-25 19:12:35 +01:00
Andreas Stadelmeier	f2002ea833	Add GenDelta for WTVS. Restructure step 2. Comment out old version	2024-03-25 14:09:46 +01:00
Andreas Stadelmeier	17559170d0	LessDotCC constraints stay preserved	2024-03-19 20:52:04 +01:00
Andreas Stadelmeier	e9f86ffda3	Add A-Normal Form transform	2024-03-18 14:57:56 +01:00
JanUlrich	e7b6786f08	Add Syntax and type rules for a normal form	2024-03-15 17:37:58 +01:00
Andreas Stadelmeier	03a7420348	Fix and comment	2024-03-13 18:51:44 +01:00
Andreas Stadelmeier	ad34a5dd00	gitignore	2024-03-13 00:37:23 +01:00
Andreas Stadelmeier	c7212cd7c6	Introduce new challenge (principal type). Restructure and remove some parts.	2024-03-13 00:30:16 +01:00
JanUlrich	9a7195d261	Add reference	2024-03-11 18:02:44 +01:00
JanUlrich	0560611304	Add Example infinite types	2024-03-11 18:02:31 +01:00
Andreas Stadelmeier	f6cb46af4a	Recap	2024-03-11 13:17:41 +01:00
Andreas Stadelmeier	9daf5ce8ef	Fix	2024-03-07 10:00:10 +01:00
Andreas Stadelmeier	5055364de5	Add Recap in introduction	2024-03-07 03:32:56 +01:00
JanUlrich	b1ce0f771b	Comments to TI Capture Conversion	2024-03-06 19:28:33 +01:00
Andreas Stadelmeier	903b2405b1	Add T-Elvis rule	2024-03-06 16:08:12 +01:00
Andreas Stadelmeier	323f2c0163	Fix T-Class method env	2024-03-06 14:20:17 +01:00
JanUlrich	ecd2975129	Add to constraints intro	2024-03-06 09:36:36 +01:00
Andreas Stadelmeier	e49b87b549	Fix input syntax	2024-03-06 00:37:03 +01:00
Andreas Stadelmeier	4547fbab40	add shuffle example to wildcard introduction	2024-03-06 00:33:54 +01:00
Andreas Stadelmeier	cbba453a73	Cleanup and remove capture conversion chapter	2024-03-05 18:31:50 +01:00
Andreas Stadelmeier	e15d61cdae	Add Global Type Inference introduction	2024-03-05 17:12:56 +01:00
Andreas Stadelmeier	3904304a1d	Cleanup	2024-03-04 16:51:20 +01:00