Reasoning About Call-by-need by Means of Types

DOI10.1007/978-3-662-49630-5_25zbMath1475.68064OpenAlexW2460688276MaRDI QIDQ2811356

Delia Kesner

Publication date: 10 June 2016

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-49630-5_25

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

Taylor expansion, finiteness and strategies, Unnamed Item, On the value of variables, A strong call-by-need calculus, Node Replication: Theory And Practice, Unnamed Item, The spirit of node replication, The bang calculus revisited, The bang calculus revisited, Unnamed Item, Unnamed Item, Unnamed Item, A Fresh Look at the λ-Calculus, Normalization by Evaluation for Typed Weak lambda-Reduction

Cites Work

• Unnamed Item
• Unnamed Item
• An extension of basic functionality theory for \(\lambda\)-calculus
• Complete restrictions of the intersection type discipline
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Call-by-name, call-by-value, call-by-need and the linear lambda calculus
• Principality and type inference for intersection types using expansion variables
• Distilling abstract machines
• Non-idempotent intersection types and strong normalisation
• The Call-by-Need Lambda Calculus, Revisited
• Quantitative Types for the Linear Substitution Calculus
• The Inhabitation Problem for Non-idempotent Intersection Types
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Solvability in Resource Lambda-Calculus
• Functional Characters of Solvable Terms
• The call-by-need lambda calculus
• The call-by-need lambda calculus
• A linearization of the Lambda-calculus and consequences
• A semantics for lambda calculi with resources
• Types, potency, and idempotency