A Schema for Adding Dependent Types to ML

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 type-checking a sufficient...

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.50.6863
http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.50.6863
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.50.6863 2023-05-15T16:01:27+02:00 A Schema for Adding Dependent Types to ML Hongwei Xi Frank Pfenning The Pennsylvania State University CiteSeerX Archives 1997 application/postscript http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863 http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863 http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz text 1997 ftciteseerx 2016-01-08T09:03:52Z 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 type-checking 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. 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 type-checking 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.
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Hongwei Xi
Frank Pfenning
spellingShingle Hongwei Xi
Frank Pfenning
A Schema for Adding Dependent Types to ML
author_facet Hongwei Xi
Frank Pfenning
author_sort Hongwei Xi
title A Schema for Adding Dependent Types to ML
title_short A Schema for Adding Dependent Types to ML
title_full A Schema for Adding Dependent Types to ML
title_fullStr A Schema for Adding Dependent Types to ML
title_full_unstemmed A Schema for Adding Dependent Types to ML
title_sort schema for adding dependent types to ml
publishDate 1997
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863
http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz
genre DML
genre_facet DML
op_source http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.50.6863
http://foxnet.cs.cmu.edu/people/fp/papers/dml97.ps.gz
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766397295804284928

Similar Items