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

Article

Free access

Inference of polymorphic and conditional strictness properties

Author:

Thomas P. JensenAuthors Info & Claims

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

Pages 209 - 221

https://doi.org/10.1145/268946.268964

Published: 21 January 1998 Publication History

Abstract

We define an inference system for modular strictness analysis of functional programs by extending a conjunctive strictness logic with polymorphic and conditional properties. This extended set of properties is used to define a syntax-directed, polymorphic strictness analysis based on polymorphic recursion whose soundness is established via a translation from the polymorphic system into the conjunctive system. From the polymorphic analysis, an inference algorithm based on constraint resolution is derived and shown complete for variant of the polymorphic analysis. The algorithm deduces at the same time a property and a set of hypotheses on the free variables of an expression which makes it suitable for analysis of program with module structure.

References

[1]

A. Aiken and E. Wimmers. Type inclusion constraints and type inference. In Proe. of Functional Programming Languages and Computer Architecture (FPCA '93), pages 31-41. ACM Press, 1993.

Digital Library

[2]

A. Aiken, E. L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Proc. of the 21st Annual A CM Symposium on Principles of Programming Languages, pages 163-173. ACM Press, 1994.

Digital Library

[3]

A. Banerjee. A modular, polyvariant and type-based closure analysis. In Proc. A CM Int. Conf. on Functional Programming (ICFP'97), pages 1-10. ACM Press, 1997.

Digital Library

[4]

P. N. Benton. Strictness logic and polymorphie invariance. In A. Nerode and M. Taitslin, editors, Proc. of the 2. International Symposium on Logical Foundations of Computer Science, Tver, Russia, LNCS vol. 620. Springer, 1992.

Digital Library

[5]

G. L. Burn, C. Hankin, and S. Abramsky. The theory and practice of s~rlctness analysis for higher order functions. Science of Computer Programming, 7:249- 278, 1986.

Digital Library

[6]

M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal type schemes and lambda calculus semantics. In J.P. Seldin and J.R. tIindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Caleulas and Formalism, pages 535-560. Academic Press, 1980.

[7]

M. Coppo and P. Giamfini. A complete type inference algorithm for simple intersection types. In Jean-Claude Raoult, editor, Proc. of CAAP "92, 17th Colloquium on Trees in Algebra and Pro#ramming, LNCS vol. 581, pages 102-123. Springer-Verlag, 1992.

Digital Library

[8]

L. Damas. Type assignment in programming languages. PhD thesis, Univ. of Edinburgh, 1985.

[9]

L. Damns and R. Milner. Principal type schemes for functional programs, l, Proc. of 9th ACId Symposium on Principles ojf Programming Languages, pages 207- 212. ACM Press, New York, 1982.

Digital Library

[10]

D. Dussart, F. Henglein, and {2. Mossin. Polymorphie recursion and subtype qualifications: Poiymorphic binding-time analysis in polynomial time. In Proe. 2nd Int. Static Analysis Symposium (SAS), Glasgow, Scotland, LNCS vol. 983. Springer, 1995.

Digital Library

[11]

C. Hankin and D. Le Mdtayer. Deriving algorithms from type inference systems: Applications to strictness analysis, in Proc. of 21s~ A GM Syrup. on Principles of Programming Languages, pages 202-212. ACM Press, 1994.

Digital Library

[12]

C. Haakia and D. Le Mdtayer. Lazy type inference and program analysis. Science o} Computer Programming, 25:219-249, 1995.

Digital Library

[13]

J. Hannah and D. Miller. From operational semantics to abstrac~ machines. Mathematical Structures in Computer Science, 2(4), 1992.

[14]

F. Hengleia and C. Mossin. Pofymorphic binding-time analysis, in D. Sannellu, editor, Proc. of 5~h European Symposium or~ Programming, LNCS vol. 788, pages 287-301. Springer Verlag, 1994.

Digital Library

[15]

T. Jensen. Strictzless analysis in logical form. In J. Hughes, editor, Proc. of 5th A GM Conference on Fundional Programming Languages and Computer Architecture, LNCS vol. 523, pages 352-366. Springer, 1991.

Digital Library

[16]

T. Jensen. Abstract interpretation over algebraic data types. In H. Bal, editor, Proc. 5th IBEE International Conference on Computer Languages. IEEE Press, 1994.

[17]

T. Jensen. Clock analysis of synchronous data~ow programs. In W. Scherlis, editor, Proc. of A CM Symposium on Par$ial Evaluation and Semantics-Based Program Manipulation, pages 156-167, San Diego, 1995. ACM Press.

Digital Library

[18]

T. Jensen. Conjunctive type systems and abstrac~ interpretation of higher-order functional programs. Journal of Logic and Computation, 5(4):397-421, 1995.

[19]

T. Jensen. Disjunc~ive program analysis for Mgebraic data types. A GM Transactions on Programming Lan. 9uages and Systems, 19(5):752-804, 1997.

Digital Library

[20]

T. Jim. What are principal typings and what are they good for? In Proc. of 23rd Symposium on Principles of Programming Languages, pages 42-54. ACM Press, 1996.

Digital Library

[21]

T-M Kuo and P. Mishra. Strictness analysis : A new perspective based on type inference. In Proc. 4th. Int. Conf. on Functional Programming and Computer At. chitecture. ACM Press, 1989.

Digital Library

[22]

P. Le Guernic, T. Gauthier, M. Le Borgne, and C. Le Maire. Programming real-time applications with SIG- NAL. Proceedings of the IEEE, 79(9):1321-i336, 1991,

[23]

D. Leivant. Polymorphic type inference. In Proc. of the Tenth Annual A GM Symposium on Principles of Pro. tramming Languages, pages 88-98. ACM Press, 1983,

Digital Library

[24]

K. Milner. A theory o1~ type polymorphism in prostemming. Journal of Computer and System Sciences, 17:348-375, 1978.

[25]

B. Monsuez. Using abstract interpretation to define a strictness type inference system. In W. Schedi% editor, Proe. of A CM Symposium on Partial Evaluation and Semantics-based program manipulation (PEPM'95), pages 122-133. ACM Press, 1995.

Digital Library

[26]

A. Mycroft. Polymorphie type schemes and reeursive definitions. In Proc. of Int. Bymposium on Program. ruing, Toulouse, France., pages 217-239. Springer LNCS vol. 167, 1984.

Digital Library

[27]

J. Rehof and T. Mogensen. Tractable constraints in finite semitattices. In K. Cousot and D. Schmidt, editors, Proc. of 3rd Int. Static Analysis Symposium (8A8'96)~ pages 285-300. Springer LNCS vol. 1145, 1996.

Digital Library

[28]

J. C. Reynolds. Automatic computation of data set definitions, lnJormation Processing, 68~ 1969.

[29]

S. Ronchi Della Rocca. Principal type scheme and unification for intersection type discipline. Theoretical Computer Science, 59, 1988.

Digital Library

[30]

S. v. Bakel. Complete restrictions of the intersection type discipline. Theoretical Computer Science~ 102(1):135-163, 1992.

Digital Library

Cited By

Schrijvers TMycroft A(2010)Strictness meets data flowProceedings of the 17th international conference on Static analysis10.5555/1882094.1882121(439-454)Online publication date: 14-Sep-2010
https://dl.acm.org/doi/10.5555/1882094.1882121
Holdermans SHage JBrabrand CMoreau P(2010)On the rôle of minimal typing derivations in type-driven program transformationProceedings of the Tenth Workshop on Language Descriptions, Tools and Applications10.1145/1868281.1868283(1-8)Online publication date: 28-Mar-2010
https://dl.acm.org/doi/10.1145/1868281.1868283
Holdermans SHage JGallagher JVoigtländer J(2010)Making "stricterness" more relevantProceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and program manipulation10.1145/1706356.1706379(121-130)Online publication date: 19-Jan-2010
https://dl.acm.org/doi/10.1145/1706356.1706379
Show More Cited By

Index Terms

Inference of polymorphic and conditional strictness properties
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Polymorphism
  2. Software organization and properties
    1. Software functional properties
      1. Correctness
2. Theory of computation
  1. Logic
    1. Proof theory
  2. Semantics and reasoning
    1. Program reasoning
      1. Program analysis
    2. Program semantics

Recommendations

Polymorphic type inference
POPL '83: Proceedings of the 10th ACM SIGACT-SIGPLAN symposium on Principles of programming languages

The benefits of strong typing to disciplined programming, to compile-time error detection and to program verification are well known. Strong typing is especially natural for functional (applicative) languages, in which function application is the central ...
Polymorphic type inference for languages with overloading and subtyping
Type checking and inference for polymorphic and existential types
CATS '09: Proceedings of the Fifteenth Australasian Symposium on Computing: The Australasian Theory - Volume 94

This paper proves undecidability of type checking and type inference problems in some variants of typed lambda calculi with polymorphic and existential types. First, type inference in the domain-free polymorphic lambda calculus is proved to be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

January 1998

403 pages

ISBN:0897919793

DOI:10.1145/268946

Chairmen:
David B. MacQueen
Bell Labs
,
Luca Cardelli
Digital Equipment Corp.

Copyright © 1998 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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 January 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL98

Sponsor:

POPL98: Symposium on Principles of Programming Languages

January 19 - 21, 1998

California, San Diego, USA

Acceptance Rates

POPL '98 Paper Acceptance Rate 32 of 175 submissions, 18%;

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

20
Total Citations
View Citations
102
Total Downloads

Downloads (Last 12 months)47
Downloads (Last 6 weeks)5

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Schrijvers TMycroft A(2010)Strictness meets data flowProceedings of the 17th international conference on Static analysis10.5555/1882094.1882121(439-454)Online publication date: 14-Sep-2010
https://dl.acm.org/doi/10.5555/1882094.1882121
Holdermans SHage JBrabrand CMoreau P(2010)On the rôle of minimal typing derivations in type-driven program transformationProceedings of the Tenth Workshop on Language Descriptions, Tools and Applications10.1145/1868281.1868283(1-8)Online publication date: 28-Mar-2010
https://dl.acm.org/doi/10.1145/1868281.1868283
Holdermans SHage JGallagher JVoigtländer J(2010)Making "stricterness" more relevantProceedings of the 2010 ACM SIGPLAN workshop on Partial evaluation and program manipulation10.1145/1706356.1706379(121-130)Online publication date: 19-Jan-2010
https://dl.acm.org/doi/10.1145/1706356.1706379
Holdermans SHage J(2010)Making "stricterness" more relevantHigher-Order and Symbolic Computation10.1007/s10990-011-9079-723:3(315-335)Online publication date: 1-Sep-2010
https://dl.acm.org/doi/10.1007/s10990-011-9079-7
Schrijvers TMycroft A(2010)Strictness Meets Data FlowStatic Analysis10.1007/978-3-642-15769-1_27(439-454)Online publication date: 2010
https://doi.org/10.1007/978-3-642-15769-1_27
Yokouchi H(2008)Strictness analysis algorithms based on an inequality system for lazy typesProceedings of the 9th international conference on Functional and logic programming10.5555/1788446.1788473(255-271)Online publication date: 14-Apr-2008
https://dl.acm.org/doi/10.5555/1788446.1788473
Yokouchi H(2008)Strictness Analysis Algorithms Based on an Inequality System for Lazy TypesFunctional and Logic Programming10.1007/978-3-540-78969-7_19(255-271)Online publication date: 2008
https://doi.org/10.1007/978-3-540-78969-7_19
Schmidt-Schauss MSabel DSchütz M(2007)Deciding inclusion of set constants over infinite non-strict data structuresRAIRO - Theoretical Informatics and Applications10.1051/ita:200701041:2(225-241)Online publication date: 18-Jul-2007
https://doi.org/10.1051/ita:2007010
Carlier SWells J(2005)ExpansionElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2005.03.026136(173-202)Online publication date: 1-Jul-2005
https://dl.acm.org/doi/10.1016/j.entcs.2005.03.026
Neergaard PMairson HOkasaki CFisher K(2004)Types, potency, and idempotencyProceedings of the ninth ACM SIGPLAN international conference on Functional programming10.1145/1016850.1016871(138-149)Online publication date: 19-Sep-2004
https://dl.acm.org/doi/10.1145/1016850.1016871
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