Completeness and partial soundness results for intersection and union typing for
From MaRDI portal
Publication:636376
Recommendations
- Sound and complete typing for \(\lambda\mu\)
- Completeness and soundness results for \(\mathcal X\) with intersection and union types
- Intersection and union types in the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus
- A Translation of Intersection and Union Types for the λμ-Calculus
- Completeness of intersection and union type assignment systems for call-by-value -models
Cites work
- A filter lambda model and the completeness of type assignment
- A new type assignment for λ-terms
- A syntactic theory of sequential control
- Call-by-value is dual to call-by-name
- Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
- Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
- Complete restrictions of the intersection type discipline
- Completeness of intersection and union type assignment systems for call-by-value -models
- Computation with classical sequents
- Coppo-Dezani types do not correspond to propositional logic
- Cut-elimination in the strict intersection type assignment system is strongly normalizing
- scientific article; zbMATH DE number 3596799 (Why is no real title available?)
- scientific article; zbMATH DE number 1222571 (Why is no real title available?)
- scientific article; zbMATH DE number 1324438 (Why is no real title available?)
- scientific article; zbMATH DE number 482822 (Why is no real title available?)
- scientific article; zbMATH DE number 517083 (Why is no real title available?)
- scientific article; zbMATH DE number 1956517 (Why is no real title available?)
- scientific article; zbMATH DE number 2079018 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- Intersection and union types: Syntax and semantics
- Intersection type assignment systems
- Intersection types and computational effects
- Normalization, approximation, and semantics for combinator systems
- Programming Languages and Systems
- Strict intersection types for the lambda calculus
- Strong normalisation of cut-elimination in classical logic
- Strong Normalization of the Dual Classical Sequent Calculus
- The duality of computation
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Theoretical Computer Science
- Untersuchungen über das logische Schliessen. I
Cited in
(12)- Intersection and union types in the \(\bar{\lambda}\mu\tilde{\mu}\)-calculus
- Soundness and principal contexts for a shallow polymorphic type system based on classical logic
- A Filter Model for the λμ-Calculus
- Approximation semantics and expressive predicate assignment for object-oriented programming (extended abstract)
- Semantic types and approximation for Featherweight Java
- Completeness and soundness results for \(\mathcal X\) with intersection and union types
- Sound and complete typing for \(\lambda\mu\)
- scientific article; zbMATH DE number 7204443 (Why is no real title available?)
- The duality of classical intersection and union types
- Functional type assignment for Featherweight Java. To Rinus Plasmeijer, in honour of his 61st birthday
- Completeness of intersection and union type assignment systems for call-by-value -models
- Completeness of type assignment systems with intersection, union, and type quantifiers
This page was built for publication: Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q636376)
