\(
% cbs-katex.sty
%
\newcommand{\STYLE}[2]{\htmlClass{cbs-#1}{#2}}
\newcommand{\DECL}[3]{\htmlId{#1:#2}{#3}}
\newcommand{\REF}[3]{\href{###1:#2}{#3}}
\newcommand{\HYPER}[5]{\href{#1/#2/index.html###3:#4}{#5}}
% \SHADE{MATH} can be defined to produce a shaded background to highlight
% inline MATH in running text:
\newcommand{\SHADE}[1]{#1}
% \KEY{TEXT}, \STRING{TEXT}, \ATOM{TEXT}, \LEX{TEXT} can be used in math mode:
\newcommand{\KEY}[1]{\textsf{\textit{\STYLE{Key}{#1}}}}
\newcommand{\STRING}[1]{\textsf{``\texttt{#1}''}}
\newcommand{\ATOM}[1]{\textsf{`\texttt{#1}'}}
\newcommand{\LEX}[1]{\textsf{\STYLE{Key}{`}\texttt{#1}\STYLE{Key}{'}}}
% The following commands produce ASCII characters that are treated specially by LaTeX:
\newcommand{\HASH}{\char`\#}
\newcommand{\DOLLAR}{\char`\$}
\newcommand{\PERCENT}{\char`\%}
\newcommand{\AMPERSAND}{\char`\&}
\newcommand{\APOSTROPHE}{\char`\'}
\newcommand{\BACKSLASH}{\char`\\}
\newcommand{\CARET}{\char`\^}
\newcommand{\UNDERSCORE}{\char`\_}
\newcommand{\GRAVE}{\char`\`}
\newcommand{\LEFTBRACE}{\char`\{}
\newcommand{\RIGHTBRACE}{\char`\}}
\newcommand{\TILDE}{\textasciitilde} % {\char`\~}
% \NAME{name} highlights the name;
% \NAMEDECL{name} declares Name.name as the target of links to name;
% \NAMEREF{name} links name to the target Name.name in the current file;
% \NAMEHYPER{url}{file}{name} links name to Name.name at url/file/file.pdf.
% Similarly for \VAR{partvariable}, \SYN{syntaxname}, \SEM{semanticsName},
% and \SECT{sectionnumber}
% The kerns in \SUB and \VAR avoid overlaps with primes:
\newcommand{\SUB}[1]{_{\kern-2mu\STYLE{PartVariable}{\textsf{#1}}}}
% PLAIN
\newcommand{\VAR}[1]{\STYLE{PartVariable}{\textsf{\textit{#1}\kern2mu}}}
\newcommand{\NAME}[1]{\STYLE{Name}{\textsf{#1}}}
\newcommand{\SYN}[1]{\STYLE{SyntaxName}{\textsf{#1}}}
\newcommand{\SEM}[1]{\STYLE{SemanticsName}{\textsf{#1}}}
\newcommand{\SECT}[1]{\STYLE{SectionNumber}{\textsf{#1}}}
% DECL
\newcommand{\VARDECL}[1]{\DECL{PartVariable}{#1}{\VAR{#1}}}
\newcommand{\NAMEDECL}[1]{\DECL{Name}{#1}{\NAME{#1}}}
\newcommand{\SYNDECL}[1]{\DECL{SyntaxName}{#1}{\SYN{#1}}}
\newcommand{\SEMDECL}[1]{\DECL{SemanticsName}{#1}{\SEM{#1}}}
\newcommand{\SECTDECL}[1]{\DECL{SectionNumber}{#1}{\textsf{#1}}}
% REF
\newcommand{\VARREF}[1]{\REF{PartVariable}{#1}{\VAR{#1}}}
\newcommand{\NAMEREF}[1]{\REF{Name}{#1}{\NAME{#1}}}
\newcommand{\SYNREF}[1]{\REF{SyntaxName}{#1}{\SYN{#1}}}
\newcommand{\SEMREF}[1]{\REF{SemanticsName}{#1}{\SEM{#1}}}
\newcommand{\SECTREF}[1]{\REF{SectionNumber}{#1}{\SECT{#1}}}
% HYPER
\newcommand{\VARHYPER}[3]{\HYPER{#1}{#2}{PartVariable}{#3}{\VAR{#3}}}
\newcommand{\NAMEHYPER}[3]{\HYPER{#1}{#2}{Name}{#3}{\NAME{#3}}}
\newcommand{\SYNHYPER}[3]{\HYPER{#1}{#2}{SyntaxName}{#3}{\SYN{#3}}}
\newcommand{\SEMHYPER}[3]{\HYPER{#1}{#2}{SemanticsName}{#3}{\SEM{#3}}}
\newcommand{\SECTHYPER}[3]{\HYPER{#1}{#2}{SectionNumber}{#3}{\SECT{#3}}}
% \LEFTPHRASE MATH \RIGHTPHRASE produces [[ MATH ]] with proper brackets:
\newcommand{\LEFTPHRASE}{\llbracket}
\newcommand{\RIGHTPHRASE}{\rrbracket}
% \LEFTGROUP MATH \RIGHTGROUP produces ( MATH ) where the parentheses are
% highlighted the same as keywords:
\newcommand{\LEFTGROUP}{\STYLE{Key}{(}}
\newcommand{\RIGHTGROUP}{\STYLE{Key}{)}}
% MATH\PLUS produces a superscript +
% MATH\STAR produces a superscript *
% MATH\QUERY produces a superscript ?
\newcommand{\PLUS}{{}^{\texttt{+}}}
\newcommand{\STAR}{{}^{\texttt{*}}}
\newcommand{\QUERY}{{}^{\texttt{?}}}
% \RULE{& PREMISE \\ & ...}{& FORMULA ... \\ & ...} produces an inference rule
% with separately aligned premises and conclusion
% PREMISE
% ...
% -----------
% FORMULA ...
% ...
\newcommand{\RULE}[2]
{\frac{\begin{aligned}#1\end{aligned}}{\begin{aligned}#2\end{aligned}}}
% \AXIOM{& FORMULA ... \\ & ...} produces an aligned formula
%
% FORMULA ...
% ...
\newcommand{\AXIOM}[1]{\begin{aligned}#1\end{aligned}}
% \TO TYPE produces => TYPE
\newcommand{\TO}{\mathop{\Rightarrow}}
% TERM \TRANS TERM produces TERM ---> TERM
\newcommand{\TRANS}{\longrightarrow}
% TERM \xrightarrow{LABEL} TERM puts the label above the long arrow
%
\)
OCaml-Light is a core sublanguage of OCaml, corresponding closely to
Caml-Light (an obsolete pedagogical functional programming language).
Its CBS illustrates scaling up to a medium-sized language.
The start of the specification of OCaml-Light in CBS is at OCaml-Light.
The specification is divided into sections corresponding to Chapter 7 of the
OCaml Manual.
The OCaml-Light language corresponds closely to the language whose static
and dynamic semantics have been specified by Scott Owens in the Ott framework.
The correctness of the CBS semantics (in relation to the implementation
provided by the OCaml developers) has been partially tested by generating
a parser, translator, and interpreter from the specifications, and checking
that the results of running a suite of about 150 small programs using the
generated implementation correspond to the results of running them directly.
Colophon
Status:
abstract syntax: complete, derived from OCaml Manual
dynamic semantics: complete
static semantics: not specified
disambiguation: incomplete, derived from OCaml Manual