Explicit substitutions with de bruijn's levels

DOI10.1007/3-540-59200-8_65zbMATH Open1503.03028OpenAlexW1589216209MaRDI QIDQ5055838FDOQ5055838

Authors: 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)

Cites Work

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

Cited In (8)

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

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

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