[Prev][Next][Index][Thread]
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
software.
Comments are welcome,
Martin Hofmann
AG Logik und mathemat. Grundl. der Informatik
Fachbereich Mathematik
Technische Hochschule Darmstadt
Schlossgartenstrasse 7
D-64289 Darmstadt
Germany
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 -------