[1] K. R. Apt and E.-R. Olderog. Verification of sequential and concurrent programs. Springer-Verlag, 1991. [ bib ]
[2] J. R. Abrial. The B-Book. Assigning programs to meaning. Cambridge University Press, 1996. [ bib ]
[3] R. J. R. Back. On correct refinement of programs. Journal of Computer and Systems Sciences, 23(1):49--68, August 1981. [ bib ]
[4] B. Barras. Auto-validation d'un système de preuves avec familles inductives. Thèse de doctorat, Université Paris 7, November 1999. [ bib ]
[5] J. L. Bentley. Writing Efficient Programs. Prentice Hall, 1982. [ bib ]
[6] J. L. Bentley. Programming Pearls. Addison-Wesley, 1989. [ bib ]
[7] S. Berardi. Pruning Simply Typed λ--terms. Technical report, Turin University, 1993. [ bib | .rtf.gz ]
[8] R. S. Boyer and J. S. Moore, editors. The Correctness Problem in Computer Science. Academic Press, 1981. [ bib ]
[9] P. Chartier. Formalization of B in Isabelle/HOL. In Proceedings of the Second B International Conference, volume 1393 of Lecture Notes in Computer Science, Montpellier, France, April 1998. Springer-Verlag. [ bib ]
[10] Proceedings of the Second B International Conference, volume 1393 of Lecture Notes in Computer Science, Montpellier, France, April 1998. Springer-Verlag. [ bib ]
[11] P. Cousot. Handbook of Theoretical Computer Science, volume B, chapter Methods and Logics for Proving Programs, pages 841--993. Elsevier Science Publishers B. V., 1990. [ bib ]
[12] N.J. de Bruijn. A survey of the project Automath. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980. [ bib ]
[13] E. W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976. [ bib ]
[14] R. W. Floyd. Algorithm 113: Treesort. Communications of the ACM, 5(8), August 1962. [ bib ]
[15] R. W. Floyd. Assigning meanings to programs. In J. T. Schwartz, editor, Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19, pages 19--32, Providence, 1967. American Mathematical Society. [ bib ]
[16] E. Giménez. Two Approaches to the Verification of Concurrent Programs in Coq. Personal communication, 1999. [ bib | .html ]
[17] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989. [ bib ]
[18] C. Goad. Proofs as Description of Computation. Proceedings of the 5th Conference on Automated Deduction, 87, 1980. [ bib ]
[19] Mike Gordon. Teaching and Learning Formal Methods, chapter Teaching hardware and software verification in a uniform framework. Academic Press, 1996. [ bib | .ps.gz ]
[20] D. Gries. The Science of Programming. Springer-Verlag, 1981. [ bib ]
[21] Jim Grundy. A Method of Program Refinement. PhD thesis, University of Cambridge, Computer Laboratory, New Museums Site, Pembroke Street, Cambridge CB2 3QG, England, November 1993. Technical Report 318. [ bib | .ps.gz ]
[22] J. Guzmán and A. Suárez. An Extended Type System for Exceptions. In Record of the fifth ACM SIGPLAN workshop on ML and its Applications, June 1994. Also appears as Research Report 2265, INRIA, BP 105 - 78153 Le Chesnay Cedex, France. [ bib | .ps ]
[23] Haskell 1.4, a non-strict, purely functional language. Technical report, Yale University, April 1997. [ bib ]
[24] I. Hayes. Specification Case Studies. Oxford University Computing Laboratory, 1985. Technical monograph PRG-46. [ bib ]
[25] C. A. R. Hoare. Algorithm 65: Find. Communications of the ACM, 4(7):321--322, July 1961. [ bib ]
[26] C. A. R. Hoare. Quicksort. Computer Journal, 5(1):10--15, April 1962. [ bib ]
[27] C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580,583, 1969. Also in [29] pages 45--58. [ bib ]
[28] C. A. R. Hoare. Proof of a program: Find. Communications of the ACM, 14(1):39--45, January 1971. Also in [29] pages 59--74. [ bib ]
[29] C. A. R. Hoare and C. B. Jones. Essays in Computing Science. Prentice Hall, 1989. [ bib ]
[30] F. Honsell, I. A. Mason, S. F. Smith, and C. L. Talcott. A Theory of Classes for a Functional Language with Effects. In 1992 Annual Conference of the European Association for Computer Science Logic CSL92, San Miniato, volume 702 of Lecture Notes in Computer Science, pages 309--326. Springer-Verlag, 1992. [ bib ]
[31] B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java Classes (Preliminary Report). ACM, 1998. [ bib | .ps.Z ]
[32] J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Java Series. Sun Microsystems, 1996. [ bib ]
[33] C. B. Jones. Software Development. A rigorous approach. Prentice Hall, 1980. [ bib ]
[34] C. B. Jones. Systematic Software Development Using VDM. Prentice Hall, 1989. [ bib ]
[35] C. B. Jones. VDM : une méthode rigoureuse pour le développement du logiciel. Masson, 1991. Traduction française de [34]. [ bib ]
[36] M. P. Jones and L. Duponcheel. Composing monads. Research Report YALEU/DCS/RR-1004, Yale University, December 1993. [ bib | .ps ]
[37] P. Jouvelot and D. K. Gifford. Algebraic Reconstruction of Types and Effects. In Proceedings of the 18th ACM Symposium on Principles of Programming Languages, pages 303--310. ACM, January 1991. [ bib ]
[38] B. W. Kernighan and R. Pike. The Practice of Programming. Addison-Wesley, 1999. [ bib ]
[39] B. W. Kernighan and D. M. Ritchie. The C Programming Language. Prentice Hall, second edition, 1978. [ bib ]
[40] S.C. Kleene. Introduction to Metamathematics. Bibliotheca Mathematica. North-Holland, 1952. [ bib ]
[41] T. Kleymann. Metatheory of Verification Calculi in LEGO: To What Extent Does Syntax Matter? Technical Report 98-393, LFCS, September 1998. [ bib | .ps.gz ]
[42] D. E. Knuth. The Art of Computer Programming. Volume 1: Fundamental Algorithms. Addison-Wesley, 1968. [ bib ]
[43] D. E. Knuth. The Art of Computer Programming. Volume 2: Seminumerical Algorithms. Addison-Wesley, 1969. [ bib ]
[44] D. E. Knuth. The Art of Computer Programming. Volume 3: Sorting and Searching. Addison-Wesley, 1973. [ bib ]
[45] D. E. Knuth. Selected Papers on Computer Science. CSLI Publications and Cambridge University Press, 1996. [ bib ]
[46] D. E. Knuth, J. H. Morris, and V. R. Pratt. Fast pattern matching in strings. SIAM Journal on Computing, 6:323--350, 1977. [ bib ]
[47] J. Launchbury and S. L. Peyton Jones. Lazy Functional State Threads. In SIGPLAN Symposium on Programming Language Design and Implementation (PLDI'94), pages 24--35, June 1994. [ bib | .ps.Z ]
[48] X. Leroy and F. Pessaux. Type-based analysis of uncaught exceptions. ACM Transactions on Programming Languages and Systems, 2(22), 2000. [ bib ]
[49] X. Leroy and P. Weis. Polymorphic type inference and assignment. In Proceedings of the 1991 ACM Conference on Principles of Programming Languages, pages 291--302, 1991. [ bib | .dvi.gz ]
[50] M. Lillibridge. Exceptions Are Strictly More Powerful Than Call/CC. Technical Report 178, Carnegie Mellon University, July 1995. [ bib | .ps ]
[51] I. A. Mason and C. L. Talcott. Axiomatizing Operational Equivalence in the Presence of Side Effects. In Fourth Annual Symposium on Logic in Computer Science, pages 284--293. IEEE, 1989. [ bib | .ps ]
[52] R. Milner. A theory of type polymorphism in programming. Journal of Computing System Science, 17:348--375, 1978. [ bib ]
[53] E. Moggi. An abstract view of programming languages. Technical Report ECS-LFCS-90-113, Edinburgh University, Department of Computer Science, June 1989. Lecture Notes for course CS 359, Stanford University. [ bib | .dvi.gz ]
[54] E. Moggi. Computational lambda-calculus and monads. In IEEE Symposium on Logic in Computer Science, 1989. [ bib | .dvi.gz ]
[55] E. Moggi. Notions of computations and monads. Information and Computation, 93(1), 1991. [ bib ]
[56] J.-F. Monin. Comprendre les méthodes formelles. Masson, 1996. [ bib ]
[57] E. Moggi and F. Palumbo. Monadic Encapsulation of Effects: a Revised Approach. In Third International Workshop on Higher Order Operational Techniques in Semantics, 1999. [ bib | .ps.gz ]
[58] C. C. Morgan. Programming from Specifications. Prentice Hall, 1990. [ bib ]
[59] J. H. Morris and V. R. Pratt. A Linear Pattern Matching Algorithm. Technical Report 40, Computing Center, University of California, Berkeley, 1970. [ bib ]
[60] C. Muñoz. Supporting the B-method in PVS: An Approach to the Abstract Machine Notation in Type Theory. Submitted to FSE-98, 1998. [ bib | .ps.gz ]
[61] P. W. O'Hearn and J. C. Reynolds. From Algol to Polymorphic Linear Lambda-calculus. Journal of the ACM, April 1997. To appear. [ bib | .ps ]
[62] C. Paulin-Mohring. Réalisabilité et extraction de programmes. In Logique et informatique : une introduction, pages 163--180. INRIA, 1991. [ bib ]
[63] W. Reif. The KIV-approach to software verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software -- Final Report, volume 1009 of Lecture Notes in Computer Science. Springer-Verlag, 1995. [ bib | .ps ]
[64] T. Fuchß, W. Reif, G. Schellhorn, and K. Stenzel. Three Selected Case Studies in Verification. In M. Broy and S. Jähnichen, editors, KORSO: Methods, Languages, and Tools for the Construction of Correct Software -- Final Report, volume 1009 of Lecture Notes in Computer Science. Springer-Verlag, 1995. [ bib | .ps.gz ]
[65] T. Schreiber. Auxiliary Variables and Recursive Procedures. In TAPSOFT'97: Theory and Practice of Software Development, volume 1214 of Lecture Notes in Computer Science, pages 697--711. Springer-Verlag, April 1997. [ bib | .ps.gz ]
[66] R. Sedgewick. Quicksort. Garland, New York, 1978. Also appeared as the author's Ph.D. dissertation, Stanford University, 1975. [ bib ]
[67] R. Sedgewick. Algorithms. Addison-Wesley, 1988. [ bib ]
[68] M. Semmelroth and A. Sabry. Monadic Encapsulation in ML. In ACM SIGPLAN International Conference on Functional Programming. ACM, 1999. [ bib | .ps ]
[69] G. L. Steele Jr. Building interpreters by composing monads. In Symposium on Principles of Programming Languages, pages 472--492. Association for Computing Machinery, January 1994. [ bib ]
[70] Y. Takayama. Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs. Journal of Symbolic Computation, 1(12):29--69, 1991. [ bib ]
[71] J.-P. Talpin and P. Jouvelot. Polymorphic Type, Region and Effect Inference. Journal of Functional Programming, 2(3), 1992. [ bib | .ps.Z ]
[72] J.-P. Talpin and P. Jouvelot. The Type and Effect discipline. Information and Computation, 111(2):245--296, 1994. [ bib | .ps.Z ]
[73] M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, University of Edinburgh, 1987. [ bib ]
[74] A. Tolmach. Optimizing ML Using a Hierarchy of Monadic Types. In Types in Compilation '98 Workshop, volume 1473 of Lecture Notes in Computer Science, pages 97--113, Kyoto, Japan, March 1998. Springer-Verlag. [ bib | .ps ]
[75] P. Wadler. Monads for functional programming. In Proceedings of the Marktoberdorf Summer School on Program Design Calculi, August 1992. [ bib ]
[76] P. Wadler. Comprehending monads. Mathematical Structures in Computer Science, pages 461--493, 1992. [ bib ]
[77] D. J. King and P. Wadler. Combining monads. In Glasgow Workshop on Functional Programming. Springer-Verlag Workshops in Computing Series, July 1992. [ bib ]
[78] P. Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi, NATO ASI Series. Springer Verlag, 1993. [ bib ]
[79] P. Wadler. The marriage of effects and monads. In International Conference on Functional Programming, pages 63--74, Baltimore, September 1998. ACM. [ bib ]
[80] J. W. J. Williams. Algorithm 232: Heapsort. Communications of the ACM, 7(6), June 1964. [ bib ]
[81] G. Winskel. The formal semantics of programming languages. The MIT Press, 1993. [ bib ]
[82] A. K. Wright. Typing References by Effect Inference. In European Symposium on Programming, volume 582 of Lecture Notes in Computer Science, pages 473--491. Springer-Verlag, February 1992. [ bib ]
[83] A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115:38--94, 1994. [ bib | .ps.gz ]

This file was generated by bibtex2html 1.97pl3.