Tight typings and split bounds, fully developed

DOI10.1017/S095679682000012XzbMath1482.68077arXiv1807.02358MaRDI QIDQ5120229

Delia Kesner, Stéphane Graham-Lengrand, Beniamino Accattoli

Publication date: 9 September 2020

Published in: Journal of Functional Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Type inference for rank-2 intersection types using set unification ⋮ Quantitative weak linearisation ⋮ Quantitative global memory ⋮ Tight typings and split bounds, fully developed ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The bang calculus revisited ⋮ A Fresh Look at the λ-Calculus

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A semantic account of strong normalization in linear logic
• A type assignment for \(\lambda\)-calculus complete both for FPTIME and strong normalization
• A relational semantics for parallelism and non-determinism in a functional setting
• A semantic measure of the execution time in linear logic
• Normal functors, power series and \(\lambda\)-calculus
• An extension of basic functionality theory for \(\lambda\)-calculus
• Perpetual reductions in \(\lambda\)-calculus
• Head linear reduction and pure proof net extraction
• Proof nets and the linear substitution calculus
• Call-by-need, neededness and all that
• (In)efficiency and reasonable cost models
• Type-based cost analysis for lazy functional languages
• Linear dependent types in a call-by-value scenario
• A Resource Aware Computational Interpretation for Herbelin’s Syntax
• (Leftmost-Outermost) Beta Reduction is Invariant, Indeed
• Non-idempotent intersection types and strong normalisation
• Local Bigraphs and Confluence: Two Conjectures
• The geometry of types
• Static prediction of heap space usage for first-order functional programs
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types
• Quantitative Types for the Linear Substitution Calculus
• The Inhabitation Problem for Non-idempotent Intersection Types
• A new type assignment for λ-terms
• Call-by-Value Non-determinism in a Linear Logic Type Discipline
• Amortized Resource Analysis with Polynomial Potential
• The Structural λ-Calculus
• Using Intersection Types for Cost-Analysis of Higher-Order Polymorphic Functional Programs
• Inhabitation of Low-Rank Intersection Types
• A linearization of the Lambda-calculus and consequences
• Execution time of λ-terms via denotational semantics and intersection types
• Non-idempotent intersection types for the Lambda-Calculus
• Linear Dependent Types and Relative Completeness
• The emptiness problem for intersection types
• Tight typings and split bounds, fully developed
• Types, potency, and idempotency
• Essential and relational models
• The Relational Model Is Injective for Multiplicative Exponential Linear Logic
• Intersection type calculi of bounded dimension
• A nonstandard standardization theorem
• A Semantical and Operational Account of Call-by-Value Solvability
• Implementation of Functional Languages
• On phase semantics and denotational semantics: The exponentials
• Types of fireballs