Normalization, approximation, and semantics for combinator systems
This paper studies normalization of typeable terms and the relation between approximation semantics and filter models for combinator systems. It presents notions of approximants for terms, intersection type assignment, and reduction on type derivations; the last will be proved to be strongly normalizable. With this result, it is proved that every typeable term has an approximant with the same type, and a characterization of the normalization behaviour of terms using their assignable types is given. Then the two semantics are defined and compared, and it is shown that the approximants semantics is fully abstract but the filter semantics is not.
- Approximation and normalization results for typeable term rewriting systems
- The heart of intersection type assignment: Normalisation proofs revisited
- A filter lambda model and the completeness of type assignment
- (Head-)normalization of typeable rewrite systems
- A Filter Model for Concurrent \lambda-Calculus
- A filter lambda model and the completeness of type assignment
- Approximation and normalization results for typeable term rewriting systems
- Combinatory logic. With two sections by William Craig.
- Complete restrictions of the intersection type discipline
- Full abstraction and limiting completeness in equational languages
- Functional Characters of Solvable Terms
- Functionality in Combinatory Logic
- scientific article; zbMATH DE number 108434 (Why is no real title available?)
- scientific article; zbMATH DE number 599028 (Why is no real title available?)
- scientific article; zbMATH DE number 1142316 (Why is no real title available?)
- scientific article; zbMATH DE number 1142322 (Why is no real title available?)
- Intensional interpretations of functionals of finite type I
- Intersection type assignment systems
- Intersection types for combinatory logic
- Normalization results for typeable rewrite systems
- Principal type schemes for an extended type theory
- Principal Type Schemes for the Strict Type Assignment System
- Sequentiality in orthogonal term rewriting systems
- The lambda calculus. Its syntax and semantics. Rev. ed.
- The Relation between Computational and Denotational Properties for Scott’s ${\text{D}}_\infty $-Models of the Lambda-Calculus
- Approximation semantics and expressive predicate assignment for object-oriented programming (extended abstract)
- Semantic types and approximation for Featherweight Java
- scientific article; zbMATH DE number 598799 (Why is no real title available?)
- Approximation and normalization results for typeable term rewriting systems
- Functional type assignment for Featherweight Java. To Rinus Plasmeijer, in honour of his 61st birthday
- Cut-elimination in the strict intersection type assignment system is strongly normalizing
- Explicit Composition and Its Application in Proofs of Normalization
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
This page was built for publication: Normalization, approximation, and semantics for combinator systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1853619)
