Compare commits
2 Commits
eb2ae1eb34
...
59e80f556c
| Author | SHA1 | Date | |
|---|---|---|---|
|
59e80f556c | ||
|
|
4f3350cdcb |
72
aspUnify.tex
72
aspUnify.tex
@ -2,8 +2,9 @@
|
||||
% LLNCS macro package for Springer Computer Science proceedings;
|
||||
% Version 2.21 of 2022/01/12
|
||||
%
|
||||
\documentclass[runningheads]{llncs}
|
||||
%
|
||||
\documentclass[submission]{eptcs}
|
||||
\providecommand{\event}{Symposium in honor of Peter Thiemann's 60th birthday} % Name of the event you are submitting to
|
||||
\usepackage{underscore}
|
||||
\usepackage[T1]{fontenc}
|
||||
% T1 fonts will be used to generate the final print and online PDFs,
|
||||
% so please use T1 fonts in your manuscript whenever possible.
|
||||
@ -23,39 +24,48 @@
|
||||
\usepackage{mathpartir}
|
||||
\usepackage{amsmath}
|
||||
\usepackage{amssymb}
|
||||
\usepackage{amsthm}
|
||||
\usepackage{enumitem}
|
||||
%\usepackage{amsthm}
|
||||
|
||||
|
||||
\newtheorem{theorem}{Theorem}
|
||||
\newtheorem{lemma}[theorem]{Lemma}
|
||||
|
||||
\title{Global Type Inference for Java using SAT Solvers}
|
||||
\author{Andreas Stadelmeier
|
||||
\institute{DHBW\\ Stuttgart}
|
||||
\email{a.stadelmeier@hb.dhbw-stuttgart.de}
|
||||
}
|
||||
\newcommand{\authorrunning}{Andreas Stadelmeier}
|
||||
\newcommand{\titlerunning}{Type Unification to SAT}
|
||||
\hypersetup{
|
||||
bookmarksnumbered,
|
||||
pdftitle = {\titlerunning},
|
||||
pdfauthor = {\authorrunning},
|
||||
pdfsubject = {Global Type Inference for Java}, % Consider adding a more appropriate subject or description
|
||||
pdfkeywords = {typeinference, java, sat solving, answer set programming} % Uncomment and enter keywords specific to your paper
|
||||
}
|
||||
|
||||
\begin{document}
|
||||
%
|
||||
\title{Global Type Inference for Java using SAT Solvers}
|
||||
%
|
||||
%\titlerunning{Abbreviated paper title}
|
||||
% If the paper title is too long for the running head, you can set
|
||||
% an abbreviated paper title here
|
||||
%
|
||||
\author{First Author\inst{1}\orcidID{0000-1111-2222-3333} \and
|
||||
Second Author\inst{2,3}\orcidID{1111-2222-3333-4444} \and
|
||||
Third Author\inst{3}\orcidID{2222--3333-4444-5555}}
|
||||
%
|
||||
\authorrunning{F. Author et al.}
|
||||
% First names are abbreviated in the running head.
|
||||
% If there are more than two authors, 'et al.' is used.
|
||||
%
|
||||
\institute{Princeton University, Princeton NJ 08544, USA \and
|
||||
Springer Heidelberg, Tiergartenstr. 17, 69121 Heidelberg, Germany
|
||||
\email{lncs@springer.com}\\
|
||||
\url{http://www.springer.com/gp/computer-science/lncs} \and
|
||||
ABC Institute, Rupert-Karls-University Heidelberg, Heidelberg, Germany\\
|
||||
\email{\{abc,lncs\}@uni-heidelberg.de}}
|
||||
%
|
||||
\maketitle % typeset the header of the contribution
|
||||
%
|
||||
\begin{abstract}
|
||||
The abstract should briefly summarize the contents of the paper in
|
||||
150--250 words.
|
||||
Global type inference for Java is able to compute correct types for an input program
|
||||
which has no type annotations at all.
|
||||
Global type inference for Featherweigt Generic Java is NP-hard.
|
||||
Former implementations of the algorithm struggled with bad runtime performance.
|
||||
In this paper we translated the type inference algorithm for Featherweight Generic Java to an
|
||||
Answer Set Program.
|
||||
Answer Set Programming (ASP) promises to solve complex computational search problems
|
||||
as long as they are finite domain.
|
||||
|
||||
\keywords{First keyword \and Second keyword \and Another keyword.}
|
||||
%TODO: Is this correct?
|
||||
\end{abstract}
|
||||
%
|
||||
%
|
||||
@ -117,6 +127,7 @@ The need to have an upper bound to every type placeholder.
|
||||
|
||||
We have to formulate the unification algorithm with implication rules.
|
||||
Those can be directly translated to ASP.
|
||||
\label{sec:implicationRules}
|
||||
\begin{mathpar}
|
||||
\inferrule[Subst]{
|
||||
\tv{a} \doteq \type{N}
|
||||
@ -297,7 +308,7 @@ Fail:
|
||||
}
|
||||
\and
|
||||
\inferrule[Fail-Sigma]{
|
||||
\tv{a} \doteq \type{N} \\
|
||||
\tv{a} \mapsto \type{N} \\
|
||||
\tv{a} \in \type{N}
|
||||
}{
|
||||
\emptyset
|
||||
@ -326,10 +337,22 @@ Fail:
|
||||
The algorithm terminates if every type placeholder in the input constraint set has an assigned type.
|
||||
|
||||
\section{ASP Encoding}
|
||||
The implication rules defined in chapter \ref{sec:implicationRules} can be translated to an ASP program.
|
||||
|
||||
\begin{tabular}{l | r}
|
||||
$\exptype{C}{\ol{X}}$ & \texttt{type("C", paramX)}\\
|
||||
\end{tabular}
|
||||
|
||||
\section{Termination}
|
||||
The amount of different constraints is limited by the maximum amount of encapsulated generics.
|
||||
The only part that is able to add an additional nesting is the Subst-Param rule.
|
||||
Here a type placeholder inside a type parameter list is replaced by another type which possibly adds
|
||||
another layer of nesting but it also removes one type placeholder.
|
||||
|
||||
There must be one substitution that does not add another type placeholder.
|
||||
Otherwise there has to be a loop and this woul lead to an incorrect constraint set due to the Fail-Sigma rule.
|
||||
|
||||
|
||||
\section{Completeness}
|
||||
To proof completeness we have to show that every type can be replaced by a placeholder in a correct constraint set.
|
||||
|
||||
@ -451,4 +474,7 @@ and every type placeholder has an upper bound $\tv{a} \lessdot \type{N}$.
|
||||
And more text.
|
||||
\end{proof}
|
||||
|
||||
\bibliographystyle{eptcs}
|
||||
\bibliography{martin}
|
||||
|
||||
\end{document}
|
||||
|
||||
263
eptcs.cls
Normal file
263
eptcs.cls
Normal file
@ -0,0 +1,263 @@
|
||||
\NeedsTeXFormat{LaTeX2e}[1995/12/01]
|
||||
\ProvidesClass{eptcs}[2022/05/20 v1.7]
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%%% options %%%%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newif\ifadraft
|
||||
\newif\ifsubmission
|
||||
\newif\ifpreliminary
|
||||
\newif\ifcopyright
|
||||
\newif\ifpublicdomain
|
||||
\newif\ifcreativecommons
|
||||
\newif\ifnoderivs
|
||||
\newif\ifsharealike
|
||||
\newif\ifnoncommercial
|
||||
\adraftfalse
|
||||
\submissionfalse
|
||||
\preliminaryfalse
|
||||
\copyrightfalse
|
||||
\publicdomainfalse
|
||||
\creativecommonsfalse
|
||||
\noderivsfalse
|
||||
\sharealikefalse
|
||||
\noncommercialfalse
|
||||
\DeclareOption{adraft}{\adrafttrue}
|
||||
\DeclareOption{submission}{\submissiontrue}
|
||||
\DeclareOption{preliminary}{\preliminarytrue}
|
||||
\DeclareOption{copyright}{\copyrighttrue}
|
||||
\DeclareOption{publicdomain}{\publicdomaintrue}
|
||||
\DeclareOption{creativecommons}{\creativecommonstrue}
|
||||
\DeclareOption{noderivs}{\noderivstrue}
|
||||
\DeclareOption{noncommercial}{\noncommercialtrue}
|
||||
\DeclareOption{sharealike}{\sharealiketrue}
|
||||
\ProcessOptions\relax
|
||||
|
||||
\LoadClass[letterpaper,11pt,twoside]{article}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%% On US letter paper the margins (left-top-right-bottom) are %%
|
||||
%% 2.795cm - 1.23cm - 2.795cm - 3.46cm %%
|
||||
%% Note: When \topmargin would be 0, the real top margin would be %%
|
||||
%% (72-25-12=35pt) + 1pt (unused portion of head) = .5in = 1.27cm. %%
|
||||
%% The bottom margin is 11in - 1in + 0.04cm - 623/72in = 3.46cm. %%
|
||||
%% On the first page the bottom margin contains various footers. %%
|
||||
%% When translating from US letter to A4 paper, without scaling, by %%
|
||||
%% leaving the centre of the paper invariant (as is possible when %%
|
||||
%% printing the paper with acroread), the resulting A4 margins are %%
|
||||
%% 2.5cm - 2.11cm - 2.5cm - 4.34cm %%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
\textwidth 16cm % A4 width is 21cm %
|
||||
\textheight 623.01pt % 46 lines exactly = 21.98cm %
|
||||
\oddsidemargin -0.04cm % +1 inch = 2.5cm %
|
||||
\evensidemargin -0.04cm % +1 inch = 2.5cm %
|
||||
\topmargin -0.04cm % +1 inch = 2.5cm %
|
||||
\advance\topmargin-\headheight % 12pt %
|
||||
\advance\topmargin-\headsep % 25pt %
|
||||
\marginparwidth 45pt % leaves 15pt from A4 edge %
|
||||
\advance\evensidemargin .295cm % centre w.r.t. letter paper %
|
||||
\advance\oddsidemargin .295cm % centre w.r.t. letter paper %
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%%% load eptcsdata when available %%%%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\IfFileExists{eptcsdata.tex}{\input{eptcsdata}}{}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%%% Pagestyle and titlepage %%%%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\pagestyle{myheadings}
|
||||
\renewcommand\pagestyle[1]{} % ignore further \pagestyles
|
||||
|
||||
\renewcommand\maketitle{\par
|
||||
\begingroup
|
||||
\providecommand{\event}{}
|
||||
\ifadraft
|
||||
\providecommand{\publicationstatus}{\Large DRAFT\quad\today}
|
||||
\else\ifsubmission
|
||||
\providecommand{\publicationstatus}{Submitted to:\\
|
||||
\event}
|
||||
\else\ifpreliminary
|
||||
\providecommand{\publicationstatus}{Preliminary Report. Final version to appear in:\\
|
||||
\event}
|
||||
\else
|
||||
\providecommand{\publicationstatus}{To appear in EPTCS.}
|
||||
\fi\fi\fi
|
||||
\providecommand{\titlerunning}{Please define {\ttfamily $\backslash$titlerunning}}
|
||||
\providecommand{\authorrunning}{Please define {\ttfamily $\backslash$authorrunning}}
|
||||
\providecommand{\copyrightholders}{\authorrunning}
|
||||
\renewcommand\thefootnote{\@fnsymbol\c@footnote}%
|
||||
\def\@makefnmark{\rlap{\@textsuperscript{\normalfont\@thefnmark}}}%
|
||||
\long\def\@makefntext##1{\parindent 1em\noindent
|
||||
\hb@xt@1.8em{%
|
||||
\hss\@textsuperscript{\normalfont\@thefnmark}}##1}%
|
||||
\newpage
|
||||
\global\@topnum\z@ % Prevents figures from going at top of page.
|
||||
\@maketitle
|
||||
\thispagestyle{empty}\@thanks
|
||||
\endgroup
|
||||
\setcounter{footnote}{0}%
|
||||
\label{FirstPage}
|
||||
\global\let\thanks\relax
|
||||
\global\let\maketitle\relax
|
||||
\global\let\@maketitle\relax
|
||||
\global\let\@thanks\@empty
|
||||
\global\let\@author\@empty
|
||||
\global\let\@date\@empty
|
||||
\global\let\@title\@empty
|
||||
\global\let\title\relax
|
||||
\global\let\author\relax
|
||||
\global\let\date\relax
|
||||
\global\let\and\relax
|
||||
}
|
||||
\def\@maketitle{% adapted from article.cls
|
||||
\newpage
|
||||
\noindent
|
||||
\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
|
||||
\begin{tabular}{@{}l}
|
||||
\publicationstatus
|
||||
\end{tabular}}
|
||||
\hfill\vspace{-1em}
|
||||
\raisebox{-22.8cm}[0pt][0pt]{\footnotesize
|
||||
\makebox[0pt][r]{
|
||||
\begin{tabular}{l@{}}
|
||||
\ifpublicdomain
|
||||
This work is \href{https://creativecommons.org/publicdomain/zero/1.0/}
|
||||
{dedicated to the public domain}.
|
||||
\else
|
||||
\ifcopyright
|
||||
\copyright~\copyrightholders\\
|
||||
\fi
|
||||
\ifcreativecommons
|
||||
This work is licensed under the
|
||||
\ifnoncommercial
|
||||
\href{https://creativecommons.org}{Creative Commons}\\
|
||||
\ifnoderivs
|
||||
\href{https://creativecommons.org/licenses/by-nc-nd/4.0/}
|
||||
{Attribution-Noncommercial-No Derivative Works} License.
|
||||
\else\ifsharealike
|
||||
\href{https://creativecommons.org/licenses/by-nc-sa/4.0/}
|
||||
{Attribution-Noncommercial-Share Alike} License.
|
||||
\else
|
||||
\href{https://creativecommons.org/licenses/by-nc/4.0/}
|
||||
{Attribution-Noncommercial} License.
|
||||
\fi\fi
|
||||
\else
|
||||
\ifnoderivs
|
||||
\href{https://creativecommons.org}{Creative Commons}\\
|
||||
\href{https://creativecommons.org/licenses/by-nd/4.0/}
|
||||
{Attribution-No Derivative Works} License.
|
||||
\else\ifsharealike
|
||||
\href{https://creativecommons.org}{Creative Commons}\\
|
||||
\href{https://creativecommons.org/licenses/by-sa/4.0/}
|
||||
{Attribution-Share Alike} License.
|
||||
\else
|
||||
\\\href{https://creativecommons.org}{Creative Commons}
|
||||
\href{https://creativecommons.org/licenses/by/4.0/}
|
||||
{Attribution} License.
|
||||
\fi\fi
|
||||
\fi
|
||||
\fi
|
||||
\fi
|
||||
\end{tabular}}}
|
||||
\null
|
||||
%\vskip 2em% a bit of space removed (< 2em)
|
||||
\begin{center}%
|
||||
\let \footnote \thanks
|
||||
{\LARGE\bfseries \@title \par}% \bf added
|
||||
\vskip 2em% was: 1.5em
|
||||
{\large
|
||||
\lineskip .5em%
|
||||
\begin{tabular}[t]{c}%
|
||||
\@author
|
||||
\end{tabular}\par}%
|
||||
\vskip 1em% \date and extra space removed
|
||||
\end{center}%
|
||||
\par
|
||||
\markboth{\hfill\titlerunning}{\authorrunning\hfill}
|
||||
\vskip .5em}
|
||||
|
||||
\AtBeginDocument{
|
||||
\providecommand{\firstpage}{1}
|
||||
\setcounter{firstpage}{\firstpage}
|
||||
\setcounter{page}{\firstpage}
|
||||
\@ifpackageloaded{array}% Contributed by Wolfgang Jeltsch
|
||||
{\newcommand{\IfArrayPackageLoaded}[2]{#1}}
|
||||
{\newcommand{\IfArrayPackageLoaded}[2]{#2}}}
|
||||
\newcommand{\institute}[1]{\IfArrayPackageLoaded
|
||||
{\\{\scriptsize\begin{tabular}[t]{@{}>{\footnotesize}c@{}}#1\end{tabular}}}
|
||||
{\\{\scriptsize\begin{tabular}[t]{@{\footnotesize}c@{}}#1\end{tabular}}}}
|
||||
\newcommand{\email}[1]{\\{\footnotesize\ttfamily #1}}
|
||||
|
||||
\renewenvironment{abstract}{\begin{list}{}% header removed and noindent
|
||||
{\rightmargin\leftmargin
|
||||
\listparindent 1.5em
|
||||
\parsep 0pt plus 1pt}
|
||||
\small\item}{\end{list}
|
||||
}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\RequirePackage{hyperref} % add hyperlinks
|
||||
\RequirePackage{mathptmx} % Pick Times Roman as a base font
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%%% Remember page numbers %%%%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\newcounter{firstpage}
|
||||
\setcounter{firstpage}{1}
|
||||
\AtEndDocument{\clearpage
|
||||
\addtocounter{page}{-1}
|
||||
\immediate\write\@auxout{\string
|
||||
\newlabel{LastPage}{{}{\thepage}{}{page.\thepage}{}}}%
|
||||
\newwrite\pages
|
||||
\immediate\openout\pages=\jobname.pag
|
||||
\immediate\write\pages{\arabic{firstpage}-\arabic{page}}
|
||||
\addtocounter{page}{1}}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%%% Less space in lists %%%%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\def\@listi{\leftmargin\leftmargini
|
||||
\parsep 2.5\p@ \@plus1.5\p@ \@minus\p@
|
||||
\topsep 5\p@ \@plus2\p@ \@minus5\p@
|
||||
\itemsep2.5\p@ \@plus1.5\p@ \@minus\p@}
|
||||
\let\@listI\@listi
|
||||
\@listi
|
||||
\def\@listii {\leftmargin\leftmarginii
|
||||
\labelwidth\leftmarginii
|
||||
\advance\labelwidth-\labelsep
|
||||
\topsep 1\p@ \@plus\p@ \@minus\p@
|
||||
\parsep 1\p@ \@plus\p@ \@minus\p@
|
||||
\itemsep \parsep}
|
||||
\def\@listiii{\leftmargin\leftmarginiii
|
||||
\labelwidth\leftmarginiii
|
||||
\advance\labelwidth-\labelsep
|
||||
\topsep \z@
|
||||
\parsep \z@
|
||||
\itemsep \topsep}
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
%%%% References small and with less space between items %%%%
|
||||
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
||||
\renewenvironment{thebibliography}[1]
|
||||
{\section*{\refname}\small% small added
|
||||
\list{\@biblabel{\@arabic\c@enumiv}}%
|
||||
{\settowidth\labelwidth{\@biblabel{#1}}%
|
||||
\leftmargin\labelwidth
|
||||
\advance\leftmargin\labelsep
|
||||
\@openbib@code
|
||||
\usecounter{enumiv}%
|
||||
\let\p@enumiv\@empty
|
||||
\renewcommand\theenumiv{\@arabic\c@enumiv}}%
|
||||
\sloppy
|
||||
\clubpenalty4000
|
||||
\@clubpenalty \clubpenalty
|
||||
\widowpenalty4000%
|
||||
\sfcode`\.\@m
|
||||
\setlength{\parskip}{0pt}%
|
||||
\setlength{\itemsep}{3pt plus 2pt}% less space between items
|
||||
}
|
||||
{\def\@noitemerr
|
||||
{\@latex@warning{Empty `thebibliography' environment}}%
|
||||
\endlist}
|
||||
@ -22,8 +22,6 @@
|
||||
backgroundcolor=\color{red!20}
|
||||
}
|
||||
|
||||
\newtheorem{recap}[note]{Recap}
|
||||
|
||||
\newcommand{\rulenameAfter}[1]{\begin{array}[b]{l}\rulename{#1}\\[-1em] \ \end{array}}
|
||||
|
||||
\newcommand{\tifj}{\texttt{TamedFJ}}
|
||||
|
||||
Loading…
Reference in New Issue
Block a user