Types as abstract interpretations

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Types as abstract interpretations

Full text

Pdf (1.24 MB)

Source

Annual Symposium on Principles of Programming Languages archive
Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages table of contents

Paris, France

Pages: 316 - 331

Year of Publication: 1997

ISBN:0-89791-853-3

Author

Patrick Cousot

LIENS, École Normale Supérieure, 45, rue d'Ulm, 75230 Paris cedex 05 (France)

Sponsors

L'Ecole des Mines de Paris : L'Ecole des Mines de Paris
SIGACT: ACM Special Interest Group on Algorithms and Computation Theory
Ctr Natl de la Recherche Sci :
SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 42, Citation Count: 22

Additional Information:

references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/263699.263744 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	H. P. Barendregt, Lambda calculi with types, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
	2	Luca Cardelli, Type systems, ACM Computing Surveys (CSUR), v.28 n.1, p.263-264, March 1996 [doi>10.1145/234313.234418]
	3	Mario Coppo, A Completeness Theorem for Recursively Defined Types, Proceedings of the 12th Colloquium on Automata, Languages and Programming, p.120-129, July 15-19, 1985
	4	Mario Coppo , Ferruccio Damiani , Paola Giannini, Refinement Types for Program Analysis, Proceedings of the Third International Symposium on Static Analysis, p.143-158, September 24-26, 1996
	5	M. Coppo & M. Dezani-Ciancaglini. An extension of the basic functionality theory for the h-calculus. Notre Dame J. Formal Logic, 21(4):685-693, 1980.
	6	P. Cousot. Semantic foundations of program analysis. Ch. 10 of Program Flow Analysis: Theory and Applications, pp. 303-342. Prentice-Hall, 1981.
	7	Patrick Cousot , Radhia Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.238-252, January 17-19, 1977, Los Angeles, California [doi>10.1145/512950.512973]
	8	#. Constructive versions of Tarski's fixed point theorems. Pacific J. Math., 82(1):43-57, 1979.
	9	Patrick Cousot , Radhia Cousot, Systematic design of program analysis frameworks, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.269-282, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567778]
	10	Patrick Cousot , Rahida Cousot, Abstract interpretation and application to logic programs, Journal of Logic Programming, v.13 n.2-3, p.103-179, July 1992 [doi>10.1016/0743-1066(92)90030-7]
	11	-#---. Abstract interpretation frameworks. J. Logic and Comp., 2(4):511-547, 1992.
	12	Patrick Cousot , Radhia Cousot, Inductive definitions, semantics and abstract interpretations, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.83-94, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143184]
	13	#---. Higher-order abstract interpretation (and application to comportment analysis generalizing strictness, termination, projection and PER. analysis of functional languages). ICCL'94f:95-112. IEEE Comp. Soc. Press, 1994.
	14	Patrick Cousot , Radhia Cousot, Formal language, grammar and set-constraint-based program analysis by abstract interpretation, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.170-181, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224199]
	15	Patrick Cousot , Radhia Cousot, Compositional and Inductive Semantic Definitions in Fixpoint, Equational, Constraint, Closure-condition, Rule-based and Game-Theoretic Form, Proceedings of the 7th International Conference on Computer Aided Verification, p.293-308, July 03-05, 1995
	16	Patrick Cousot , Nicolas Halbwachs, Automatic discovery of linear restraints among variables of a program, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.84-96, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512770]
	17	Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
	18	Saumya K. Debray, Formal bases for dataflow analysis of logic programs, Advances in logic programming theory, Oxford University Press, Inc., New York, NY, 1995
	19	Carl A. Gunter, The semantics of types in programming languages, Handbook of logic in computer science (vol. 3): semantic structures, Oxford University Press, Oxford, 1995
	20	C. A. Gunter , D. S. Scott, Semantic domains, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	21	R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. Amer. Math. Soc., 146:29- 80, 1969.
	22	T. Jensen. Disjunctive strictness analysis. 7th LICS:174-185. IEEE Comp. Soc. Press, 1992.
	23	Trevor Jim, What are principal typings and what are they good for?, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.42-53, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237728]
	24	Neil D. Jones , Flemming Nielson, Abstract interpretation: a semantics-based tool for program analysis, Handbook of logic in computer science (vol. 4): semantic modelling, Oxford University Press, Oxford, 1995
	25	Pierre Jouvelot , David Gifford, Algebraic reconstruction of types and effects, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.303-310, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99623]
	26	Tsung-Min Kuo , Prateek Mishra, Strictness analysis: a new perspective based on type inference, Proceedings of the fourth international conference on Functional programming languages and computer architecture, p.260-272, September 11-13, 1989, Imperial College, London, United Kingdom [doi>10.1145/99370.99390]
	27	J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
	28	David MacQueen , Gordon Plotkin , Ravi Sethi, An ideal model for recursive polymorphic types, Information and Control, v.71 n.1-2, p.95-130, Oct/Nov. 1986 [doi>10.1016/S0019-9958(86)80019-5]
	29	R. Milner. A theory of polymorphism in programming. J. Comput. Sys. Sci., 17(3):348-375, 1978.
	30	Robin Milner , Mads Tofte, Co-induction in relational semantics, Theoretical Computer Science, v.87 n.1, p.209-220, Sept. 16, 1991 [doi>10.1016/0304-3975(91)90033-X]
	31	John C. Mitchell, Type systems for programming languages, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
	32	Bruno Monsuez, Polymorphic Typing by Abstract Interpretation, Proceedings of the 12th Conference on Foundations of Software Technology and Theoretical Computer Science, p.217-228, December 18-20, 1992
	33	LNCS 724:267-281. Springer, 1993.
	34	Bruno Monsuez, Polymorphic Typing for Call-by-Name Semantics, Proceedings of the International Conference on Formal Methods in Programming and Their Applications, p.156-169, June 28-July 02, 1993
	35	Bruno Monsuez, System F and Abstract Interpretation, Proceedings of the Second International Symposium on Static Analysis, p.279-295, September 25-27, 1995
	36	B. Monsuez, Using abstract interpretation to define a strictness type inference system, Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.122-133, June 21-23, 1995, La Jolla, California, United States [doi>10.1145/215465.215574]
	37	Alan Mycroft, Polymorphic Type Schemes and Recursive Definitions, Proceedings of the 6th Colloquium on International Symposium on Programming, p.217-228, April 17-19, 1984
	38	Alan. Mycroft , Neil. D. Jones, A relational framework for abstract interpretation, on Programs as data objects, p.156-171, April 1986, Copenhagen, Denmark
	39	Alan Mycroft , Richard A. O'Keefe, A polymorphic type system for PROLOG., Artificial Intelligence, v.23 n.3, p.295-307, August 1984 [doi>10.1016/0004-3702(84)90017-1]
	40	Jens Palsberg , Patrick O'Keefe, A type system equivalent to flow analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.17 n.4, p.576-599, July 1995 [doi>10.1145/210184.210187]
	41	Adi Shamir , William W. Wadge, Data Types as Objects, Proceedings of the Fourth Colloquium on Automata, Languages and Programming, p.465-479, July 18-22, 1977

CITED BY 22

	Thomas Jensen, Types in program analysis, The essence of computation: complexity, analysis, transformation, Springer-Verlag New York, Inc., New York, NY, 2002
	Roberto Giacobazzi , Francesco Ranzato , Francesca Scozzari, Making abstract interpretations complete, Journal of the ACM (JACM), v.47 n.2, p.361-416, March 2000
	Patric Cousot, Directions for research in approximate system analysis, ACM Computing Surveys (CSUR), v.31 n.3es, Sept. 1999
	Jens Palsberg , Christina Pavlopoulou, From polyvariant flow information to intersection and union types, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.197-208, January 19-21, 1998, San Diego, California, United States
	Naoki Kobayashi, A type system for lock-free processes, Information and Computation, v.177 n.2, p.122-159, 15 September 2002
	Fausto Spoto , Thomas Jensen, Class analyses as abstract interpretations of trace semantics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.25 n.5, p.578-630, September 2003
	Francesca Levi , Sergio Maffeis, On abstract interpretation of mobile ambients, Information and Computation, v.188 n.2, p.179-240, 29 January 2004
	Patrick Cousot , Radhia Cousot, Temporal abstract interpretation, Proceedings of the 27th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.12-25, January 19-21, 2000, Boston, MA, USA
	Patrick Cousot , Radhia Cousot, Parsing as abstract interpretation of grammar semantics, Theoretical Computer Science, v.290 n.1, p.531-544, 1 January 2003
	Roly Perera , Jeff Foster , György Koch, A delta-driven execution model for semantic computing, Companion to the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	Manuel V. Hermenegildo , Elvira Albert , Pedro López-García , Germán Puebla, Abstraction carrying code and resource-awareness, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.1-11, July 11-13, 2005, Lisbon, Portugal
	Roly Perera , Jeff Foster, A delta-driven execution model for semantic computing, Companion to the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	Damiano Zanardini, Abstract non-interference in a fragment of Java bytecode, Proceedings of the 2006 ACM symposium on Applied computing, April 23-27, 2006, Dijon, France
	Peeter Laud , Tarmo Uustalu , Varmo Vene, Type systems equivalent to data-flow analyses for imperative languages, Theoretical Computer Science, v.364 n.3, p.292-310, 8 November 2006
	Patrick Cousot , Radhia Cousot, Bi-inductive Structural Semantics, Electronic Notes in Theoretical Computer Science (ENTCS), v.192 n.1, p.29-44, October, 2007
	Jens Palsberg , Christina Pavlopoulou, From Polyvariant flow information to intersection and union types, Journal of Functional Programming, v.11 n.3, p.263-317, May 2001
	Ferruccio Damiani, Rank 2 Intersection for Recursive Definitions, Fundamenta Informaticae, v.77 n.4, p.451-488, December 2007
	François Fages , Sylvain Soliman, Abstract interpretation and types for systems biology, Theoretical Computer Science, v.403 n.1, p.52-70, August, 2008
	Simon Perdrix, A Hierarchy of Quantum Semantics, Electronic Notes in Theoretical Computer Science (ENTCS), v.192 n.3, p.71-83, November, 2008
	Oege de Moor , Damien Sereni , Pavel Avgustinov , Mathieu Verbaere, Type inference for datalog and its application to query optimisation, Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 09-12, 2008, Vancouver, Canada
	Mayur Naik , Jens Palsberg, A type system equivalent to a model checker, ACM Transactions on Programming Languages and Systems (TOPLAS), v.30 n.5, p.1-24, August 2008
	Patrick Cousot , Radhia Cousot, Bi-inductive structural semantics, Information and Computation, v.207 n.2, p.258-283, February, 2009