On reduction and normalization in the computational core

DOI10.1017/S0960129522000433MaRDI QIDQ5879269zbMATH OpenOpenAlexFDO

Authors Claudia Faggian, Giulio Guerrieri, Ugo de'Liguoro, Riccardo Treglia

Publication date 28 February 2023

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2104.10267

zbMATH Keywords

factorizationnormalizationrewritingcomputational lambda-calculus

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 1722652
• Strong normalization in core type theory
• From reduction-based to reduction-free normalization
• Head reduction and normalization in a call-by-value lambda-calculus
• Parallel reductions in \(\lambda\)-calculus

Cites work

• scientific article; zbMATH DE number 4179333 (Why is no real title available?)
• scientific article; zbMATH DE number 6825409 (Why is no real title available?)
• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 2090722 (Why is no real title available?)
• scientific article; zbMATH DE number 7526055 (Why is no real title available?)
• A Semantical and Operational Account of Call-by-Value Solvability
• A reflection on call-by-value
• An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Call-by-value solvability, revisited
• Collapsing non-idempotent intersection types
• Confluence by Decreasing Diagrams
• Confluence by decreasing diagrams
• Effectful applicative bisimilarity: monads, relators, and Howe's method
• Enriching an Effect Calculus with Linear Types
• Factorization in call-by-name and call-by-value calculi via linear logic
• Head reduction and normalization in a call-by-value lambda-calculus
• Modelling environments in call-by-value programming languages.
• Notions of computation and monads
• On theories with a combinatorial definition of 'equivalence'
• Open call-by-value
• Proof nets and the call-by-value \(\lambda\)-calculus
• Term Rewriting and Applications
• The bang calculus and the two Girard's translations
• The bang calculus revisited
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The marriage of effects and monads
• The weak lambda calculus as a reasonable machine

Cited in

(5)

• scientific article; zbMATH DE number 7089070 (Why is no real title available?)
• The benefits of diligence
• Quantitative global memory
• Twin procedures, two kinds of variable binding, and two kinds of computation
• What Is the Limit of Redundancy Reduction with Divisive Normalization?

Describes a project that uses

Uses Software

• Haskell

This page was built for publication: On reduction and normalization in the computational core

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