An implementation of the SAX programming language based on a session type
interpretation of pure linear logic with recursion in the form of the
semi-axiomatic sequent calculus

Examples: see lecture15.sax and test.sax

Creating a standalone executable with mlton

% make sax
% ./sax lecture15.sax   (single file)
% make test         (regression testing)

Running interactively in SML/NJ

% sml
- CM.make "sources.cm";
- Top.sax "lecture15.sax";    (* testing single file *)

Version notes

0.1 first release with Assignment 5
0.2 bug fixes

--------------------------------------------------
Grammar
--------------------------------------------------

COMMENTS

'%' <comment> '\n'  for single-line comment
'(*' <comment> '*)' for multi-line, properly nested comment

IDENTIFIERS

<special> ::= [!"#$%&'()*+,-./:;<=>?@[]^_`{|}~] (all except '_\ and whitespace)
<idchar> ::= [a-zA-Z_0-9']*
<id> ::= [a-zA-Z_]<idchar>*
<tag> ::= '<special> | '<idchar>+
<whitespace> ::= [ \n\t\r\v\f]+

Shadowing of variables is disallowed.

OPERATOR PRECEDENCE

<tp> operator precedence

  prec 5: *   (infix, right assoc)
  prec 4: -o  (infix, right assoc)

<val> operator precedence

  ',' is right assoc

<proc> operator precedence

  ';' is right assoc

GRAMMAR

<tp> ::= <id>
       | '1'
       | '+' '{' <alts> '}'
       | '&' '{' <alts> '}'
       | <tp> '*' <tp>
       | <tp> '-o' <tp>
       | '(' <tp> ')'

<alts> ::= <tag> ':' <tp> [ ',' <alts> ]

<parm> ::= '(' <id> ':' <tp> ')'

<val> ::= <id>
        | <tag> <val>
        | <id> ',' <val>
        | '(' ')'
        | '(' <val> ')'

<proc> ::= 'send' <id> <val>
         | 'recv' <id> '(' <cont> ')'
         | 'fwd' <id> <id>
         | 'call' <id> <id> <id>*
         | <id> [ ':' <tp> ] '<-' <proc> ';' <proc>
         | '(' <proc> ')'

<cont> ::= <val> '=>' <proc> [ '|' <cont> ]

<defn> ::= 'type' <id> = <tp>
         | 'proc' <id> <parm> <parms>* = <proc>
         | 'exec' <id>   % requires empty antecedent
         | 'fail' <defn>

<prog> ::= <defn>*