Proving properties of programs defined over recursive data structures

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Proving properties of programs defined over recursive data structures

Full text

Pdf (796 KB)

Source

ACM/SIGPLAN Workshop Partial Evaluation and Semantics-Based Program Manipulation archive
Proceedings of the 1995 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation table of contents

La Jolla, California, United States

Pages: 88 - 99

Year of Publication: 1995

ISBN:0-89791-720-0

Author

Daniel Le Métayer

Irisa/Inria, Campus de Beaulieu, 35042 Rennes, France

Sponsor

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 2, Downloads (12 Months): 4, Citation Count: 2

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/215465.215567 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	Robert S. Boyer , J. Strother Moore, A computational logic handbook, Academic Press Professional, Inc., San Diego, CA, 1988
	2	Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
	3	T. Coquand, B. NordstrSm, J. M. Smith and B. von Sydow, Type theory and programming, Programming Methodology Group, University of GSteborg and Chalmers University of Technology, Research Report 81, 1994.
	4	P. Cousot and R. Cousot, Static determination of dynamic properties of recursive procedures, in E. J. Neuhold (ed.), Formal Description of Programming Concepts, North-Holland, 1977, pp. 237-277.
	5	John V. Guttag , James J. Horning, Larch: languages and tools for formal specification, Springer-Verlag New York, Inc., New York, NY, 1993
	6	M. Gordon, R. Milner and C. Wadsworth, Edinburgh LCF, LNCS 78, Springer Verlag, 1979.
	7	Chris Hankin , Daniel Le Métayer, Deriving algorithms from type inference systems: application to strictness analysis, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.202-212, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.177858]
	8	Chris Hankin , Daniel Le Métayer, Lazy Type Inference for the Strictness Analysis of Lists, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.257-271, April 11-13, 1994
	9	Thomas P. Jensen, Strictness analysis in logical form, Proceedings of the 5th ACM conference on Functional programming languages and computer architecture, p.352-366, June 1991, Cambridge, Massachusetts, United States
	10	T. P. Jensen, Abstract interpretation over algebraic data types, in Proceedings of the 199~ int. Conference on Computer Languages, IEEE, 1994, 265-276.
	11	Julia L. Lawall, Proofs by structural induction using partial evaluation, Proceedings of the 1993 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.155-166, June 14-16, 1993, Copenhagen, Denmark [doi>10.1145/154630.154646]
	12	R. Milner, A theory of type polymorphism in programming, Journal of Comp. Syst. Sci., 17, 1978, pp. 348- 375.
	13	Philip Wadler , R. J. M. Hughes, Projections for strictness analysis, Proc. of a conference on Functional programming languages and computer architecture, p.385-407, October 1987, Portland, Oregon, United States
	14	P. Wadler, Strictness analysis on non-fiat domains, in S. Abr~tmsky and C. L. Hankin (eds), Abstract Interpretation of Declarative Languages, Ellis Horwood, 1987, pp. 266-275.

CITED BY 2

	Wei-Ngan Chin , Siau-Cheng Khoo , Dana N. Xu, Extending sized type with collection analysis, ACM SIGPLAN Notices, v.38 n.10, p.75-84, October 2003
	Thomas Jensen, Disjunctive program analysis for algebraic data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.5, p.751-803, Sept. 1997