A lambda term representation inspired by linear ordered logic

DOI10.4204/EPTCS.71.1MaRDI QIDQ6940448zbMATH OpenFDO

Authors Andreas Abel, Nicolai Kraus

Publication date 19 August 2025

Copyright license Creative Commons license

Full work available at URL https://doi.org/10.4204/EPTCS.71.1

zbMATH Keywords

explicit substitutionslogical frameworkordered contextsrepresentation of bindersspace leaks

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18)

Cites work

• A compiled implementation of strong reduction
• A Linear Spine Calculus
• An algorithm for type-checking dependent types
• Choices in representation and reduction strategies for lambda terms in intensional contexts
• Contification using dominators
• Director Strings Revisited: A Generic Approach to the Efficient Representation of Free Variables in Higher-order Rewriting
• Explicit substitutions
• scientific article; zbMATH DE number 1692888 (Why is no real title available?)
• scientific article; zbMATH DE number 1332647 (Why is no real title available?)
• scientific article; zbMATH DE number 1342286 (Why is no real title available?)
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• Lambda-calculus with director strings
• Linear logic
• Resource operators for \(\lambda\)-calculus
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The view from the left

This page was built for publication: A lambda term representation inspired by linear ordered logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6940448)