Dependent types in practical programming

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	Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
	2	R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
	3	Danvy, O. (1998, May). Functional unparsing. Technical Report RS-98-12, University of Aarhus.
	4	Dowek, G., A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner (1993). The Coq proof assistant user's guide. Rapport Techniques 154, IN- RIA, Rocquencourt, France. Version 5.8.
	5	Tim Freeman , Frank Pfenning, Refinement types for ML, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.268-277, June 24-28, 1991, Toronto, Ontario, Canada
	6	Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
	7	Susumu Hayashi , Hiroshi Nakano, PX: a computational logic, MIT Press, Cambridge, MA, 1989
	8	Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
	9	John Hughes , Lars Pareto , Amr Sabry, Proving the correctness of reactive systems using sized types, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.410-423, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.240882]
	10	Jay, C. and M. Sekanina (1996). Shape checking of array programs. Technical Report 96.09, University of Technology, Sydney, Australia.
	11	Christoph Kreitz , Mark Hayden , Jason Hickey, A Proof Environment for the Development of Group Communication Systems, Proceedings of the 15th International Conference on Automated Deduction: Automated Deduction, p.317-332, July 05-10, 1998
	12	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	13	E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
	14	George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
	15	George C. Necula , Peter Lee, The design and implementation of a certifying compiler, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.333-344, June 17-19, 1998, Montreal, Quebec, Canada
	16	Sam Owre , S. Rajan , John M. Rushby , Natarajan Shankar , Mandayam K. Srivas, PVS: Combining Specification, Proof Checking, and Model Checking, Proceedings of the 8th International Conference on Computer Aided Verification, p.411-414, August 03, 1996
	17	Catherine Parent, Synthesizing Proofs from Programs in the Calculus of Inductive Constructions, Mathematics of Program Construction, p.351-379, July 17-21, 1995
	18	Benjamin C. Pierce , David N. Turner, Local type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.252-265, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268967]
	19	Amr Sabry , Matthias Felleisen, Reasoning about programs in continuation-passing style, Lisp and Symbolic Computation, v.6 n.3-4, p.289-360, Nov. 1993 [doi>10.1007/BF01019462]
	20	Sannella, D. and A. Tarlecki (1989, February). Toward formal development of ML programs: Foundations and methodology. Technical Report ECS-LFCS-89-71, Laboratory for Foundations of Computer Science, Depatment of Computer Science, University of Edinburgh.
	21	Sulzmann, M., M. Odersky, and M. Wehr (1997). Type inference with constrained types. In Proceedings of 4th International Workshop on Foundations o~ Object-Oriented Languages.
	22	Weis, P. and X. Leroy (1993). Le langage Carol. Paris: InterEditions.
	23	Xi, H. (1997, November). Some examples of DML programming. Available at ht tp : //www. cs. cmu. edu/'hwxi/DbIL/oxamplos 1.
	24	H. (1998). Dependent Types in Practical Programming. Ph. D. thesis, Carnegie Mellon University. pp. viii+189. Forthcoming. The current version is available as http : //www. ~ s. cmu. edu/" hwxi/DML/thes is. ps.
	25	Hongwei Xi, Dead Code Elimination through Dependent Types, Proceedings of the First International Workshop on Practical Aspects of Declarative Languages, p.228-242, January 18-19, 1999
	26	Hongwei Xi , Frank Pfenning, Eliminating array bound checking through dependent types, Proceedings of the ACM SIGPLAN 1998 conference on Programming language design and implementation, p.249-257, June 17-19, 1998, Montreal, Quebec, Canada
	27	Christoph Zenger, Indexed types, Theoretical Computer Science, v.187 n.1-2, p.147-165, Nov. 15, 1997 [doi>10.1016/S0304-3975(97)00062-5 ]
	28	Zenger, C. (1998). Indizierte Typen. Ph. D. thesis, Fakultgt fiir Informatik, Universitgt Karlsruhe. Forthcoming.

Peer to Peer - Readers of this Article have also read:

Constructing reality Proceedings of the 11th annual international conference on Systems documentation
Douglas A. Powell , Norman R. Ball , Mansel W. Griffiths
Data structures for quadtree approximation and compression Communications of the ACM 28, 9
Hanan Samet
A hierarchical single-key-lock access control using the Chinese remainder theorem Proceedings of the 1992 ACM/SIGAPP Symposium on Applied computing
Kim S. Lee , Huizhu Lu , D. D. Fisher
An intelligent component database for behavioral synthesis Proceedings of the 27th ACM/IEEE conference on Design automation
Gwo-Dong Chen , Daniel D. Gajski
The GemStone object database management system Communications of the ACM 34, 10
Paul Butterworth , Allen Otis , Jacob Stein