summaryrefslogtreecommitdiff
path: root/chapters/core
diff options
context:
space:
mode:
authorericmarin <maarin.eric@gmail.com>2026-05-05 10:52:37 +0200
committerericmarin <maarin.eric@gmail.com>2026-05-05 10:57:47 +0200
commit00439f8eacc04bee31dad6cb476d6f23f0b868dd (patch)
tree06196ccbbf582f21e595106144a213a2b275c861 /chapters/core
parent44972e22a7db20b0614cd76aef38cf8d822af1a1 (diff)
downloadvein-00439f8eacc04bee31dad6cb476d6f23f0b868dd.tar.gz
vein-00439f8eacc04bee31dad6cb476d6f23f0b868dd.zip
core chapter skeleton
Diffstat (limited to '')
-rw-r--r--chapters/core/01-implementation.tex12
-rw-r--r--chapters/core/02-soundness-proof.tex12
-rw-r--r--chapters/core/implementation/01-inpla.tex4
-rw-r--r--chapters/core/implementation/02-interaction-rules.tex4
-rw-r--r--chapters/core/implementation/03-translation.tex4
-rw-r--r--chapters/core/implementation/04-python-module.tex4
-rw-r--r--chapters/core/soundness-proof/01-mathematical-definitions.tex4
-rw-r--r--chapters/core/soundness-proof/02-soundness-of-translation.tex4
-rw-r--r--chapters/core/soundness-proof/03-soundness-of-interaction-rules.tex4
-rw-r--r--chapters/core/soundness-proof/04-soundness-of-reduction.tex4
10 files changed, 56 insertions, 0 deletions
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