A focused linear logical framework and its application to metatheory of object logics
From MaRDI portal
Publication:5022931
DOI10.1017/S0960129521000323OpenAlexW3213158637MaRDI QIDQ5022931
Bruno Xavier, Carlos Olarte, 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
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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.
- A framework for proof systems
- Focusing and polarization in linear, intuitionistic, and classical logics
- A linear logical framework
- Multi-focused proofs with different polarity assignments
- Structural cut elimination. I: Intuitionistic and classical logic
- A formal framework for specifying sequent calculus proof systems
- A fresh view of linear logic as a logical framework
- Formalization of metatheory of the Quipper quantum programming language in a linear logic
- Mechanizing focused linear logic in Coq
- On subexponentials, focusing and modalities in concurrent systems
- Formalized meta-theory of sequent calculi for linear logics
- Structural Focalization
- The representational adequacy of <scp>Hybrid</scp>
- From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
- Logic Programming with Focusing Proofs in Linear Logic
- A concurrent constraint programming interpretation of access permissions
- A uniform framework for substructural logics with modalities
- Generic Methods for Formalising Sequent Calculi Applied to Provability Logic
- Parametric higher-order abstract syntax for mechanized semantics
- Hybrid linear logic, revisited
- Reasoning with higher-order abstract syntax in a logical framework
- An extended framework for specifying and reasoning about proof systems
- Linear logic propositions as session types
- A logical framework for modelling breast cancer progression
This page was built for publication: A focused linear logical framework and its application to metatheory of object logics
