Sciweavers

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

31

ENTCS
2002

favoriteEmaildiscussreport

77views more ENTCS 2002»

Syntactic Type Soundness for HM(X)

13 years 10 months ago

Syntactic Type Soundness for HM(X)

Download www.cs.uvm.edu

The HM(X) framework is a constraint-based type framework with built-in letpolymorphism. This paper establishes purely syntactic type soundness for the framework, treating an extended version of the language containing state and recursive binding. These results demonstrate that any instance of HM(X), comprising a specialized constraint system and possibly additional functional constants and their types, enjoys syntactic type soundness.

Christian Skalka, François Pottier

Real-time Traffic

Built-in Letpolymorphism | Constraint-based Type Framework | ENTCS 2002 | Syntactic Type Soundness |

claim paper

Related Content

» Syntactic Type Soundness for the Region Calculus

» Syntactic Type Soundness Results for the Region Calculus

» StepIndexed Syntactic Logical Relations for Recursive and Quantified Types

» A Syntactic Approach to Foundational ProofCarrying Code

» A Semantics of Object Types

» Component nextgen a sound and expressive component framework for java

» Enriching an Effect Calculus with Linear Types

» Geometry of synthesis a structured approach to VLSI design

» Semicontinuous Sized Types and Termination

Post Info
More Details (n/a)

Added	18 Dec 2010
Updated	18 Dec 2010
Type	Journal
Year	2002
Where	ENTCS
Authors	Christian Skalka, François Pottier

Comments (0)