An extension of basic functionality theory for -calculus
From MaRDI portal
An extension of basic functionality theory for \(\lambda\)-calculus
Cited in
(81)- Cut-elimination in the strict intersection type assignment system is strongly normalizing
- Structural rules and algebraic properties of intersection types
- Dependent types with subtyping and late-bound overloading
- scientific article; zbMATH DE number 7559299 (Why is no real title available?)
- Strong normalization from an unusual point of view
- The heart of intersection type assignment: Normalisation proofs revisited
- The emptiness problem for intersection types
- A Datalog recognizer for almost affine \(\lambda \)-CFGs
- Logical semantics for stability
- Principal type scheme and unification for intersection type discipline
- Characterization of the principal type of normal forms in an intersection type system
- A semantic account of strong normalization in linear logic
- A type assignment for -calculus complete both for FPTIME and strong normalization
- Inhabitation for non-idempotent intersection types
- Pre-grammars and inhabitation for a subset of rank 2 intersection types
- Complete restrictions of the intersection type discipline
- Tight typings and split bounds, fully developed
- scientific article; zbMATH DE number 7526055 (Why is no real title available?)
- scientific article; zbMATH DE number 7204443 (Why is no real title available?)
- A Filter Model for the λμ-Calculus
- scientific article; zbMATH DE number 7559294 (Why is no real title available?)
- Effective λ-models versus recursively enumerable λ-theories
- Intersection type assignment systems
- Compositional characterisations of \(\lambda\)-terms using intersection types
- Weak linearization of the lambda calculus
- Linear dependent types in a call-by-value scenario
- Full abstraction for lambda calculus with resources and convergence testing
- Strong normalization through intersection types and memory
- Recursive Domain Equations of Filter Models
- Intersection typed \(\lambda \)-calculus
- Approximation semantics and expressive predicate assignment for object-oriented programming (extended abstract)
- \(F\)-semantics for type assignment systems
- A type assignment system for game semantics
- Finite combinatory logic with intersection types
- Quantitative weak linearisation
- Implicit computation complexity in higher-order programming languages
- Typing and computational properties of lambda expressions
- A characterization of F-complete type assignments
- Higher-order subtyping and its decidability
- Inhabitation of Low-Rank Intersection Types
- A completeness result for a realisability semantics for an intersection type system
- Typing untyped \(\lambda\)-terms, or reducibility strikes again!
- Intersection types for the resource control lambda calculi
- A metamodel of access control for distributed environments: applications and properties
- Principality and type inference for intersection types using expansion variables
- Reasoning about call-by-need by means of types
- Functional type assignment for Featherweight Java. To Rinus Plasmeijer, in honour of his 61st birthday
- Intersection, Universally Quantified, and Reference Types
- The bang calculus revisited
- Intersection type assignment systems with higher-order algebraic rewriting
- Combining type disciplines
- Approximation and normalization results for typeable term rewriting systems
- Intersection types and computational rules
- Type Inference for Rank 2 Gradual Intersection Types
- The bang calculus revisited
- Refinement types for program analysis
- Intersection types for explicit substitutions
- A realizability interpretation for intersection and union types
- Proof-functional connectives and realizability
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
- Strongly normalising cut-elimination with strict intersection types
- On Isomorphisms of Intersection Types
- Type inference for rank-2 intersection types using set unification
- scientific article; zbMATH DE number 7155170 (Why is no real title available?)
- An irregular filter model
- Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca
- On strong normalization and type inference in the intersection type discipline
- Simple easy terms
- A resource aware semantics for a focused intuitionistic calculus
- Easy lambda-terms are not always simple
- Strictness, totality, and non-standard-type inference
- Types with intersection: An introduction
- Reducibility: a ubiquitous method in lambda calculus with intersection types
- Normalization results for typeable rewrite systems
- Intersection-types à la Church
- Intersection types and domain operators
- Generalized filter models
- Non-idempotent intersection types in logical form
- Semantic types and approximation for Featherweight Java
- Linearity and iterator types for Gödel's system \(\mathcal T\)
- Graph lambda theories
This page was built for publication: An extension of basic functionality theory for \(\lambda\)-calculus
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1134141)
