A Meta Linear Logical Framework

DOI10.1016/j.entcs.2007.11.016zbMath1278.03061OpenAlexW2140623168MaRDI QIDQ2871843

Andrew McCreight, Carsten Schuermann

Publication date: 10 January 2014

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.11.016

zbMATH Keywords

logical framework\(\mathcal{L}^+_{\omega}\)linear logical frameworkmeta languagemeta logic

Mathematics Subject Classification ID

Logic in computer science (03B70)

Related Items

Towards substructural property-based testing, Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax, LINCX: A Linear Logical Framework with First-Class Contexts, Case Analysis of Higher-Order Data

Uses Software

• Isabelle
• HOL Light

Cites Work

• Linear logic
• Isabelle. A generic theorem prover
• A linear logical framework
• A framework for defining logics
• A proof theory for generic judgments
• Automated Deduction – CADE-19
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item