Skip to main content
SpringerLink
Log in

A Formalization of Static Analyses in System F

  • Conference paper
  • First Online:
Automated Deduction — CADE-16 (CADE 1999)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 1632))

Included in the following conference series:

Abstract

In this paper, we propose a common theoretical framework for type based static analyses. The aim is the study of relationships between typing and program analysis.

We present a variant of Girard’s System F called F stackП stack≤:. We prove standard properties of F stackП stack≤:. We show how it can be used to formalize various program analyses like binding time and dead code. We relate our work to previous analyses in terms of expressivness (often only simply typed calculi are considered) and power (more information can be inferred). F stackП: features polymorphism as well as subtyping at the level of universe extending previous author work where only universe polymorphism (on a simply typed calculus) was considered

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Berardi and L. Boerio. Using subtyping in program optimization. In Proceedings of TLCA’95, LNCS 902. Spinger-Verlag, 1995.

    Google Scholar 

  2. B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliatre, H. Herbelin, G. Huet, P. Manoury, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. Saïbi, and B. Werner. The Coq Proof Assistant ReferenceManual Version 6.1. INRIA-Rocquencourt-CNRS-ENS Lyon, December 1996.

    Google Scholar 

  3. S. Berardi. Pruning simply typed lambda terms. Journal of Logic and Computation, 125(2):663–681, 15 March 1996.

    Article  Google Scholar 

  4. L. Boerio. Extending pruning techniques to polymorphic second order λ-calculus. In D. Sanella, editor, Proceedings of ESOP’94, LNCS 788, pages 120–134. Springer-Verlag, April 1994.

    Google Scholar 

  5. P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL’ 77 ), pages 238–252, New York, 1977. ACM Press.

    Google Scholar 

  6. D. Clément, J. Despeyroux, T. Desperoux, and G. Kahn. A simple applicative language: Mini-ML. Technical Report 529, INRIA-Sophia Antipolis, May 1986.

    Google Scholar 

  7. D. Dussart, F. Henglein, and C. Mossin. Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time. In Alan Mycroft, editor, SAS’95: 2nd Int’l Static Analysis Symposium, volume 983 of Lecture Notes in Computer Science, pages 118–135, Glasgow, Scotland, September 1995. Springer-Verlag.

    Google Scholar 

  8. F. Damiani and F. Prost. Detecting and removing dead code using rank-2 intersection. In International Workshop:“TYPES’96”, selected papers, LNCS1512. Spinger-Verlag, 1998.

    Google Scholar 

  9. J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

    Google Scholar 

  10. N. Heintze. Control-flow analysis and type systems. In Alan Mycroft, editor, Proceeding of SAS 1995, LNCS 983, pages 189–206. Springer-Verlag, 1995.

    Google Scholar 

  11. C. Hankin and D. Le Métayer. A type-based framework for program analysis. In Proceedings of the Static Analysis Symposium, LNCS 864, pages 380–394. Springer-Verlag, 1994.

    Google Scholar 

  12. S. Hunt. Abstract Interpretation of functionnal languages: from theory to Practice. PhD thesis, Department of Computing, Imperial College, London, 1991.

    Google Scholar 

  13. Z. Luo and R. Pollack. Lego proof development system: User’s manual. Technical Report ECS-LFCS-92-211, University of Edinburgh., 1992.

    Google Scholar 

  14. J.C. Mitchell. A type inference approach to reduction properties and semantics of polymorphic expressions. In G. Huet, editor, Logical Foundations of Functionnal programming, pages 195–211. Addison-Wesley, 1990. (Chapter 9).

    Google Scholar 

  15. H.R. Nielson, K.L. Solberg, and F. Nielson. Strictness and totality analysis. In Static Analysis, LNCS 864, pages 408–422. Springer-Verlag, 1994.

    Google Scholar 

  16. C. Paulin. Extraction de programmes dans le calcul des constructions. PhD thesis, Université Paris 7, January 1989.

    Google Scholar 

  17. C. Paulin-Mohring. Extracting Fω’s programs from proofs in the Calculus of Constructions. In Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, January 1989. ACM.

    Google Scholar 

  18. F. Prost. Using ML type inference for dead code analysis. Research Report RR 97-09, LIP, ENS Lyon, France, May 1997.

    Google Scholar 

  19. K. Lackner Solberg. Annotated Type Systems for Program Analysis. PhD thesis, Odense University, July 1995.

    Google Scholar 

  20. J.-P. Talpin and P. Jouvelot. The type and effect discipline. In IEEE Computer Society Press, editor, Proceedings of the 1992 Conference on Logic in Computer Science, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIP, Ecole Normale Supérieure de Lyon46 Allée d’Italie, 69364, Lyon Cedex 07, France

    Frédéric Prost

Authors
  1. Frédéric Prost
    View author publications

    You can also search for this author in PubMed Google Scholar

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Prost, F. (1999). A Formalization of Static Analyses in System F . In: Automated Deduction — CADE-16. CADE 1999. Lecture Notes in Computer Science(), vol 1632. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48660-7_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-48660-7_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66222-8

  • Online ISBN: 978-3-540-48660-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation