diff options
Diffstat (limited to 'main.tex')
| -rw-r--r-- | main.tex | 261 |
1 files changed, 261 insertions, 0 deletions
diff --git a/main.tex b/main.tex new file mode 100644 index 0000000..e96270e --- /dev/null +++ b/main.tex @@ -0,0 +1,261 @@ +\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} |