A Linear Spine Calculus

DOI10.1093/LOGCOM/13.5.639MaRDI QIDQ4444935zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

linear lambda calculusuniform provabilityterm assignment systems

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Spinal atomic \(\lambda\)-calculus
• A Terminating and Confluent Linear Lambda Calculus
• Curry-Style Explicit Substitutions for the Linear and Affine Lambda Calculus
• A linearization of the Lambda-calculus and consequences
• scientific article; zbMATH DE number 1086680

Cited in

(24)

• 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
• scientific article; zbMATH DE number 7350767 (Why is no real title available?)
• 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
• The \(\lambda \)-calculus and the unity of structural proof theory
• Superposition with lambdas
• Superposition for higher-order logic
• Two applications of logic programming to Coq
• A linear logical framework
• A type checker for a logical framework with union and intersection types (system description)
• Permutability in proof terms for intuitionistic sequent calculus with cuts
• A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
• Partial proof terms in the study of idealized proof search
• Coherence via focusing for symmetric skew monoidal and symmetric skew closed categories
• 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
• A lambda term representation inspired by linear ordered logic
• Pattern unification for the lambda calculus with linear and affine types

Describes a project that uses

Uses Software

• Elf
• Twelf

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)