Types, potency, and idempotency: why nonlinearity and amnesia make a type system work

No abstract is available for this paper.

• Publication year

  2004

• Venue

  ACM SIGPLAN International Conference on Functional Programming

• Publication date

  2004-09-19

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1145/1016850.1016871
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Functional Programming

  2020cited by this paper
• Weak linearization of the lambda calculus

  2005cited by this paper
• Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

  2004cited by this paper
• System E: Expansion Variables for Flexible Typing with Linear and Non-linear Types and Intersection Types

  2004influential reference
• Principality and type inference for intersection types using expansion variables

  2004influential reference
• A conjunctive type system for useless-code elimination

  2003cited by this paper
• Implementing Compositional Analysis Using Intersection Types With Expansion Variables

  2003cited by this paper
• Rank 2 intersection types for modules

  2003cited by this paper
• Rank 2 intersection types for local definitions and conditional expressions

  2003cited by this paper
• From Hilbert Spaces to Dilbert Spaces: Context Semantics Made Simple

  2002cited by this paper
• Strictness, totality, and non-standard-type inference

  2002cited by this paper
• Automatic useless-code elimination for HOT functional programs

  2000cited by this paper
• Relating typability and expressiveness in finite-rank intersection type systems (extended abstract)

  1999cited by this paper
• Principality and decidable type inference for finite-rank intersection types

  1999cited by this paper
• Typability and Type Checking in System F are Equivalent and Undecidable

  1999cited by this paper
• Domains and lambda-calculi

  1998cited by this paper
• The optimal implementation of functional programming languages

  1998cited by this paper
• Inference of polymorphic and conditional strictness properties

  1998cited by this paper
• Exact flow analysis

  1997cited by this paper
• A modular, polyvariant and type-based closure analysis

  1997cited by this paper
• A New Presentation of the Intersection Type Discipline through Principal Typings of Normal Forms

  1996cited by this paper
• A linearization of the Lambda-calculus and consequences

  1996cited by this paper
• What are principal typings and what are they good for?

  1996cited by this paper
• From proof-nets to interaction nets

  1995cited by this paper
• Intersection type disciplines in Lambda Calculus and applicative term rewriting systems

  1993cited by this paper
• Lambda-calcul et reseaux

  1992cited by this paper
• Linear logic without boxes

  1992cited by this paper
• The geometry of optimal lambda reduction

  1992cited by this paper
• Type Systems for Programming Languages

  1991cited by this paper
• Unification and ML-Type Reconstruction

  1991cited by this paper
• Outline of a Proof Theory of Parametricity

  1991cited by this paper
• The Complexity of Type Inference for Higher-Order

  1990cited by this paper
• An algorithm for optimal lambda calculus reduction

  1989cited by this paper
• The structure of multiplicatives

  1989influential reference
• Deciding ML typability is complete for deterministic exponential time

  1989cited by this paper
• Theorems for free!

  1989cited by this paper
• Principal Type Scheme and Unification for Intersection Type Discipline

  1988cited by this paper
• Structure and interpretation of computer programs

  1985cited by this paper
• The Lambda Calculus: Its Syntax and Semantics

  1985cited by this paper
• Principal Type Schemes for an Extended Type Theory

  1984influential reference
• Functional Characters of Solvable Terms

  1981cited by this paper
• To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism

  1980cited by this paper
• The typed λ-calculus is not elementary recursive

  1979cited by this paper
• A Theory of Type Polymorphism in Programming

  1978cited by this paper
• The Principal Type-Scheme of an Object in Combinatory Logic

  1969cited by this paper
• Under Consideration for Publication in J. Functional Programming a Calculus with Polymorphic and Polyvariant Flow Types

  year unknowncited by this paper

• Principal Typing for Intersection Types, Forty-Five Years Later

  2026cites this paper
• Quantitative Types for the Functional Machine Calculus

  2025cites this paper
• Extending the Quantitative Pattern-Matching Paradigm

  2024cites this paper
• Call-by-Value Solvability and Multi Types

  2022cites this paper
• The theory of call-by-value solvability

  2022cites this paper
• Multi types and reasonable space

  2022cites this paper
• Principal Types as Lambda Nets

  2021influential citation
• Tight typings and split bounds, fully developed

  2020cites this paper
• The (In)Efficiency of interaction

  2020cites this paper
• Intersection types and (positive) almost-sure termination

  2020cites this paper
• Types by Need

  2019cites this paper
• Types of Fireballs Beniamino Accattoli , Giulio Guerrieri

  2019cites this paper
• Types by Need (Extended Version)

  2019cites this paper
• Principality and approximation under dimensional bound

  2019cites this paper
• Types of Fireballs (Extended Version)

  2018cites this paper
• Tight typings and split bounds

  2018cites this paper
• Non-idempotent types for classical calculi in natural deduction style

  2018cites this paper
• Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus (Long Version)

  2018cites this paper
• Types of Fireballs

  2018cites this paper
• L O ] 3 0 A ug 2 01 8 Types of Fireballs ( Extended Version )

  2018cites this paper
• Non-idempotent typing operators, beyond the lambda-calculus. (Opérateurs de typage non-idempotents, au delà du lambda-calcul)

  2017cites this paper
• A resource aware semantics for a focused intuitionistic calculus

  2017cites this paper
• Polyadic approximations, fibrations and intersection types

  2017cites this paper
• Execution time of λ-terms via denotational semantics and intersection types

  2017influential citation
• Inhabitation for Non-idempotent Intersection Types

  2017cites this paper
• Generalised species of rigid resource terms

  2017influential citation
• Reasoning About Call-by-need by Means of Types

  2016cites this paper
• Theoretical Aspects of Computing - ICTAC 2015

  2015cites this paper
• A Resource Aware Computational Interpretation for Herbelin's Syntax

  2015cites this paper
• Linear logic, type assignment systems and implicit computational complexity. (Logique linéaire, systèmes de types et complexité implicite)

  2015cites this paper
• Essential and relational models †

  2015cites this paper
• Types intersections non-idempotents pour raffiner la normalisation forte avec des informations quantitatives. (Non idempotent-intersection types to refine strong normalisation with quantitative information)

  2014cites this paper
• Quantitative Types for the Linear Substitution Calculus

  2014cites this paper
• The Inhabitation Problem for Non-idempotent Intersection Types

  2014cites this paper
• Theoretical Computer Science

  2014cites this paper
• Quantitative Types for Intuitionistic Calculi

  2014cites this paper
• Bounding normalization time through intersection types

  2013cites this paper
• Innocent Game Semantics via Intersection Type Assignment Systems

  2013cites this paper
• Non-idempotent intersection types and strong normalisation

  2013cites this paper
• The Complexity of Flow Analysis in Higher-Order Languages

  2013influential citation
• Elaborating intersection and union types

  2012cites this paper
• Higher-Order Model Checking by Abstraction of Type Derivation Rewriting

  2012cites this paper
• Filter Models: Non-idempotent Intersection Types, Orthogonality and Polymorphism

  2011cites this paper
• Complexity of Strongly Normalising λ-Terms via Non-idempotent Intersection Types

  2011cites this paper
• Dependent types from counterexamples

  2010cites this paper
• Solvability in Resource Lambda-Calculus

  2010cites this paper
• Linearity, Non-determinism and Solvability

  2010cites this paper
• Type inference and optimisation for an impure world

  2009cites this paper
• Execution Time of lambda-Terms via Denotational Semantics and Intersection Types

  2009influential citation
• Inhabitation of Low-Rank Intersection Types

  2009cites this paper
• On strong normalization and type inference in the intersection type discipline

  2008cites this paper
• Deciding kCFA is complete for EXPTIME

  2008cites this paper
• Control-flow analysis of functional programs

  2007cites this paper
• A unified system of type refinements

  2007cites this paper
• Relating complexity and precision in control flow analysis

  2007influential citation
• Unification with Expansion Variables : Preliminary Results and Problems ⋆

  2005cites this paper
• Type inference with expansion variables and intersection types in system E and an exact correspondence with β-reduction

  2004cites this paper
• A Functional Language for Logarithmic Space

  2004cites this paper
• about the Internet and Networking : 2010 – 2019

  2003cites this paper
• Mathematical Structures in Computer Science

  year unknowncites this paper
• Under Consideration for Publication in J. Functional Programming Expansion: the Crucial Mechanism for Type Inference with Intersection Types: a Survey and Explanation

  year unknowncites this paper