[TYPES/announce] Matita Web Interface

[Andrea Asperti]

We are pleased to announce the first release of the Matita Web Interface:

http://matita.cs.unibo.it/matitaweb.shtml

Matita <http://matita.cs.unibo.it/> is a light-weight implementation of 
the Calculus of Inductive Construction akin,
for many respects, to the recent SSreflect dialect.

The web inteface provides full on-line access to most system 
functionalities.
There is nothing to install: you can immediately start playing with the 
prover.
The release comprises a first version of the Matita Online Tutorial, 
covering basic
Matita usage, constructive logic, and core topics in the theory of 
formal languages.
The novelty is that not only the course is completely formalized, but it 
is also immediately
executable.

-- Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen