An extension of basic functionality theory for -calculus
From MaRDI portal
An extension of basic functionality theory for \(\lambda\)-calculus
Cited in
(95)- A characterization of F-complete type assignments
- Principal type scheme and unification for intersection type discipline
- Complete restrictions of the intersection type discipline
- Types with intersection: An introduction
- Typing untyped \(\lambda\)-terms, or reducibility strikes again!
- Combining type disciplines
- \(F\)-semantics for type assignment systems
- Proof-functional connectives and realizability
- Intersection type assignment systems
- Normalization results for typeable rewrite systems
- Intersection types and domain operators
- Generalized filter models
- Strong normalization through intersection types and memory
- Typing and computational properties of lambda expressions
- Dependent types with subtyping and late-bound overloading
- Principality and type inference for intersection types using expansion variables
- Intersection types for explicit substitutions
- The bang calculus revisited
- Non-idempotent intersection types in logical form
- Pre-grammars and inhabitation for a subset of rank 2 intersection types
- Intersection-types à la Church
- Linear dependent types in a call-by-value scenario
- Weak linearization of the lambda calculus
- Compositional characterisations of \(\lambda\)-terms using intersection types
- A semantic account of strong normalization in linear logic
- A type assignment for -calculus complete both for FPTIME and strong normalization
- Logical semantics for stability
- Reasoning about call-by-need by means of types
- Simple easy terms
- Strongly normalising cut-elimination with strict intersection types
- Reducibility: a ubiquitous method in lambda calculus with intersection types
- Intersection typed -calculus
- Easy lambda-terms are not always simple
- Finite combinatory logic with intersection types
- A Filter Model for the λμ-Calculus
- Approximation semantics and expressive predicate assignment for object-oriented programming (extended abstract)
- Intersection types for the resource control lambda calculi
- A Datalog recognizer for almost affine -CFGs
- A realizability interpretation for intersection and union types
- Graph lambda theories
- On Isomorphisms of Intersection Types
- Inhabitation of Low-Rank Intersection Types
- Effective λ-models versus recursively enumerable λ-theories
- Intersection, Universally Quantified, and Reference Types
- Semantic types and approximation for Featherweight Java
- A resource aware semantics for a focused intuitionistic calculus
- Inhabitation for non-idempotent intersection types
- A metamodel of access control for distributed environments: applications and properties
- Approximation and normalization results for typeable term rewriting systems
- Intersection types and computational rules
- The emptiness problem for intersection types
- Refinement types for program analysis
- Towards a semantic measure of the execution time in call-by-value lambda-calculus
- The -calculus: syntax and types
- Sequence types for hereditary permutators
- Type Inference for Rank 2 Gradual Intersection Types
- scientific article; zbMATH DE number 7204443 (Why is no real title available?)
- Tight typings and split bounds, fully developed
- Non-idempotent types for classical calculi in natural deduction style
- Strong normalization from an unusual point of view
- Functional type assignment for Featherweight Java. To Rinus Plasmeijer, in honour of his 61st birthday
- Recursive Domain Equations of Filter Models
- Cut-elimination in the strict intersection type assignment system is strongly normalizing
- Implicit computation complexity in higher-order programming languages
- Full abstraction for lambda calculus with resources and convergence testing
- Strictness, totality, and non-standard-type inference
- Higher-order subtyping and its decidability
- Type inference for rank-2 intersection types using set unification
- The bang calculus revisited
- Structural rules and algebraic properties of intersection types
- Quantitative weak linearisation
- Characterization of the principal type of normal forms in an intersection type system
- Linearity and iterator types for Gödel's system \(\mathcal T\)
- Intersection type assignment systems with higher-order algebraic rewriting
- Categorifying non-idempotent intersection types
- A deep quantitative type system
- Pregrammars and intersection types
- Intersection types and denotational semantics: an extended abstract (invited paper)
- Böhm and Taylor for all!
- Mechanized subject expansion in uniform intersection types for perpetual reductions
- Meaningfulness and genericity in a subsuming framework (invited talk)
- Nondeterministic and nonconcurrent computational semantics for \(\mathrm{BB}^+\) and related logics
- Genericity through stratification
- Hybrid intersection types for PCF
- YACC: Yet Another Church Calculus. A birthday present for Herman inspired by his supervisor activity
- Intersection types via finite-set declarations
- Strong normalization through idempotent intersection types: a new syntactical approach
- Lambda galore
- A completeness result for a realisability semantics for an intersection type system
- 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
- The heart of intersection type assignment: Normalisation proofs revisited
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
- An irregular filter model
- A type assignment system for game semantics
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)
