Confluence and strong normalisation of the generalised multiary -calculus

DOI10.1007/978-3-540-24849-1_13MaRDI QIDQ5712305zbMATH OpenOpenAlexFDO

Authors José Espírito Santo, Luís Pinto

Publication date 23 December 2005

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b98246

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Functional programming and lambda calculus (68N18)

Recommendations

• A calculus of multiary sequent terms
• Permutative conversions in intuitionistic multiary sequent calculi with cuts
• Standardization and confluence for a lambda calculus with generalized applications
• Structural Proof Theory as Rewriting
• Confluency and strong normalizability of call-by-value -calculus

Cited in

(8)

• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names.
• Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications
• Standardization and confluence for a lambda calculus with generalized applications
• A formalised first-order confluence proof for the -calculus using one-sorted variable names (Barendregt was right after all . . . almost)
• A calculus of multiary sequent terms
• Permutative conversions in intuitionistic multiary sequent calculi with cuts
• Axiomatic rewriting theory II: the   -calculus enjoys finite normalisation cones
• scientific article; zbMATH DE number 7106482 (Why is no real title available?)

This page was built for publication: Confluence and strong normalisation of the generalised multiary \(\lambda\)-calculus

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