A Linear Logical Framework

We present the linear type theory λ Π⊸&⊤ as the formal basis for LLF, a conservative extension of the logical framework LF. 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 th...

Full description

Saved in:
Bibliographic Details
Published in:Information and computation 2002-11, Vol.179 (1), p.19-75
Main Authors: Cervesato, Iliano, Pfenning, Frank
Format: Article
Language:English
Subjects:
Applied sciences
Computer science
control theory
systems
Exact sciences and technology
General logic
Language theory and syntactical analysis
Logic and foundations
Mathematical logic, foundations, set theory
Mathematics
Programming languages
Sciences and techniques of general use
Software
Software engineering
Theoretical computing
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We present the linear type theory λ Π⊸&⊤ as the formal basis for LLF, a conservative extension of the logical framework LF. 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 mutable references including its type system and its operational semantics and describe how to take practical advantage of the representation of its computations.
ISSN:0890-5401
1090-2651
DOI:10.1006/inco.2001.2951