mx 0.2

Home:  http://libmx.sourceforge.net/
Project:  https://sourceforge.net/projects/libmx/
Download:  https://sourceforge.net/projects/libmx/files/
Lambda calculus:  http://en.wikipedia.org/wiki/Lambda_calculus
Hindley-Milner types http://en.wikipedia.org/wiki/Hindley-Milner
Copyright: 
© 2013 by Peter Belkner <info@pbelkner.de>

01.09.2012  0.2     NPAPI plugin for the Mozilla Firefox web browser
23.08.2013  0.1     Initial release

"mx" is a command line test driver for "libmx" (see below) evaluating
both the type and the value of an lambda calculus expression
(http://en.wikipedia.org/wiki/Lambda_calculus) provided by the user.

"libnpmx.so" ("npmx.dll" on MS Windows) is a NPAPI plugin for the
Mozilla Firefox web browser (http://en.wikipedia.org/wiki/Firefox)
based on "libmx".

"libmx" provides a framework for dealing with (extended and optional typed)
lambda calculus expressions. The abstract syntax supported by the framework
is as follows (cf. "struct mx" in "mx.h"):

// expressions:
ex       =  ex_num | ex_id | ex_bi | ex_br | ex_lam | ex_let | ex_ref
ex_num   =  NUM                 // integer number
ex_id    =  ID                  // identifier
ex_bi    =  OP ARITY tp         // build-in operation on integers
ex_br    =  ex ex ex            // if-then-else branching
ex_lam   =  ID tp? ex           // optional typed lambda abstraction
ex_let   =  ID tp? ex ex        // optional typed (recursive) let
ex_ref   =  ex?                 // updatable reference (optional empty)

// types:
tp       =  tp_cons | tp_op | tp_var
tp_cons  =  CONS                // type constant (MX_INT or MX_BOOL)
tp_op    =  SYM tp tp           // type operator (MX_ARR, i.e. "=>")
tp_var   =  ID GEN tp? tp?      // type variable (optionally linked to a
                                // representative and a fresh instance)

For the concrete syntax supported by "mx" cf. "mx_parser.y".

Among other features the framework provides

  o  a template instantiation machine for evaluating the value of an
     lambda calculus expression,
  o  a template instantiation machine for evaluating the Hindley-Milner
     type (http://en.wikipedia.org/wiki/Hindley-Milner) of an lambda
     calculus expression, and
  o  reference counter based memory management for lambda calculus
     expressions and types.

"libmx" is written in C (C99).