Abstract

We present an approach to enriching ML’s type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure inference for the resulting system is no longer possible, but we show that typechecking a sufficiently ann...

Full description

Bibliographic Details
Main Authors: Hongwei Xi, Frank Pfenning
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Published: 1997
Subjects:
DML
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.1857
http://www.cs.cmu.edu/~fp/papers/dml97.pdf
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.67.1857
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.67.1857 2023-05-15T16:01:25+02:00 Abstract Hongwei Xi Frank Pfenning The Pennsylvania State University CiteSeerX Archives 1997 application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.1857 http://www.cs.cmu.edu/~fp/papers/dml97.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.1857 http://www.cs.cmu.edu/~fp/papers/dml97.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.cs.cmu.edu/~fp/papers/dml97.pdf text 1997 ftciteseerx 2016-01-08T17:17:05Z We present an approach to enriching ML’s type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure inference for the resulting system is no longer possible, but we show that typechecking a sufficiently annotated program can be reduced to constraint satisfaction. We exhibit the unobtrusiveness of our approach through practical examples (including static array bounds checking) and prove that DML(C) is conservative over ML. The main technical contribution of the paper lies in our language design, including its elaboration and type-checking rules which make the approach practical. 1 Text DML Unknown
institution Open Polar
collection Unknown
op_collection_id ftciteseerx
language English
description We present an approach to enriching ML’s type system with a form of dependent types, where index objects are restricted to some constraint domains C, leading to the DML(C) language schema. Pure inference for the resulting system is no longer possible, but we show that typechecking a sufficiently annotated program can be reduced to constraint satisfaction. We exhibit the unobtrusiveness of our approach through practical examples (including static array bounds checking) and prove that DML(C) is conservative over ML. The main technical contribution of the paper lies in our language design, including its elaboration and type-checking rules which make the approach practical. 1
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Hongwei Xi
Frank Pfenning
spellingShingle Hongwei Xi
Frank Pfenning
Abstract
author_facet Hongwei Xi
Frank Pfenning
author_sort Hongwei Xi
title Abstract
title_short Abstract
title_full Abstract
title_fullStr Abstract
title_full_unstemmed Abstract
title_sort abstract
publishDate 1997
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.1857
http://www.cs.cmu.edu/~fp/papers/dml97.pdf
genre DML
genre_facet DML
op_source http://www.cs.cmu.edu/~fp/papers/dml97.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.67.1857
http://www.cs.cmu.edu/~fp/papers/dml97.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766397285965496320

Similar Items