More Web Proxy on the site http://driver.im/

Article

Free access

Using dependent types to express modular structure

Author:

David B. MacQueenAuthors Info & Claims

POPL '86: Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

Pages 277 - 286

https://doi.org/10.1145/512644.512670

Published: 01 January 1986 Publication History

Abstract

Writing any large program poses difficult problems of organization. In many modern programming languages these problems are addressed by special linguistic constructs, variously known as modules, packages, or clusters, which provide for partitioning programs into manageable components and for securely combining these components to form complete programs. Some general purpose components are able to take on a life of their own, being separately compiled and stored in libraries of generic, reusable program units. Usually modularity constructs also support some form of information hiding, such as "abstract data types." "Programming in the large" is concerned with using such constructs to impose structure on large programs, in contrast to "programming in the small", which deals with the detailed implementation of algorithms in terms of data structures and control constructs. Our goal here is to examine some of the proposed linguistic notions with respect to how they meet the pragmatic requirements of programming in the large.

References

[1]

{BC85} J. L. Bates and R. L. Constable, Proofs as Programs, ACM Trans. on Programming Languages and Systems, 7, 1, January 1985, pp 113--136.

Digital Library

[2]

{BDD80} H. Boehm, A. Demers, and J. Donahue, An informal description of Russell, Technical Report TR 80-430, Computer Science Dept., Cornell Univ., October 1980.

Digital Library

[3]

{BL84} R. M. Burstall and B. Lampson, A kernel language for abstract data types and modules, in Semantics of Data Types, G. Kahn, D. B. MacQueen, and G. Plotkin, eds., LNCS, Vol 173, Springer-Verlag, Berlin, 1984.

Digital Library

[4]

{Bur84} R. M. Burstall, Programming with modules as typed functional programming, Int'l Conf. on 5th Generation Computing Systems, Tokyo, Nov. 1984.

[5]

{Car85} L. Cardelli, The impredicative typed &lambda;-calculus, unpublished manuscript, 1985.

[6]

{CF58} H. B. Curry and R. Feys, Combinatory Logic I, North-Holland, 1958.

[7]

{CH85} T. Coquand and G. Huet, A calculus of constructions, Information and Control, to appear.

[8]

{CM85} L. Cardelli and D. B. MacQueen, Persistence and type abstraction, Proceedings of the Appin Workshop on Data Types and Persistence, Aug 1985, to appear.

Digital Library

[9]

{CW85} L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Technical Report No. CS-85-14, Brown University, August 1985.

Digital Library

[10]

{CZ84} R. L. Constable and D. R. Zlatin, The type theory of PL/CV3, ACM Trans. on Programming Languages and Systems, 6, 1. January 1984, pp. 94--117.

Digital Library

[11]

{dcB80} N. G. de Bruijn. A survey of project AUTOMATH, in To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, Academic Press, 1980, pp. 579--607.

[12]

{DD85} J. Donahue and A. Demers, Data Types are Values, ACM Trans. on Programming Languages and Systems, 7, 3, July 1985. pp. 426--445.

Digital Library

[13]

{Gir71} J. Y. Girard, Une extension de l'interpretation de G&ouml;del &agrave; l'analyse, et son application &agrave; l'&eacute;limination des coupures dans l'analyse et la th&eacute;orie des types, in Second Scandinavian Logic Symposium, J. E. Fenstad, Ed., North-Holland, 1971, pp. 63--92.

[14]

{Hoo84} J. G. Hook, Understanding Russell--a first attempt, in Semantics of Data Types, G. Kahn, D. B. MacQueen, and G. Plotkin, Eds., LNCS Vol 173, Springer-Verlag, 1984, pp. 69--85.

Digital Library

[15]

{How80} W. Howard, The formulas-as-types notion of construction, in To H. B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, Academic Press, 1980, pp. 476--490. (written 1969)

[16]

{Mac85} D. B. MacQueen, Modules for Standard ML (Revised), Polymorphism Newsletter, ll, 2, Oct 1985.

[17]

{McC79} N. J. McCracken, An investigation of a programming language with a polymorphic type structure, Ph.D. Thesis, Computer and Information Science, Syracuse Univ., June 1979.

Digital Library

[18]

{M-L71} P. Martin-L&ouml;f, A theory of types, unpublished manuscript, October 1971.

[19]

{M-L74} P. Martin-L&ouml;f, An intuitionistic theory of types: predicative part, Logic Colloquium 73, H. Rose and J. Shepherdson, Eds., North-Holland, 1974, pp. 73--118.

[20]

{M-L82} P. Martin-L&ouml;f, Constructive mathematics and computer programming, in Logic, Methodology and Philosophy of Science, VI. North-Holland, Amsterdam, 1982, pp. 153--175.

[21]

{MR86} A. R. Meyer and M. B. Reinhold, 'Type' is not a type, 13th Annual ACM POPL Symposium, St. Petersburg, January 1986.

Digital Library

[22]

{MIL78} R. Milner, A theory of type polymorphism in programming, JCSS, 17, 3, Dec 1978, pp. 348--375.

[23]

{Mit86} J. C. Mitchell, Representation independence and data abstraction, 13th Annual ACM POPL Symposium, St. Petersburg, January 1986.

Digital Library

[24]

{MP85} J. C. Mitchell and G. D. Plotkin, Abstract types have existential types, 12th ACM Symp. on Principles of Programming Languages, New Orleans, Jan. 1985, pp. 37--51.

Digital Library

[25]

{Rey74} J. C. Reynolds, Towards a theory of type structure, in Colloquium sur la Programmation, Lecture Notes in Computer Science, Vol. 19, Springer Verlag, Berlin, 1974, pp. 408--423.

Digital Library

[26]

{Sco70} D. Scott, Constructive Validity, in Symposium on Automatic Demonstration, Lecture Notes in Math., Vol 125, Springer-Verlag, 1970, pp. 237--275.

Cited By

Clement BRémy DRadanne G(2024)Fulfilling OCaml Modules with TransparencyProceedings of the ACM on Programming Languages10.1145/36498188:OOPSLA1(194-222)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649818
Ho SFromherz AProtzenko J(2023)Modularity, Code Specialization, and Zero-Cost Abstractions for Program VerificationProceedings of the ACM on Programming Languages10.1145/36078447:ICFP(385-416)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607844
Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Show More Cited By

Recommendations

QuickBASIC and QBASIC Using Modular Structure Alternate Edition with Visual Basic
Using parameterized signatures to express modular structure
POPL '96: Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Module systems are a powerful, practical tool for managing the complexity of large software systems. Previous attempts to formulate a type-theoretic foundation for modular programming have been based on existential, dependent, or manifest types. These ...
Using Types and Inheritance in Object-Oriented Languages
ECOOP '87: Proceedings of the European Conference on Object-Oriented Programming

If the object-oriented style of programming hopes to live up to its potential as an improved methodology for software programming, a clear understanding of how to use types and inheritance is essential. Our experiences with using object-oriented ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '86: Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

January 1986

326 pages

ISBN:9781450373470

DOI:10.1145/512644

Copyright © 1986 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1986

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

126
Total Citations
View Citations
597
Total Downloads

Downloads (Last 12 months)121
Downloads (Last 6 weeks)21

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Clement BRémy DRadanne G(2024)Fulfilling OCaml Modules with TransparencyProceedings of the ACM on Programming Languages10.1145/36498188:OOPSLA1(194-222)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649818
Ho SFromherz AProtzenko J(2023)Modularity, Code Specialization, and Zero-Cost Abstractions for Program VerificationProceedings of the ACM on Programming Languages10.1145/36078447:ICFP(385-416)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607844
Sterling JHarper R(2021)Logical Relations as Types: Proof-Relevant Parametricity for Program ModulesJournal of the ACM10.1145/347483468:6(1-47)Online publication date: 5-Oct-2021
https://dl.acm.org/doi/10.1145/3474834
Eisenberg RDuboc GWeirich SLee D(2021)An existential crisis resolved: type inference for first-class existential typesProceedings of the ACM on Programming Languages10.1145/34735695:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473569
Yang LShi ZWu YLi XZhou KFu HZheng Y(2020)iOrthoPredictorACM Transactions on Graphics10.1145/3414685.341777139:6(1-15)Online publication date: 27-Nov-2020
https://dl.acm.org/doi/10.1145/3414685.3417771
Smith BWu CWen HPeluse PSheikh YHodgins JShiratori T(2020)Constraining dense hand surface tracking with elasticityACM Transactions on Graphics10.1145/3414685.341776839:6(1-14)Online publication date: 27-Nov-2020
https://dl.acm.org/doi/10.1145/3414685.3417768
Karimi MKim H(2020)Energy scheduling for task execution on intermittently-powered devicesACM SIGBED Review10.1145/3412821.341282717:1(36-41)Online publication date: 27-Jul-2020
https://dl.acm.org/doi/10.1145/3412821.3412827
Stornaiuolo LCarloni FPressiani RNatale GSantambrogio MSciuto D(2020)Enabling transparent hardware acceleration on Zynq SoC for scientific computingACM SIGBED Review10.1145/3412821.341282617:1(30-35)Online publication date: 27-Jul-2020
https://dl.acm.org/doi/10.1145/3412821.3412826
MacQueen DHarper RReppy J(2020)The history of Standard MLProceedings of the ACM on Programming Languages10.1145/33863364:HOPL(1-100)Online publication date: 12-Jun-2020
https://dl.acm.org/doi/10.1145/3386336
Umuroglu YConficconi DRasnayake LPreusser TSjälander M(2019)Optimizing Bit-Serial Matrix Multiplication for Reconfigurable ComputingACM Transactions on Reconfigurable Technology and Systems10.1145/333792912:3(1-24)Online publication date: 20-Aug-2019
https://dl.acm.org/doi/10.1145/3337929
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents