moved mathql/ under software/

[helm.git] / mathql / doc / mathql_operational.tex

diff --git a/mathql/doc/mathql_operational.tex b/mathql/doc/mathql_operational.tex
new file mode 100644 (file)
index 0000000..a7b3a9a
--- /dev/null
+++ b/mathql/doc/mathql_operational.tex
@@ -0,0 +1,14 @@
+\section {Operational Semantics} \label {Operational}
+
+This section describes {\MathQL} semantics, that we present in a natural
+operational style \cite{Lan98,Win93}. 
+Here we use a simple type system that includes basic types such as strings and
+Booleans, and some type constructors such as product and exponentiation.
+$ y \oft Y $ will denote a typing judgement.
+This semantics is not meant as a formal system \emph{per se}, but should be a
+reference for implementors.
+
+\input{mathql_operational_background}
+\input{mathql_operational_core}
+\input{mathql_operational_basic}
+