scientific article; zbMATH DE number 7029315

MaRDI QIDQ4625705zbMATH OpenFDO

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

Publication date 25 February 2019

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

Mathematics Subject Classification ID

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

Recommendations

• Almost every simply typed -term has a long -reduction sequence
• An upper bound for reduction sequences in the typed -calculus
• Exact bounds for lengths of reductions in typed -calculus
• Effective longest and infinite reduction paths in untyped λ-calculi
• BCK-combinators and linear \(\lambda\)-terms have types
• A completeness result for the simply typed \(\lambda \mu \)-calculus
• On the uniqueness of \(\beta\delta\)-normal form of typed \(\lambda\)-terms for the canonical notion of \(\delta\)-reduction
• The simply typed theory of \(\beta\)-conversion has no maximum extension
• Reducibility Proofs in the λ-Calculus
• A necessary and sufficient condition for the uniqueness of \(\beta\delta\)-normal form of typed \(\lambda\)-terms for the canonical notion of \(\delta\)-reduction

Cites work

• A concrete approach to classical analysis
• A natural counting of lambda terms
• A type-directed abstraction refinement approach to higher-order model checking
• Almost every simply typed -term has a long -reduction sequence
• Analytic combinatorics
• Asymptotically almost all \lambda-terms are strongly normalizing
• Complexity analysis of term-rewriting systems
• Computational Complexity
• Counting and generating lambda terms
• Exact bounds for lengths of reductions in typed -calculus
• scientific article; zbMATH DE number 5852776 (Why is no real title available?)
• scientific article; zbMATH DE number 125891 (Why is no real title available?)
• scientific article; zbMATH DE number 475420 (Why is no real title available?)
• scientific article; zbMATH DE number 2087432 (Why is no real title available?)
• Model checking higher-order programs
• On the likelihood of normalization in combinatory logic
• Patterns and pattern-matching in trees: An analysis
• Saturation-Based Model Checking of Higher-Order Recursion Schemes.
• Semantic evaluation; intersection types and complexity of simply typed lambda calculus
• Types and higher-order recursion schemes for verification of higher-order programs
• Verifying higher-order functional programs with pattern-matching algebraic data types

Cited in

(6)

• Exact bounds for lengths of reductions in typed -calculus
• Almost every simply typed -term has a long -reduction sequence
• Statman's hierarchy theorem
• Simply typed convertibility is \textsc{Tower}-complete even for safe lambda-terms
• On average-case hardness of higher-order model checking
• Deciding sparseness of regular languages of finite trees and infinite words

Describes a project that uses

Uses Software

• MoCHi

This page was built for publication:

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