A Linear Spine Calculus

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

• 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

zbMATH Keywords

linear lambda calculusuniform provabilityterm assignment systems

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (17)

• Superposition with lambdas
• 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
• LeoPARD — A Generic Platform for the Implementation of Higher-Order Reasoners
• Proofs, Upside Down
• A Note on the Analytical Resolution of a Nonhydrostatic Standing‐Wave Eigenvalue Problem for a Parabolic Basin
• Superposition with lambdas
• Structural Focalization
• LINCX: A Linear Logical Framework with First-Class Contexts
• 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

Uses Software

• Twelf
• Elf

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)