Higher-order representation of substructural logics

DOI10.1145/1863543.1863565MaRDI QIDQ5176934zbMATH OpenOpenAlexFDO

Authors Karl Crary

Publication date 5 March 2015

Published in Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://figshare.com/articles/journal_contribution/Higher-order_Representation_of_Substructural_Logics/6606116

zbMATH Keywords

linear logiclogical frameworksmechanized metatheorymodal logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Modal logic (including the logic of norms) (03B45) Substructural logics (including relevance, entailment, linear logic, Lambek calculus, BCK and BCI logics) (03B47)

Recommendations

• Encoding modal logics in logical frameworks
• Reasoning with higher-order abstract syntax in a logical framework
• Structured theory presentations and logic representations
• scientific article; zbMATH DE number 7204444
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF

Cited in

(10)

• Structured theory presentations and logic representations
• A third-order representation of the -calculus
• Comparing higher-order encodings in logical frameworks and tile logic
• Proof Pearl: The Power of Higher-Order Encodings in the Logical Framework LF
• Higher-Order Categorical Substructural Logic: Expanding the Horizon of Tripos Theory
• scientific article; zbMATH DE number 7204444 (Why is no real title available?)
• scientific article; zbMATH DE number 7297101 (Why is no real title available?)
• The calculus of dependent lambda eliminations
• A framework for substructural type systems
• A linear algebra approach to linear metatheory

This page was built for publication: Higher-order representation of substructural logics

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