Mixed modal/linear lambda calculus with type inference and subtyping

Dear Typists,

As part of a quest for pragmatically more appealing versions of
Bellantoni-Cook's safe recursion scheme I have developed a mixed
linear/modal lambda calculus with subtyping and type inference. The
types of the system are 

A,B ::= N | A -o B | A -> B | $A -o B | $A -> B

The subtyping is generated by A-oB <: A->B <: $A -> B and A-oB <: $A-o
B <: $A -> B. This allows us to have only one kind of functional
abstraction and application; and no term formers referring to
linearity and/or modality. 

The system contains constants for various kinds of safe recursion
whose types make use of modality and linearity. 

A draft paper and a prototype implementation can be found under
http://www.mathematik.th-darmstadt.de/~mh/slr_test.html The
implementation can be tried out via WWW without installing any

Comments are welcome, 

Martin Hofmann                                
AG Logik und mathemat. Grundl. der Informatik
Fachbereich Mathematik                     
Technische Hochschule Darmstadt            
Schlossgartenstrasse 7
D-64289 Darmstadt

Tel.  : x49-6151-16-3615
FAX   : x49-6151-16-4011
e-mail: mh@mathematik.th-darmstadt.de
WWW   : http://www.mathematik.th-darmstadt.de/ags/ag14/mitglieder/hofmann-e.html

- ------- =_aaaaaaaaaa--
------- End of forwarded message -------