]> matita.cs.unibo.it Git - helm.git/blob - mathql/doc/mathql_operational.tex
1. is_meta_closed should be applied only to terms on which a substitution
[helm.git] / 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