From: Mark Tarver
Subject: Qi/tk - a type secure graphical extension to Qi
Date: 
Message-ID: <144b196e-14dc-49c0-bde3-70a8841d44b3@v38g2000yqb.googlegroups.com>
Qi/tk 1.01 is a type secure integration of TCL/tk into Qi.  There is a
56 page manual to go with it.

There is a whist program demo program (http://www.lambdassociates.org/
Lib/
graphics/whist.jpg for screen shot) you can download.
*************************************************************************
Some figures.

The type theory for Qi/tk in Lisp was generated from a 511 line Qi
program that used tables to generate sequent calculus axioms that were
compiled into code.  Over 200 rules and axioms were generated
resulting in a 27,000 line Lisp program; more than 3X the size of Qi
itself.

The whist program of 561 lines in its final form took 317,411
inferences to prove type secure using this technology ....

... but took only 5 seconds to prove and load in CLisp.  SBCL would
probably do it in 1-2 seconds but we don't have a port yet.

This is the first constructive existence proof of the scalability of
the Qi approach to a large case.

***************************************************************************
You can get the system from the Qi library.

http://www.lambdassociates.org/Lib/libraries.htm

see the section on Graphics.

The download for Qi/tk does not include TCL/tk.  But you can download
that from the same section or from the TCL/tk homepage.

Note Qi/tk runs under CLisp and Windows only for now.

Features include:

* concurrent graphics and top level
* constraint propagation - dataflow architecture for widgets
* type security for a big piece of TCL/tk
* capacity for user defined attributes for widgets

Menus remain to be done.  They need to be written in Qi/tk itself.
Bug reports to qilang or mail direct to me.

Mark