A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
From MaRDI portal
Publication:6597960
DOI10.46298/LMCS-20(3:10)2024MaRDI QIDQ6597960
José Espírito Santo, Delia Kesner, Loïc Peyrot
Publication date: 4 September 2024
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- The \(\lambda \)-calculus and the unity of structural proof theory
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Call-by-push-value: Decomposing call-by-value and call-by-name
- An equivalence between lambda- terms
- Natural deduction with general elimination rules
- Short proofs of normalization for the simply-typed \(\lambda\)-calculus, permutative conversions and Gödel's \(\mathbf T\)
- The polarized \(\lambda\)-calculus
- Variations and interpretations of naturality in call-by-name lambda-calculi with generalized applications
- A Resource Aware Computational Interpretation for Herbelin’s Syntax
- Decidability for non-standard conversions in typed lambda-calculi
- Preservation of strong normalisation modulo permutations for the structural \(\lambda\)-calculus
- A calculus of multiary sequent terms
- Ultimate Normal Forms for Parallelized Natural Deductions
- The Structural λ-Calculus
- A natural extension of natural deduction
- Characterising Strongly Normalising Intuitionistic Terms
- Tight typings and split bounds, fully developed
- Strong Normalization for Truth Table Natural Deduction
- Deriving Natural Deduction Rules from Truth Tables
- Generalized Elimination Inferences, Higher-Level Rules, and the Implications-as-Rules Interpretation of the Sequent Calculus
- Delayed Substitutions
- Parallel reductions in \(\lambda\)-calculus
- Proof Terms for Generalized Natural Deduction
- A faithful and quantitative notion of distant reduction for generalized applications
- Solvability for generalized applications
This page was built for publication: A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6597960)
