TY - GEN
T1 - The next 700 data description languages
AU - Fisher, Kathleen
AU - Mandelbaum, Yitzhak
AU - Walker, David
N1 - Copyright:
Copyright 2020 Elsevier B.V., All rights reserved.
PY - 2006
Y1 - 2006
N2 - In the spirit of Landin, we present a calculus of dependent types to serve as the semantic foundation for a family of languages called data description languages. Such languages, which include PADS, DATASCRIPT, and PACKETTYPES, are designed to facilitate programming with ad hoc data, i.e., data not in well-behaved relational or XML formats. In the calculus, each type describes the physical layout and semantic properties of a data source. In the semantics, we interpret types simultaneously as the in-memory representation of the data described and as parsers for the data source. The parsing functions are robust, automatically detecting and recording errors in the data stream without halting parsing. We show the parsers are type-correct, returning data whose type matches the simple-type interpretation of the specification. We also prove the parsers are "error-correct," accurately reporting the number of physical and semantic errors that occur in the returned data. We use the calculus to describe the features of various data description languages, and we discuss how we have used the calculus to improve PADS.
AB - In the spirit of Landin, we present a calculus of dependent types to serve as the semantic foundation for a family of languages called data description languages. Such languages, which include PADS, DATASCRIPT, and PACKETTYPES, are designed to facilitate programming with ad hoc data, i.e., data not in well-behaved relational or XML formats. In the calculus, each type describes the physical layout and semantic properties of a data source. In the semantics, we interpret types simultaneously as the in-memory representation of the data described and as parsers for the data source. The parsing functions are robust, automatically detecting and recording errors in the data stream without halting parsing. We show the parsers are type-correct, returning data whose type matches the simple-type interpretation of the specification. We also prove the parsers are "error-correct," accurately reporting the number of physical and semantic errors that occur in the returned data. We use the calculus to describe the features of various data description languages, and we discuss how we have used the calculus to improve PADS.
KW - Data description language
KW - Dependent types
KW - Domain-specific languages
UR - http://www.scopus.com/inward/record.url?scp=33745830891&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=33745830891&partnerID=8YFLogxK
U2 - 10.1145/1111037.1111039
DO - 10.1145/1111037.1111039
M3 - Conference contribution
AN - SCOPUS:33745830891
SN - 1595930272
SN - 9781595930279
T3 - Conference Record of the Annual ACM Symposium on Principles of Programming Languages
SP - 2
EP - 15
BT - Conference Record of POPL 2006
PB - Association for Computing Machinery
T2 - 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'06
Y2 - 11 January 2006 through 13 January 2006
ER -