A linear logical framework

DOI10.1006/inco.2001.2951zbMath1031.03056OpenAlexW3181070739MaRDI 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 logiclogical frameworkdeductive systemslinear type theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (35)

Linear Dependent Type Theory for Quantum Programming Languages ⋮ Mechanizing metatheory in a logical framework ⋮ Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts ⋮ I Got Plenty o’ Nuttin’ ⋮ Finitary type theories with and without contexts ⋮ A logical framework with higher-order rational (circular) terms ⋮ A formal logic for formal category theory ⋮ Towards substructural property-based testing ⋮ A linear logical framework ⋮ POPLMark reloaded: Mechanizing proofs by logical relations ⋮ Additive types in quantitative type theory ⋮ Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax ⋮ Unnamed Item ⋮ Making ``stricterness more relevant ⋮ Graded modal dependent type theory ⋮ Reverse AD at higher types: pure, principled and denotationally correct ⋮ A logical framework combining model and proof theory ⋮ Hybrid and subexponential linear logics ⋮ An Improved Proof-Theoretic Compilation of Logic Programs ⋮ Linear logic propositions as session types ⋮ Unnamed Item ⋮ \(\mathrm{HO}\pi\) in Coq ⋮ Unnamed Item ⋮ Hybrid linear logic, revisited ⋮ Efficient resource management for linear logic proof search ⋮ Proof-search in type-theoretic languages: An introduction ⋮ Formalization of metatheory of the Quipper quantum programming language in a linear logic ⋮ A rewriting logic approach to specification, proof-search, and meta-proofs in sequent systems ⋮ Soft subexponentials and multiplexing ⋮ Hybridizing a Logical Framework ⋮ Program equivalence in linear contexts ⋮ Specifying Properties of Concurrent Computations in CLF ⋮ A Meta Linear Logical Framework ⋮ A focused linear logical framework and its application to metatheory of object logics ⋮ \( \pi\) with leftovers: a mechanisation in Agda

Uses Software

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

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: A linear logical framework