helm/mathql/doc/mathql_operational.tex

   1 \section {Operational Semantics} \label {Operational}
   2
   3 This section describes {\MathQL} semantics, that we present in a natural
   4 operational style \cite{Lan98,Win93}.
   5 Here we use a simple type system that includes basic types such as strings and
   6 Booleans, and some type constructors such as product and exponentiation.
   7 $ y \oft Y $ will denote a typing judgement.
   8 This semantics is not meant as a formal system \emph{per se}, but should be a
   9 reference for implementors.
  10
  11 \input{mathql_operational_background}
  12 \input{mathql_operational_core}
  13 \input{mathql_operational_basic}
  14