Explicit substitutions with de bruijn's levels

DOI10.1007/3-540-59200-8_65zbMath1503.03028OpenAlexW1589216209MaRDI QIDQ5055838

Pierre Lescanne, Jocelyne Rouyer-Degli

Publication date: 9 December 2022

Published in: Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-59200-8_65

Mathematics Subject Classification ID

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

Related Items (8)

Explicit substitutions with de bruijn's levels ⋮ Problems in rewriting III ⋮ Confluence properties of extensional and non-extensional λ-calculi with explicit substitutions (extended abstract) ⋮ Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding ⋮ Internal models of system F for decompilation ⋮ Comparing and implementing calculi of explicit substitutions with eta-reduction ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus

Cites Work

• Combinatory logic. With two sections by William Craig.
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• Completion for rewriting modulo a congruence
• λν, a calculus of explicit substitutions which preserves strong normalisation
• Partial Applicative Theories and Explicit Substitutions
• Explicit substitutions
• Explicit substitutions with de bruijn's levels
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Explicit substitutions with de bruijn's levels