Article

Free access

Deriving algorithms from type inference systems: application to strictness analysis

Authors:

Daniel Le MétayerAuthors Info & Claims

POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 202 - 212

https://doi.org/10.1145/174675.177858

Published: 01 February 1994 Publication History

Abstract

The role of non-standard type inference in static program analysis has been much studied recently. Early work emphasised the efficiency of type inference algorithms and paid little attention to the correctness of the inference system. Recently more powerful inference systems have been investigated but the connection with efficient inference algorithms has been obscured. The contribution of this paper is twofold: first we show how to transform a program logic into an algorithm and, second, we introduce the notion of lazy types and show how to derive an efficient algorithm or strictness analysis.

References

[1]

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

Digital Library

[2]

H. Barendregt, M. Coppo, M. Dezani-Ciancaglini, A filter lambda model and the completeness of type assignment, Journal of Symbolic Logic, 48(4), 1983.

[3]

P. N. Benton, Strictness logic and polymorphic invariance, in Proceedings of the 2nd lnt. Symposium on Logical Foundations of Computer Science, LNCS 620, Springer Verlag, 1992.

Digital Library

[4]

T.-R. Chuang and B. Goldberg, A syntactic approach to fixed point computation on finite domains, in Proceedings of the 1992 A CM Conference on Lisp and Functional Programming, ACM Press, 1992.

Digital Library

[5]

C. Clack and S. L. Peyton Jones, Strictness Analysis- A Practical Approach, in J. P. :louannand (ed), Functional Programming Languages and Computer Architecture, LNCS 201, Springer Verlag, 1985.

Digital Library

[6]

P. Cousot and R. Cousot, Comparing the Galois Connection and Widening/Narrowing Approaches to Abstract Interpretation, in M. Bruynooghe and M. Wirsing (eds), PLILP'92, LNCS 631, Springer Verlag, 1992.

Digital Library

[7]

M. van Eekelen, E. Goubault, C. Hankin and E. N~ker, Abstract reduction: a theory via abstract interpretation, in R. Sleep et al (eds), Term graph rewriting: theory and practice, John Wiley & Sons Ltd, 1992.

Digital Library

[8]

A. Ferguson and R. J. M. Hughes, Fast abstract interpretation using sequential algorithms, to appear in the Proceedings WSA'93, Springer Verlag, 1993.

Digital Library

[9]

C. L. Hankin and L. S. Hunt, Approximate fixed points in abstract interpretation, in B. Krieg-Brfickner (ed), Proceedings of the $th European Symposium on Programming, LNCS 582, Springer Verlag, 1992.

Digital Library

[10]

J. J. Hannah, Investigating a proof-theoretic metalanguage, PhD thesis, University of Pennsylvania, DIKU Technical Report Nr 91/1, 1991.

Digital Library

[11]

J. Hannah and D. Miller, From Operational Semantics to Abstract Machines, Mathematical Structures in Computer Science, 2(4), 1992.

[12]

F. Henglein, Efficient type inference for higher-order binding time analysis, in Proceedings of the 5th A CM Conference on Functional Programming Languages and Computer Architecture, LNCS 523, Springer Vetlag, 1991.

Digital Library

[13]

L. S. Hunt and C. L. Hankin, Fixed Points and Frontiers: A New Perspective, Journal of Functional Programming, 1(1), 1991.

[14]

T. P. 3ensen, Strictness Analysis in Logical Form, in J. Hughes (ed), Proceedings of the 5th A CM Conference on Functional Programming Languages and Computer Architecture, LNCS 523, Springer Verlag, 1991.

Digital Library

[15]

T. P. Jensen, Abstract Interpretation in Logical Form, PhD thesis, University of London, 1992. Also available as DIKU Technical Report 93/11.

[16]

N. D. Jones and A. Mycroft, Data-flow analysis of applicative programs using minimal function graphs, in Proceedings of the A CM Conference on Principles of Programming Languages, 1986.

Digital Library

[17]

S. L. Peyton Jones and C. Clack, Finding Fixed Points in Abstract Interpretation, in S. Abramsky and C. L. Hankin (eds), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.

[18]

T.-M. Kuo and P. Mishra, Strictness analysis: a new perspective based on type inference, in Proceedings of the 4th A CM Conference on Functional Programming Languages and Computer Architecture, ACM Press, 1989.

Digital Library

[19]

J. Launchbury, Strictness and binding time: two .for the price of one, in Proceedings of the A CM Conference on Programming Languages Design and Implementation, 1991.

Digital Library

[20]

A. Leung and P. Mishra, Reasoning about simple and exhaustive demand in higher-order lazy languages, in Proceedings of the 5th A CM Conference on Functional Programming Languages and Computer Architecture, LNCS 523, Springer Verlag, 1991.

Digital Library

[21]

3. C. Mitchell, Type inference with simple subtypes, 3ournal of Functional Programming, 1(3), 1991.

[22]

B. Monsuez, Polymorphic Typing by Abstract Interpretation, in Proceedings of 12th Conference FST TCS, Springer Verlag, 1992.

Digital Library

[23]

A. Mycroft, Abstract Interpretation and Optimising Transformations for Applicative Programs, PhD thesis, University of Edinburgh, December 1981.

[24]

E. NScker, Strictness analysis using abstract reduction, in Proceedings of the 6th A CM Conference on Functional Programming Languages and Computer Archi. tecture, ACM Press, 1993.

Digital Library

[25]

P. Wadler, Strictness Analysis on Non-flat Domains, in S. Abramsky and C. L. Hankin (eds), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987.

[26]

P. Wadler, ls there a use .for linear logic?, in Proceedings of the A CM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, ACM Press, 1991.

Digital Library

Cited By

Barendsen ESmetsers S(2018)Uniqueness typing for functional languages with graph rewriting semanticsMathematical Structures in Computer Science10.1017/S09601295000701096:6(579-612)Online publication date: 19-Apr-2018
https://doi.org/10.1017/S0960129500070109
Dougherty J(2017)MATH COUNTSLet's talk about setsACM Inroads10.1145/31485348:4(33-34)Online publication date: 27-Oct-2017
https://dl.acm.org/doi/10.1145/3148534
Camp TAdrion WBizot BDavidson SHall MHambrusch SWalker EZweben S(2017)Generation CSACM Inroads10.1145/31417738:4(59-65)Online publication date: 27-Oct-2017
https://dl.acm.org/doi/10.1145/3141773
Show More Cited By

Index Terms

Deriving algorithms from type inference systems: application to strictness analysis
1. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Deriving a complete type inference for Hindley-Milner and vector sizes using expansion

Type inference and program analysis both infer static properties about a program. Yet, they are constructed using very different techniques. We reconcile both approaches by deriving a type inference from a denotational semantics using abstract ...
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 ...
Deriving a complete type inference for hindley-milner and vector sizes using expansion
PEPM '13: Proceedings of the ACM SIGPLAN 2013 workshop on Partial evaluation and program manipulation

Type inference and program analysis both infer static properties about a program. Yet, they are constructed using very different techniques. We reconcile both approaches by deriving a type inference from a denotational semantics using abstract ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '94: Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages

February 1994

492 pages

ISBN:0897916360

DOI:10.1145/174675

Chairmen:
Hans-J. Boehm
Xerox PARC
,
Bernard Lang
INRIA Rocquencourt
,
Daniel Yellin
IBM Watson Research Center

Copyright © 1994 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: 01 February 1994

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL94

Sponsor:

POPL94: 21st ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages

January 16 - 19, 1994

Oregon, Portland, USA

Acceptance Rates

POPL '94 Paper Acceptance Rate 39 of 173 submissions, 23%;

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

43
Total Citations
View Citations
318
Total Downloads

Downloads (Last 12 months)45
Downloads (Last 6 weeks)12

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Barendsen ESmetsers S(2018)Uniqueness typing for functional languages with graph rewriting semanticsMathematical Structures in Computer Science10.1017/S09601295000701096:6(579-612)Online publication date: 19-Apr-2018
https://doi.org/10.1017/S0960129500070109
Dougherty J(2017)MATH COUNTSLet's talk about setsACM Inroads10.1145/31485348:4(33-34)Online publication date: 27-Oct-2017
https://dl.acm.org/doi/10.1145/3148534
Camp TAdrion WBizot BDavidson SHall MHambrusch SWalker EZweben S(2017)Generation CSACM Inroads10.1145/31417738:4(59-65)Online publication date: 27-Oct-2017
https://dl.acm.org/doi/10.1145/3141773
Omar CAldrich J(2016)Programmable semantic fragments: the design and implementation of typyACM SIGPLAN Notices10.1145/3093335.299324552:3(81-92)Online publication date: 20-Oct-2016
https://dl.acm.org/doi/10.1145/3093335.2993245
Philips LDe Koster JDe Meuter WDe Roover C(2016)Dependence-driven delimited CPS transformation for JavaScriptACM SIGPLAN Notices10.1145/3093335.299324352:3(59-69)Online publication date: 20-Oct-2016
https://dl.acm.org/doi/10.1145/3093335.2993243
Zacharopoulos TInostroza PStorm T(2016)Extensible modeling with managed data in JavaACM SIGPLAN Notices10.1145/3093335.299324052:3(25-35)Online publication date: 20-Oct-2016
https://dl.acm.org/doi/10.1145/3093335.2993240
Smetsers SEekelen M(2012)Higher-Order Strictness TypingProceedings of the 2012 Conference on Trends in Functional Programming - Volume 782910.1007/978-3-642-40447-4_6(85-100)Online publication date: 12-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-40447-4_6
Sergey IClarke DBrabrand CWyk E(2011)From type checking by recursive descent to type checking with an abstract machineProceedings of the Eleventh Workshop on Language Descriptions, Tools and Applications10.1145/1988783.1988785(1-7)Online publication date: 26-Mar-2011
https://dl.acm.org/doi/10.1145/1988783.1988785
Agarwal PXie JYang JYu H(2009)Input-sensitive scalable continuous join query processingACM Transactions on Database Systems10.1145/1567274.156727534:3(1-41)Online publication date: 3-Sep-2009
https://dl.acm.org/doi/10.1145/1567274.1567275
Damiani FProst F(2006)Detecting and removing dead-code using rank 2 intersectionTypes for Proofs and Programs10.1007/BFb0097787(66-87)Online publication date: 26-Oct-2006
https://doi.org/10.1007/BFb0097787
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

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