core chapter skeleton

11 files changed, 61 insertions, 1 deletions

diff --git a/chapters/03-core.tex b/chapters/03-core.tex
index 09d9c90..9369522 100644
--- a/chapters/03-core.tex
+++ b/chapters/03-core.tex
@@ -1,4 +1,8 @@
-\chapter{Core}
+\chapter{VEIN: VErification via Interaction Nets}
 \label{ch:core}
 
 % This chapter contains the core of the thesis, where the work is presented in details.
+
+\input{chapters/core/01-implementation}
+
+\input{chapters/core/02-soundness-proof}
diff --git a/chapters/core/01-implementation.tex b/chapters/core/01-implementation.tex
new file mode 100644
index 0000000..fcb1345
--- /dev/null
+++ b/chapters/core/01-implementation.tex
@@ -0,0 +1,12 @@
+\section{Implementation}
+\label{sec:implementation}
+
+% This sections contain the implementation sections
+
+\input{chapters/core/implementation/01-inpla}
+
+\input{chapters/core/implementation/02-interaction-rules}
+
+\input{chapters/core/implementation/03-translation}
+
+\input{chapters/core/implementation/04-python-module}
diff --git a/chapters/core/02-soundness-proof.tex b/chapters/core/02-soundness-proof.tex
new file mode 100644
index 0000000..c353946
--- /dev/null
+++ b/chapters/core/02-soundness-proof.tex
@@ -0,0 +1,12 @@
+\section{Soundness Proof}
+\label{sec:soundness-proof}
+
+% This section contains the proof that my tool is sound
+
+\input{chapters/core/soundness-proof/01-mathematical-definitions}
+
+\input{chapters/core/soundness-proof/02-soundness-of-translation}
+
+\input{chapters/core/soundness-proof/03-soundness-of-interaction-rules}
+
+\input{chapters/core/soundness-proof/04-soundness-of-reduction}
diff --git a/chapters/core/implementation/01-inpla.tex b/chapters/core/implementation/01-inpla.tex
new file mode 100644
index 0000000..b534705
--- /dev/null
+++ b/chapters/core/implementation/01-inpla.tex
@@ -0,0 +1,4 @@
+\subsection{Inpla fork}
+\label{sec:inpla}
+
+% This subsection talks about my Inpla fork
diff --git a/chapters/core/implementation/02-interaction-rules.tex b/chapters/core/implementation/02-interaction-rules.tex
new file mode 100644
index 0000000..bef0970
--- /dev/null
+++ b/chapters/core/implementation/02-interaction-rules.tex
@@ -0,0 +1,4 @@
+\subsection{Interaction Rules}
+\label{sec:interaction-rules}
+
+% This subsection talks about the interaction rules that implement the symbolic simplification
diff --git a/chapters/core/implementation/03-translation.tex b/chapters/core/implementation/03-translation.tex
new file mode 100644
index 0000000..4f2064c
--- /dev/null
+++ b/chapters/core/implementation/03-translation.tex
@@ -0,0 +1,4 @@
+\subsection{ONNX Translation}
+\label{sec:translation}
+
+% This subsection talks about the function used to translate ONNX to Inpla syntax
diff --git a/chapters/core/implementation/04-python-module.tex b/chapters/core/implementation/04-python-module.tex
new file mode 100644
index 0000000..7f144db
--- /dev/null
+++ b/chapters/core/implementation/04-python-module.tex
@@ -0,0 +1,4 @@
+\subsection{Python Module}
+\label{sec:python-module}
+
+% This subsection talks how the tool is contained in a neat python module and various optimizations
diff --git a/chapters/core/soundness-proof/01-mathematical-definitions.tex b/chapters/core/soundness-proof/01-mathematical-definitions.tex
new file mode 100644
index 0000000..3d8c031
--- /dev/null
+++ b/chapters/core/soundness-proof/01-mathematical-definitions.tex
@@ -0,0 +1,4 @@
+\subsection{Mathematical Definitions}
+\label{sec:mathematical-definitions}
+
+% This subsection contains the mathematical definitions used in the proof
diff --git a/chapters/core/soundness-proof/02-soundness-of-translation.tex b/chapters/core/soundness-proof/02-soundness-of-translation.tex
new file mode 100644
index 0000000..f112aa5
--- /dev/null
+++ b/chapters/core/soundness-proof/02-soundness-of-translation.tex
@@ -0,0 +1,4 @@
+\subsection{Soundness of Translation}
+\label{sec:soundness-of-translation}
+
+% This subsection gives the proof for ONNX-to-Inpla translation soundness
diff --git a/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
new file mode 100644
index 0000000..9aa84ac
--- /dev/null
+++ b/chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex
@@ -0,0 +1,4 @@
+\subsection{Soundness of Interaction Rules}
+\label{sec:soundness-of-interaction-rules}
+
+% This subsections gives the proof for each interaction rule
diff --git a/chapters/core/soundness-proof/04-soundness-of-reduction.tex b/chapters/core/soundness-proof/04-soundness-of-reduction.tex
new file mode 100644
index 0000000..b2d6116
--- /dev/null
+++ b/chapters/core/soundness-proof/04-soundness-of-reduction.tex
@@ -0,0 +1,4 @@
+\subsection{Soundness of Reduction}
+\label{sec:soundness-of-reduction}
+
+% This subsection gives the proof that each reduction step doesn't alter the semantic