Explicit substitutions with de bruijn's levels
From MaRDI portal
Publication:5055838
Cites work
- scientific article; zbMATH DE number 2185670 (Why is no real title available?)
- scientific article; zbMATH DE number 3659007 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- Combinatory logic. With two sections by William Craig.
- Completion for rewriting modulo a congruence
- Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
- Explicit substitutions
- Explicit substitutions with de bruijn's levels
- Partial Applicative Theories and Explicit Substitutions
- λν, a calculus of explicit substitutions which preserves strong normalisation
Cited in
(8)- Problems in rewriting III
- 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
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)
