The Community for Technology Leaders
Logic in Computer Science, Symposium on (1996)
New Brunswick, NJ
July 27, 1996 to July 30, 1996
ISSN: 1043-6871
ISBN: 0-8186-7463-6
pp: 264
ABSTRACT
We present the linear type theory LLF as the formal basis for a conservative extension of the LF logical framework. LLF combines the expressive power of dependent types with linear logic to permit the natural and concise representation of a whole new class of deductive systems, namely those dealing with state. As an example we encode a version of Mini-ML with references including its type system, its operational semantics, and a proof of type preservation. Another example is the encoding of a sequent calculus for classical linear logic and its cut elimination theorem. LLF can also be given an operational interpretation as a logic programming language under which the representations above can be used for type inference, evaluation and cut-elimination.
INDEX TERMS
CITATION

F. Pfenning and I. Cervesato, "A Linear Logical Framework," Logic in Computer Science, Symposium on(LICS), New Brunswick, NJ, 1996, pp. 264.
doi:10.1109/LICS.1996.561339
93 ms
(Ver 3.3 (11022016))