scientific article; zbMATH DE number 1956517

MaRDI QIDQ4417863zbMATH OpenFDO

Authors Joshua Dunfield, Frank Pfenning

Publication date 30 July 2003

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2620/26200250.htm

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

Recommendations

• Completeness of intersection and union type assignment systems for call-by-value -models
• Intersection and union types: Syntax and semantics
• The duality of classical intersection and union types
• Intersection and union types for \(\mathcal{X}\)
• Subtyping and intersection types revisited

Cited in

(26)

• Call-by-value, elementary time and intersection types
• Intersection and union types for \(\mathcal{X}\)
• Elaborating intersection and union types
• Intersection types and computational effects
• Elaborating evaluation-order polymorphism
• Extensible Datasort Refinements
• A type system for call-by-name exceptions
• A System F with Call-by-Name Exceptions
• Inhabitation in Intersection and Union Type Assignment Systems
• Untangling typechecking of intersections and unions
• Taming the merge operator
• Semantic subtyping for non-strict languages
• Set constraints, pattern match analysis, and SMT
• Elaborating intersection and union types
• Subtyping and intersection types revisited
• The duality of classical intersection and union types
• Programming Languages and Systems
• Computer Science Logic
• Completeness of intersection and union type assignment systems for call-by-value -models
• Type inference for rank-2 intersection types using set unification
• Encoding tight typing in a unified framework
• Structural rules and algebraic properties of intersection types
• Polarized subtyping
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Pregrammars and intersection types
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4417863)