Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence

DOI10.1007/978-3-662-54458-7_4zbMath1486.68035OpenAlexW2963145380MaRDI QIDQ2988360

Naoki Kobayashi, Takeshi Tsukada, Ryoma Sin'ya, Kazuyuki Asada

Publication date: 19 May 2017

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-662-54458-7_4

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatory logic and lambda calculus (03B40)

Related Items

Distribution of variables in lambda-terms with restrictions on De Bruijn indices and De Bruijn levels, Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence, Unnamed Item, Unnamed Item

Uses Software

• MoCHi

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Exact bounds for lengths of reductions in typed λ-calculus
• A Natural Counting of Lambda Terms
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence
• Asymptotically almost all \lambda-terms are strongly normalizing
• Types and higher-order recursion schemes for verification of higher-order programs
• Counting and generating lambda terms
• A type-directed abstraction refinement approach to higher-order model checking
• Verifying higher-order functional programs with pattern-matching algebraic data types
• Computational Complexity