A Linear Spine Calculus
From MaRDI portal
Publication:4444935
DOI10.1093/LOGCOM/13.5.639zbMATH Open1041.03007OpenAlexW1990946582MaRDI QIDQ4444935FDOQ4444935
Authors: 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
Recommendations
Cited In (18)
- Superposition with lambdas
- Proofs, upside down. A functional correspondence between natural deduction and the sequent calculus
- Structural focalization
- \textsc{Lincx}: a linear logical framework with first-class contexts
- An insider's look at LF type reconstruction: everything you (n)ever wanted to know
- Extensional higher-order paramodulation in Leo-III
- Title not available (Why is that?)
- Higher-order dynamic pattern unification for dependent types and records
- A Note on the Analytical Resolution of a Nonhydrostatic Standing‐Wave Eigenvalue Problem for a Parabolic Basin
- Superposition with lambdas
- The \(\lambda \)-calculus and the unity of structural proof theory
- Superposition for higher-order logic
- A linear logical framework
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Partial proof terms in the study of idealized proof search
- Extending a high-performance prover to higher-order logic
- \textsc{LeoPARD} -- a generic platform for the implementation of higher-order reasoners
- Spinal atomic \(\lambda\)-calculus
Uses Software
This page was built for publication: A Linear Spine Calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4444935)