3.3 KiB
\input{out/generated/synthesis.tex}
Outline {-}
\input{out/generated/outline.tex}
Background
\label{sec:background}
Nix
General presentation
\input{out/generated/context/nix/general-presentation.tex}
Syntax and semantics
\input{out/generated/context/nix/syntax-and-semantics}
Set-theoretic types
\input{out/generated/context/set-theoretic-types}
Nix-light
\label{sec:nix-light}
Motivation
\input{out/generated/nix-light/motivation.tex}
Description
\input{out/generated/nix-light/description.tex}
From Nix to Nix-light
\input{out/generated/nix-light/compilation.tex}
Typing
\label{sec:typing}
Types and subtyping
\input{out/generated/typing/types.tex}
Functional core
\input{out/generated/typing/lambda-calculus.tex}
Data structures
\label{typing::structures}
We now extends our core calculus with the two builtins data structures of Nix (lists and records).
Lists
\label{typing::structures::listes} \input{out/generated/typing/lists.tex}
Records
\label{typing::structures::records} \input{out/generated/typing/records.tex}
About soundness
\input{out/generated/typing/about-soundness.tex}
Implementation
\label{sec:implementation} \input{out/generated/implem/intro.tex}
\cduce{} and subtyping
\input{out/generated/implem/cduce.tex}
Adaptation of the type-system
\input{out/generated/implem/modifications.tex}
Extensions
\input{out/generated/implem/extensions.tex} \label{implem::extensions}
Conclusion {-}
\input{out/generated/conclusion.tex}
\printbibliography{} \appendix
Appendix {-}
\input{out/generated/appendix/nix-grammar} \input{out/generated/appendix/nix-light-grammar} \input{appendix/nix-light-semantics.tex} \input{appendix/compilation} \input{out/generated/appendix/typecase-typing-rules.tex} \input{appendix/record-typing.tex} \input{out/generated/appendix/implem.tex} \input{out/generated/appendix/examples.tex}