Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

12

FOSSACS
2003
Springer

favoriteEmaildiscussreport

112views Software Engineering» more FOSSACS 2003»

Type Assignment for Intersections and Unions in Call-by-Value Languages

13 years 9 months ago

Type Assignment for Intersections and Unions in Call-by-Value Languages

Download www.cs.cmu.edu

We develop a system of type assignment with intersection types, union types, indexed types, and universal and existential dependent types that is sound in a call-by-value functional language. The combination of logical and computational principles underlying our formulation naturally leads to the central idea of type-checking subterms in evaluation order. We thereby provide a uniform generalization and explanation of several earlier isolated systems. The proof of progress and type preservation, usually formulated for closed terms only, relies on a notion of deﬁnite substitution.

Joshua Dunfield, Frank Pfenning

Real-time Traffic

Applied Computing | Call-by-value Functional Language | Existential Dependent Types | FOSSACS 2003 | Intersection Types |

claim paper

Related Content

» Logic and Computation in a Lambda Calculus with Intersection and Union Types

» From Polyvariant Flow Information to Intersection and Union Types

» Program Representation Size in an Intermediate Language with Intersection and Union Types

» Tridirectional typechecking

» Characterizing strong normalization in a language with control operators

» A Typed Intermediate Language for FlowDirected Compilation

» Rank 2 Types for Term Graph Rewriting

» Intersection types and computational effects

» A calculus with polymorphic and polyvariant flow types

Post Info
More Details (n/a)

Added	06 Jul 2010
Updated	06 Jul 2010
Type	Conference
Year	2003
Where	FOSSACS
Authors	Joshua Dunfield, Frank Pfenning

Comments (0)