Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language L that is completely separate from run-time programs, leading to the DML(L) language schema. This enrichment allows fo...

Full description

Bibliographic Details
Main Author: Hongwei Xi
Other Authors: The Pennsylvania State University CiteSeerX Archives
Format: Text
Language:English
Subjects:
Contents
DML
Online Access:http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.9231
http://www.cs.bu.edu/~hwxi/academic/drafts/DML.pdf
id ftciteseerx:oai:CiteSeerX.psu:10.1.1.117.9231
record_format openpolar
spelling ftciteseerx:oai:CiteSeerX.psu:10.1.1.117.9231 2023-05-15T16:01:46+02:00 Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types Hongwei Xi The Pennsylvania State University CiteSeerX Archives application/pdf http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.9231 http://www.cs.bu.edu/~hwxi/academic/drafts/DML.pdf en eng http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.9231 http://www.cs.bu.edu/~hwxi/academic/drafts/DML.pdf Metadata may be used without restrictions as long as the oai identifier remains attached to it. http://www.cs.bu.edu/~hwxi/academic/drafts/DML.pdf Contents text ftciteseerx 2016-01-07T13:57:44Z We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language L that is completely separate from run-time programs, leading to the DML(L) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types Text DML Unknown
institution Open Polar
collection Unknown
op_collection_id ftciteseerx
language English
topic Contents
spellingShingle Contents
Hongwei Xi
Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types
topic_facet Contents
description We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language L that is completely separate from run-time programs, leading to the DML(L) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types
author2 The Pennsylvania State University CiteSeerX Archives
format Text
author Hongwei Xi
author_facet Hongwei Xi
author_sort Hongwei Xi
title Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types
title_short Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types
title_full Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types
title_fullStr Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types
title_full_unstemmed Under consideration for publication in J. Functional Programming 1 Dependent ML: An Approach to Practical Programming with Dependent Types
title_sort under consideration for publication in j. functional programming 1 dependent ml: an approach to practical programming with dependent types
url http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.9231
http://www.cs.bu.edu/~hwxi/academic/drafts/DML.pdf
genre DML
genre_facet DML
op_source http://www.cs.bu.edu/~hwxi/academic/drafts/DML.pdf
op_relation http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.9231
http://www.cs.bu.edu/~hwxi/academic/drafts/DML.pdf
op_rights Metadata may be used without restrictions as long as the oai identifier remains attached to it.
_version_ 1766397501941743616

Similar Items