scientific article; zbMATH DE number 1070568

MaRDI QIDQ4357055zbMATH OpenFDO

Authors Roel Bloo

Publication date 5 October 1997

zbMATH Keywords

combinatory reduction systemsexplicit substitutionspreservation of strong normalizationrecursive path orderssubject reductiontyped \(\lambda\)-calculi

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• scientific article; zbMATH DE number 1342288
• Explicit substitutions and higher-order syntax
• Term Rewriting and Applications
• scientific article; zbMATH DE number 1500649
• scientific article; zbMATH DE number 1761900
• Explicit substitutions
• Explicit substitutions and reducibility
• scientific article; zbMATH DE number 2102742
• Termination of term rewriting by interpretation
• scientific article; zbMATH DE number 2090080

Cited in

(15)

• Explicit substitution. On the edge of strong normalization
• Revisiting the notion of function
• Comparing and implementing calculi of explicit substitutions with eta-reduction
• Intersection types for explicit substitutions
• On explicit substitution with names
• CINNI -- a generic calculus of explicit substitutions and its application to -, - and -calculi
• The Prismoid of Resources
• scientific article; zbMATH DE number 1342288 (Why is no real title available?)
• Comparing calculi of explicit substitutions with eta-reduction
• Combinatory reduction systems with explicit substitution that preserve strong normalisation
• Revisiting Zucker's work on the correspondence between cut-elimination and normalisation
• Strong Normalisation of Cut-Elimination That Simulates β-Reduction
• Proof-term synthesis on dependent-type systems via explicit substitutions
• A prismoid framework for languages with resources
• Capture-avoiding substitution as a nominal algebra

Describes a project that uses

Uses Software

• Automath

This page was built for publication:

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