A focused linear logical framework and its application to metatheory of object logics

DOI10.1017/S0960129521000323MaRDI QIDQ5022931zbMATH OpenOpenAlexFDO

Authors Carlos Olarte, Bruno Xavier, Amy P. Felty

Publication date 20 January 2022

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s0960129521000323

zbMATH Keywords

Coqcut eliminationfocusinglinear logic

Mathematics Subject Classification ID

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

Recommendations

• Mechanizing focused linear logic in Coq
• A fresh view of linear logic as a logical framework
• A framework for proof systems
• scientific article; zbMATH DE number 2152687
• scientific article; zbMATH DE number 1950250

Cites work

• A concurrent constraint programming interpretation of access permissions
• A formal framework for specifying sequent calculus proof systems
• A framework for proof systems
• A fresh view of linear logic as a logical framework
• A hybrid linear logic for constrained transition systems
• A linear logical framework
• A logical framework for modelling breast cancer progression
• A uniform framework for substructural logics with modalities
• An extended framework for specifying and reasoning about proof systems
• Focusing and polarization in linear, intuitionistic, and classical logics
• Formalization of metatheory of the Quipper quantum programming language in a linear logic
• Formalized meta-theory of sequent calculi for linear logics
• From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
• Generic methods for formalising sequent calculi applied to provability logic
• scientific article; zbMATH DE number 2185657 (Why is no real title available?)
• scientific article; zbMATH DE number 1927412 (Why is no real title available?)
• Hybrid linear logic, revisited
• Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Linear logic propositions as session types
• Logic Programming with Focusing Proofs in Linear Logic
• Mechanizing focused linear logic in Coq
• Multi-focused proofs with different polarity assignments
• On subexponentials, focusing and modalities in concurrent systems
• Parametric higher-order abstract syntax for mechanized semantics
• Reasoning with higher-order abstract syntax in a logical framework
• Structural cut elimination. I: Intuitionistic and classical logic
• Structural focalization
• The representational adequacy of Hybrid

Cited in

(5)

• A simplified account of the metatheory of linear LF
• Object calculi in linear logic
• A linear logic framework for multimodal logics
• Facilitating meta-theory reasoning (invited paper)
• YALLA: yet another deep embedding of linear logic in Rocq

Describes a project that uses

Uses Software

• Coq
• HYBRID
• Quipper
• Alcove

This page was built for publication: A focused linear logical framework and its application to metatheory of object logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5022931)