Tight typings and split bounds, fully developed
From MaRDI portal
Publication:5120229
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
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