mirror of
https://github.com/thufschmitt/tix-papers.git
synced 2024-09-11 13:00:34 +03:00
69 lines
1.3 KiB
TeX
69 lines
1.3 KiB
TeX
\input{common/header.tex}
|
|
|
|
\title{A type system for nix}
|
|
|
|
\begin{document}
|
|
\maketitle
|
|
|
|
\tableofcontents
|
|
|
|
\pagebreak
|
|
|
|
In order to lighten the type system, we will not work on the full nix language
|
|
(presented in Section~\ref{sec:nix-grammar}), but on a simplified version
|
|
called nix-light that we also presents in this document.
|
|
|
|
We also present a compilation from nix to nix-light.
|
|
|
|
\section{The nix language}
|
|
|
|
\subsection{Grammar}
|
|
\label{sec:nix-grammar}
|
|
\input{nix/grammar}
|
|
|
|
\subsection{Typing}
|
|
\label{sec:nix-typing}
|
|
\input{nix/typing}
|
|
|
|
\subsection{Preprocessing}
|
|
\todo{Reformulate to fit the position in the document}
|
|
\input{nix/preprocessing}
|
|
|
|
\section{Nix-light}
|
|
|
|
\subsection{Grammar}
|
|
\label{sec:nix-light-grammar}
|
|
\input{nix-light/grammar}
|
|
|
|
\subsection{Semantics}
|
|
\input{nix-light/semantics}
|
|
|
|
\section{Nix-light typing}
|
|
|
|
\subsection{The $\λ\&-calculus$}
|
|
\input{nix-light/typing/lambdaCalculus}
|
|
|
|
\subsection{Bidirectional typing}
|
|
\input{nix-light/typing/bidir.tex}
|
|
|
|
\section{Soundness of the type-system}
|
|
\input{soundness/intro}
|
|
|
|
\subsection{The oracle type-system}
|
|
\input{soundness/oracle}
|
|
|
|
\subsection{Soundness of the oracle type-system}
|
|
|
|
\section{Compilation}
|
|
|
|
\subsection{Compilation rules}
|
|
\input{compilation/main}
|
|
|
|
\subsection{Preservation of typing}
|
|
|
|
\todos{}
|
|
|
|
\bibliographystyle{alpha}
|
|
\bibliography{references}
|
|
\end{document}
|