Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications

DOI10.46298/lmcs-19(4:34)2023arXiv2211.05608OpenAlexW4389986185MaRDI QIDQ6178717

Lionel Vaux Auclair, Unnamed Author

Publication date: 16 January 2024

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

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

zbMATH Keywords

Taylor expansionlambda-calculusinfinitary rewritingprogram approximationsemantics of program languages

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A relational semantics for parallelism and non-determinism in a functional setting
• Linear logic
• A new approach to abstract syntax with variable binding
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Uniformity and the Taylor expansion of ordinary lambda-terms
• Set-theoretical models of lambda-calculus: theories, expansions, isomorphisms
• Normal functors, power series and \(\lambda\)-calculus
• Infinitary lambda calculus
• On the algebraic models of lambda calculus
• The differential lambda-calculus
• Confluence of the coinductive \(\lambda\)-calculus
• Inductive types and type constraints in the second-order lambda calculus
• Nominal Sets
• Probabilistic operational semantics for the lambda calculus
• An Alpha-Corecursion Principle for the Infinitary Lambda Calculus
• Meaningless terms in rewriting
• Decomposing the Lattice of Meaningless Sets in the Infinitary Lambda Calculus
• A very modal model of a modern, major, general type system
• Not Enough Points Is Enough
• Proving termination with multiset orderings
• The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
• Infinitary lambda calculi and böhm models
• On the Taylor expansion of probabilistic λ-terms
• Taylor expansion, β-reduction and normalization
• A Coinductive Confluence Proof for Infinitary Lambda-Calculus
• Practical coinduction
• Types for Hereditary Head Normalizing Terms
• Finiteness spaces
• Taylor expansion for Call-By-Push-Value
• Logical Approaches to Computational Barriers

This page was built for publication: Finitary Simulation of Infinitary $\beta$-Reduction via Taylor Expansion, and Applications