A Linear Spine Calculus
From MaRDI portal
Publication:4444935
DOI10.1093/logcom/13.5.639zbMath1041.03007OpenAlexW1990946582MaRDI QIDQ4444935
Iliano Cervesato, Frank Pfenning
Publication date: 28 January 2004
Published in: Journal of Logic and Computation (Search for Journal in Brave)
Full work available at URL: https://semanticscholar.org/paper/0231f1086267ec15ef2afb83b06db0c6fa556e03
Related Items
LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners ⋮ Proofs, Upside Down ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Structural Focalization ⋮ Unnamed Item ⋮ A linear logical framework ⋮ Superposition for higher-order logic ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ LINCX: A Linear Logical Framework with First-Class Contexts ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ An insider's look at LF type reconstruction: everything you (n)ever wanted to know ⋮ The \(\lambda \)-calculus and the unity of structural proof theory ⋮ Superposition with lambdas ⋮ Superposition with lambdas
Uses Software
