A linear logical framework

DOI10.1006/inco.2001.2951zbMath1031.03056MaRDI QIDQ1400718

Frank Pfenning, Iliano Cervesato

Publication date: 4 March 2004

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1006/inco.2001.2951

zbMATH Keywords

linear logic; logical framework; deductive systems; linear type theory

Mathematics Subject Classification ID

03B70: Logic in computer science

03F52: Proof-theoretic aspects of linear logic and other substructural logics

68N30: Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)

Related Items

Mechanizing metatheory in a logical framework, A linear logical framework, Efficient resource management for linear logic proof search, Proof-search in type-theoretic languages: An introduction, Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts

Uses Software

• ML
• HOL
• Twelf
• Automath
• Elf
• mini-ML
• Lolli

Cites Work

• Linear logic
• On the unity of logic
• Computational interpretations of linear logic
• Type inference for polymorphic references
• Strong normalization for typed terms with surjective pairing
• The lambda calculus, its syntax and semantics
• Logic programming in a fragment of intuitionistic linear logic
• A simplified account of polymorphic references
• A syntactic approach to type soundness
• A linear logical framework
• Efficient resource management for linear logic proof search
• Edinburgh LCF. A mechanized logic of computation
• Structural cut elimination. I: Intuitionistic and classical logic
• Contraction-free sequent calculi for intuitionistic logic
• A framework for defining logics
• A relevant analysis of natural deduction
• A Linear Spine Calculus
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item