Strong normalization of substitutions

DOI10.1093/LOGCOM/6.6.799MaRDI QIDQ2785671zbMATH OpenOpenAlexFDO

Authors Pierre-Louis Curien, Thérèse Hardin, A. Ríos

Publication date 26 October 1997

Published in Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1093/logcom/6.6.799

zbMATH Keywords

\(\lambda\sigma\)-calculuscalculus of substitutionscategorical combinatory logicexplicit substitutionsextended \(\lambda\)-calculusstrong normalizationtermination of substitution calculi

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1342288
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
• Explicit substitutions
• A -calculus with explicit weakening and explicit substitution

Cited in

(22)

• Categorical abstract machines for higher-order typed -calculi
• Normalisation for higher-order calculi with explicit substitutions
• Formalizing strong normalization proofs of explicit substitution calculi in ALF
• Proof of termination of the rewriting system SUBSET on CCL
• Higher-order substitutions
• Strong normalisation in -calculi with references
• scientific article; zbMATH DE number 2086241 (Why is no real title available?)
• scientific article; zbMATH DE number 4162999 (Why is no real title available?)
• The structural \(\lambda \)-calculus
• Implementing a normalizer using sized heterogeneous types
• Functional runtime systems within the lambda-sigma calculus
• scientific article; zbMATH DE number 1301734 (Why is no real title available?)
• scientific article; zbMATH DE number 1342288 (Why is no real title available?)
• scientific article; zbMATH DE number 1512610 (Why is no real title available?)
• Explicit substitutions à la de Bruijn: the local and global way
• Explicit substitutions
• scientific article; zbMATH DE number 1420789 (Why is no real title available?)
• Hereditary substitution for the \(\lambda \Delta \)-calculus
• Towards the average-case analysis of substitution resolution in \(\lambda\)-calculus
• Functional and Logic Programming
• Delayed Substitutions
• A note on preservation of strong normalisation in the \(\lambda \)-calculus

This page was built for publication: Strong normalization of substitutions

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