Standardization and confluence for a lambda calculus with generalized applications

DOI10.1007/10721975_10MaRDI QIDQ2723897zbMATH OpenFDO

Authors Felix Joachimski, Ralph Matthes

Publication date 8 July 2001

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

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

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Grammars and rewriting systems (68Q42)

Recommendations

• The permutative -calculus
• Compositional Z: confluence proofs for permutative conversion
• \(\lambda_{\beta'}\) -- a \(\lambda\)-calculus with a generalized \(\beta\)-reduction rule
• Types for Proofs and Programs
• Confluence of the lambda calculus with left-linear algebraic rewriting

Cited in

(18)

• Continuous normalization for the lambda-calculus and Gödel's T
• Confluence of the coinductive \(\lambda\)-calculus
• Strong normalization of classical natural deduction with disjunctions
• Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications
• The mechanisation of Barendregt-style equational proofs (the residual perspective)
• The permutative -calculus
• Characterising Strongly Normalising Intuitionistic Sequent Terms
• Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
• scientific article; zbMATH DE number 6825409 (Why is no real title available?)
• scientific article; zbMATH DE number 800564 (Why is no real title available?)
• Compositional Z: confluence proofs for permutative conversion
• scientific article; zbMATH DE number 7106482 (Why is no real title available?)
• Standardization of a Call-By-Value Lambda-Calculus
• Types for Proofs and Programs
• A faithful and quantitative notion of distant reduction for generalized applications
• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• Permutability in proof terms for intuitionistic sequent calculus with cuts
• On model-theoretic strong normalization for truth-table natural deduction

This page was built for publication: Standardization and confluence for a lambda calculus with generalized applications

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