path: root/main.tex

\newif\ifacmart
\acmarttrue

\ifacmart
  \documentclass[acmsmall, anonymous, review, natbib=false, pbalance]{acmart}
\else
  \documentclass[a4paper]{article}
\fi

%% Package Imports %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Provided by acmart
\ifacmart\else
  \usepackage{amsthm} %% proof environments
\fi

%% Incompatible with acmart
\ifacmart\else
  \usepackage[
    warnings-off={mathtools-colon,mathtools-overbracket}
  ]{unicode-math} %% math symbols
  \usepackage[subtle, margins=tight]{savetrees}
\fi

\usepackage[
  datamodel=acmdatamodel,
  style=acmnumeric,
  giveninits,
  doi,
  eprint = false
]{biblatex}   %% bibliography configuration
\usepackage{booktabs} %% table formatting
\usepackage{ebproof}  %% proof trees
\usepackage{expl3}  %% Latex 3
\usepackage{enumitem} %% format contributions list
\usepackage{float}  %% forcing appendix figures
\usepackage{hyperref} %% hyperlinks within document
\usepackage{mathtools}  %% matrix alignment
\usepackage[outputdir=build]{minted}  %% code formatting
\usepackage{stackrel} %% Annotating judgements
\usepackage{subcaption} %% subfigures with captions
\usepackage{subfiles} %% splitting file into sections
\usepackage{thmtools} %% proof environments
\usepackage{tikz} %% diagram
\usepackage[dvipsnames]{xcolor} %% color TODO and FIXME
\usepackage{xr} %% cross reference between sections

%% After hyperref
\usepackage{cleveref} %% easier citations

%% Document Metadata %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\author{Greg Brown}
\ifacmart
  \orcid{0009-0000-3401-8637}
  \affiliation{%
    \institution{University of Edinburgh}
    \city{Edinburgh}
    \country{UK}
  }
  \email{greg.brown01@ed.ac.uk}{}
\fi

\ifacmart
  \acmJournal{PACMPL}
  %% \acmConference[ICFP '25]{}{January 21, 2025}{Denver, CO, USA}
\fi

\ifacmart
  \setcopyright{none}
\fi

\title{ARTiST:\ Adding Regular Types in System~T}

\ifacmart
  \keywords{}
\fi

%% Package Configuration %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% biblatex
\addbibresource{\subfix{main.bib}}

%% hyperref
\ifacmart\else
  \makeatletter
  \hypersetup{
    pdftitle={\@title},
    pdfauthor={\@author},
  }
  \makeatother
\fi

%% Minted centered
\RecustomVerbatimEnvironment{Verbatim}{BVerbatim}{}

%% xr
\externaldocument[M-]{\subfix{main}}

%% Possessive textcite
\DeclareNameWrapperFormat{labelname:poss}{#1's}
\DeclareFieldFormat{shorthand:poss}{%
  \ifnameundef{labelname}{#1's}{#1}}
\DeclareFieldFormat{citetitle:poss}{\mkbibemph{#1}'s}
\DeclareFieldFormat{label:poss}{#1's}

\newrobustcmd*{\posscitealias}{%
  \AtNextCite{%
    \DeclareNameWrapperAlias{labelname}{labelname:poss}%
    \DeclareFieldAlias{shorthand}{shorthand:poss}%
    \DeclareFieldAlias{citetitle}{citetitle:poss}%
    \DeclareFieldAlias{label}{label:poss}}}

\newrobustcmd*{\posscite}{%
  \posscitealias%
  \textcite}

\newrobustcmd*{\Posscite}{\bibsentence\posscite}

\newrobustcmd*{\posscites}{%
  \posscitealias%
  \textcites}

%% Theorem Environments %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\ifacmart\else
  \declaretheorem[
    style=plain,
    numberwithin=section
  ]{definition}
  \declaretheorem[
    numberwithin=section,
    sibling=definition
  ]{lemma,corollary,proposition,theorem, conjecture}
  \declaretheorem[
    style=remark,
    numberwithin=section,
    sibling=definition
  ]{remark,example}
\fi

\renewcommand*{\textcitedelim}{\addcomma\addspace\iflastcitekey{\bibstring{and}\addspace}{}}

%% Custom Macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Needed for compatibility
\ifacmart\else
  \newcommand{\bibliofont}{\footnotesize}
\fi

% Psuedocode
\newminted[systemt]{'lexer.py:SystemTLexer -x'}{}
\newmintinline[systemtinline]{'lexer.py:SystemTLexer -x'}{}

% TODOS and such
\newcommand\lang{{\color{Green} ARTiST}}
\newcommand\TODO[1]{{\color{Blue}TODO:\ {#1}}}
\newcommand\FIXME[1]{{\color{Red}FIXME:\ {#1}}}

% Quantification: e.g. \rangeover{x_i}{i < n}
\newcommand\rangeover[2]{\overrightarrow{#1}}

% Judgements for typing and such
\newcommand\judgement[4][]{{#2} \vdash^{#1} {#3} : {#4}}
\newcommand\jdgmnt[3]{{#2} \vdash {#3}~\mathrm{#1}}

%%% Term syntax

%% Godel encoding
\newcommand\encode[1]{\llcorner {#1} \lrcorner}

%% Tuples
\DeclarePairedDelimiter\tuple{\langle}{\rangle}
\newcommand\lettm[3]{\mathsf{let}~{#1} \coloneq {#2}~\mathsf{in}~{#3}}

%% Naturals
\newcommand\nat{\mathsf{N}}
\newcommand\zero{\ensuremath{\mathsf{zero}}}
\newcommand\suc{\ensuremath{\mathsf{suc}}}

\newcommand\primreckw{\ensuremath{\mathsf{primrec}}}
\NewDocumentCommand\primrec{m m g}{%
    \primreckw~{#1}~{#2}\IfValueT{#3}{~{#3}}%
  }

\newcommand\pairingkw{\ensuremath{\mathsf{pair}}}
\NewDocumentCommand\pairing{m m}{%
    \pairingkw~{#1}~{#2}%
  }

%% Functors
\newcommand\mapkw{\ensuremath{\mathsf{map}}}
% e.g. \maptm{X}{1 + X}
\newcommand\maptm[2]{\mapkw_{\Lambda {#1}.{#2}}}

%% Recursive types
\newcommand\foldkw{\ensuremath{\mathsf{fold}}}
\newcommand\foldtm[3]{\foldkw~{#1}~\mathsf{with}~{{#2}.~{#3}}}

%% Sums
\newcommand\matchtm[2]{\mathsf{match}~{#1}~\mathsf{with}~{#2}}
\newcommand\casetm[5]{\matchtm{#1}{\rangeover{\tuple{{#4}, {#2}}.~{#3}}{{#4}<{#5}}}}

%%% Substitution
\ExplSyntaxOn
\NewDocumentCommand \squid_subpart:nn {m m} {{#1} \mapsto {#2}}
\NewDocumentCommand \squid_contsub:n {> {\SplitArgument{1}{/}} m}
  { \squid_subpart:nn #1 \squid_checksub
  }
\NewDocumentCommand \squid_checksub {O{\parallel}}
  {
   \peek_meaning_ignore_spaces:NTF \bgroup
      {#1 \squid_contsub:n}
      {]}
  }
\NewDocumentCommand \squid_startsub:n {m}
  { {#1} [ \squid_checksub []
  }
\NewDocumentCommand \sub {m > {\SplitList{,}} m}
  { \squid_startsub:n {#1} #2
  }
\ExplSyntaxOff

%% Document %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\ifacmart\else
  \maketitle{}
\fi

\begin{abstract}
G\"odel's System T is a simple calculus that performs computation. The absence
of any type abstractions, such as products or sums, along with the limited form
of recursion makes using System T as a target language difficult. In this paper
we introduce \lang{}, a new intermediate language. One can compile \lang{} into
System~T using well-known type encodings, and we have written this algorithm
within \lang{} itself. We also describe a compiler for \lang{} written in Idris
2, featuring an intrinsically well-scoped AST and runtime-erased type-checking
proofs.
\end{abstract}

\ifacmart
  \maketitle{}
\fi

%% Body

\subfile{sec/intro.ltx}
\subfile{sec/systemt.ltx}
\subfile{sec/lang.ltx}
\subfile{sec/embedding.ltx}
\subfile{sec/reducer.ltx}
\subfile{sec/compiler.ltx}
\subfile{sec/related.ltx}

\printbibliography{}

\appendix

\end{document}