A logical framework with higher-order rational (circular) terms

DOI10.1007/978-3-031-30829-1_4arXiv2210.06663OpenAlexW4366551135MaRDI QIDQ6091181

Zhibo Chen, Frank Pfenning

Publication date: 24 November 2023

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

Full work available at URL: https://arxiv.org/abs/2210.06663

zbMATH Keywords

logical frameworkscircular proofsregular Böhm trees

Mathematics Subject Classification ID

Theory of computing (68Qxx) Theory of software (68Nxx)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• On equal \(\mu \)-terms
• Fundamental properties of infinite trees
• Lambda calculus with explicit recursion
• A linear logical framework
• Sequent calculi for induction and infinite descent
• Theory of finite or infinite trees revisited
• Subtyping, Declaratively
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A framework for defining logics
• Regular Böhm trees
• On equivalence and canonical forms in the LF type theory
• A proof theory for generic judgments
• Mechanizing metatheory in a logical framework
• Automated Reasoning with Analytic Tableaux and Related Methods
• Types for Proofs and Programs