Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence
From MaRDI portal
Publication:2988360
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
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
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