@book{AptOlderog91, author = {K. R. Apt and E.-R. Olderog}, title = {Verification of sequential and concurrent programs}, publisher = {Springer-Verlag}, year = 1991 }

@book{Abrial96, author = {J. R. Abrial}, title = {The {B}-{B}ook. {A}ssigning programs to meaning}, publisher = {Cambridge University Press}, year = 1996 }

@article{Back81, author = {R. J. R. Back}, title = {{On correct refinement of programs}}, journal = {{Journal of Computer and Systems Sciences}}, year = 1981, volume = 23, number = 1, pages = {{49--68}}, month = {August} }

@phdthesis{Barras99, author = {B. Barras}, title = {Auto-validation d'un syst{\`e}me de preuves avec familles inductives}, type = {Th{\`e}se de Doctorat}, school = {Universit{\'e} Paris~7}, year = 1999, month = nov }

@book{Bentley82, author = {J. L. Bentley}, title = {{Writing Efficient Programs}}, publisher = {Prentice Hall}, year = 1982 }

@book{Bentley89, author = {J. L. Bentley}, title = {{Programming Pearls}}, publisher = {{Addison-Wesley}}, year = 1989 }

@techreport{Berardi93, author = {S. Berardi}, title = {{Pruning Simply Typed $\lambda$--terms}}, institution = {Turin University}, year = {1993}, ftp = {ftp://lambda.di.unito.it/pub/stefano/PruningFullPaper.rtf.gz} }

@book{BoyerMoore81, title = {{The Correctness Problem in Computer Science}}, publisher = {Academic Press}, year = 1981, editor = {R. S. Boyer and J. S. Moore} }

@inproceedings{Chartier98, author = {P. Chartier}, title = {{Formalization of B in Isabelle/HOL}}, booktitle = {{Proceedings of the Second B International Conference}}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 1393, year = 1998, address = {{Montpellier, France}}, month = {April} }

@proceedings{SecondeConferenceB, title = {{Proceedings of the Second B International Conference}}, year = 1998, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 1393, address = {{Montpellier, France}}, month = {April} }

@inbook{Cousot90, author = {P. Cousot}, editor = {J. van Leeuwen}, title = {{Handbook of Theoretical Computer Science}}, chapter = {{Methods and Logics for Proving Programs}}, publisher = {Elsevier Science Publishers B. V.}, year = 1990, pages = {{841--993}}, volume = {B} }

@incollection{deBruijn80, author = {N.J. de Bruijn}, booktitle = {{To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism}}, editor = {J. P. Seldin and J. R. Hindley}, publisher = {Academic Press}, title = {A survey of the project {Automath}}, year = 1980 }

@book{Dijkstra76, author = {E. W. Dijkstra}, title = {{A Discipline of Programming}}, publisher = {{Prentice Hall}}, year = 1976 }

@article{Floyd62, author = {R. W. Floyd}, title = {{Algorithm 113: Treesort}}, journal = {{Communications of the ACM}}, year = 1962, volume = 5, number = 8, month = {August} }

@inproceedings{Floyd67, author = {R. W. Floyd}, title = {Assigning meanings to programs}, booktitle = {{Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics 19}}, editor = {J. T. Schwartz}, year = 1967, organization = {American Mathematical Society}, address = {Providence}, pages = {{19--32}} }

@unpublished{Gimenez99, author = {E. Gim\'enez}, title = {{Two Approaches to the Verification of Concurrent Programs in Coq}}, year = 1999, note = {Personal communication}, url = {http://pauillac.inria.fr/~gimenez/papers.html} }

@book{GirardLafontTaylor89, author = {J.-Y. Girard and Y. Lafont and P. Taylor}, title = {{Proofs and Types}}, publisher = {Cambridge University Press}, year = 1989 }

@article{Goad80, author = {C. Goad}, title = {{Proofs as Description of Computation}}, journal = {Proceedings of the 5$^{th}$ Conference on Automated Deduction}, year = {1980}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 87 }

@inbook{Gordon96, author = {Mike Gordon}, title = {{Teaching and Learning Formal Methods}}, chapter = {{Teaching hardware and software verification in a uniform framework}}, publisher = {Academic Press}, year = 1996, editor = {C. Neville Dean and Michael G. Hinchey}, url = {http://www.cl.cam.ac.uk/users/mjcg/papers/SpecVerPaper.ps.gz} }

@book{Gries81, author = {D. Gries}, title = {{The Science of Programming}}, publisher = {Springer-Verlag}, year = 1981 }

@phdthesis{Grundy93, author = {Jim Grundy}, title = {A Method of Program Refinement}, school = {University of Cambridge, Computer Laboratory}, address = {New Museums Site, Pembroke Street, Cambridge CB2 3QG, England}, note = {Technical Report 318}, month = nov, year = 1993, url = {http://www.cl.cam.ac.uk/ftp/papers/reports/TR318-jg-program-refinement.ps.gz} }

@inproceedings{GuzmanSuarez94, author = {J. Guzm\'an and A. Su\'arez}, title = {{An Extended Type System for Exceptions}}, booktitle = {{Record of the fifth ACM SIGPLAN workshop on ML and its Applications}}, year = 1994, month = {June}, note = {Also appears as Research Report 2265, INRIA, BP 105 - 78153 Le Chesnay Cedex, France}, url = {http://www.ldc.usb.ve/~suarez/PAPERS/except.ps} }

@techreport{Haskell, editors = {J. Peterson and K. Hammond}, title = {Haskell 1.4, a non-strict, purely functional language}, institution = {Yale University}, year = 1997, month = {April} }

@book{Hayes85, author = {I. Hayes}, title = {Specification {C}ase {S}tudies}, publisher = {Oxford University Computing Laboratory}, year = 1985, note = {Technical monograph PRG-46} }

@article{Hoare61, author = {C. A. R. Hoare}, title = {{Algorithm 65: Find}}, journal = {{Communications of the ACM}}, year = 1961, volume = 4, number = 7, pages = {321--322}, month = {July} }

@article{Hoare62, author = {C. A. R. Hoare}, title = {{Quicksort}}, journal = {Computer Journal}, month = {April}, year = 1962, volume = 5, number = 1, pages = {10--15} }

@article{Hoare69, author = {C. A. R. Hoare}, title = {An axiomatic basis for computer programming}, journal = {{Communications of the ACM}}, year = 1969, volume = 12, number = 10, pages = {576--580,583}, note = {Also in \cite{HoareJones89} pages 45--58} }

@article{Hoare71, author = {C. A. R. Hoare}, title = {Proof of a program: {\em Find}}, journal = {{Communications of the ACM}}, year = 1971, volume = 14, number = 1, month = {January}, pages = {39--45}, note = {Also in \cite{HoareJones89} pages 59--74} }

@book{HoareJones89, author = {C. A. R. Hoare and C. B. Jones}, title = {{Essays in Computing Science}}, publisher = {Prentice Hall}, year = 1989 }

@inproceedings{honsell-mason-smith-talcott-92csl, author = {F. Honsell and I. A. Mason and S. F. Smith and C. L. Talcott}, year = {1992}, title = {{A Theory of Classes for a Functional Language with Effects}}, booktitle = {{1992 Annual Conference of the European Association for Computer Science Logic CSL92, San Miniato}}, series = {Lecture Notes in Computer Science}, publisher = {Springer-Verlag}, volume = {702}, pages = {309--326} }

@book{JacobsBergetc98, author = {B. Jacobs and J. van den Berg and M. Huisman and M. van Berkum and U. Hensel and H. Tews}, title = {{Reasoning about Java Classes (Preliminary Report).}}, publisher = {ACM}, year = 1998, pages = {329--340}, ps = {http://www.cs.kun.nl/~bart/PAPERS/OOPSLA98.ps.Z} }

@book{JavaSpec, author = {J. Gosling and B. Joy and G. Steele}, title = {{The Java Language Specification}}, publisher = {Sun Microsystems}, year = 1996, series = {Java Series} }

@book{Jones80, author = {C. B. Jones}, title = {{Software Development. A rigorous approach}}, publisher = {Prentice Hall}, year = 1980 }

@book{Jones89, author = {C. B. Jones}, title = {Systematic {S}oftware {D}evelopment {U}sing {VDM}}, publisher = {Prentice Hall}, year = 1989 }

@book{Jones92, author = {C. B. Jones}, title = {{VDM : une méthode rigoureuse pour le développement du logiciel}}, publisher = {Masson}, year = 1991, note = {Traduction française de \cite{Jones89}} }

@techreport{JonesDuponcheel93, author = {M. P. Jones and L. Duponcheel}, title = {Composing monads}, institution = {Yale University}, year = {1993}, month = {December}, number = {YALEU/DCS/RR-1004}, type = {Research Report}, ftp = {ftp://ftp.cs.nott.ac.uk/nott-fp/reports/yale/RR-1004.ps} }

@inproceedings{JouvelotGifford91, author = {P. Jouvelot and D. K. Gifford}, title = {Algebraic {R}econstruction of {T}ypes and {E}ffects}, booktitle = {{Proceedings of the 18th ACM Symposium on Principles of Programming Languages}}, month = {January}, year = 1991, pages = {303--310}, publisher = {ACM} }

@book{KernighanPike99, author = {B. W. Kernighan and R. Pike}, title = {{The Practice of Programming}}, publisher = {Addison-Wesley}, year = 1999 }

@book{KernighanRitchie88, author = {B. W. Kernighan and D. M. Ritchie}, title = {{The C Programming Language}}, publisher = {{Prentice Hall}}, year = 1978, edition = {Second} }

@book{Kleene52, author = {S.C. Kleene}, publisher = {North-Holland}, series = {Bibliotheca Mathematica}, title = {Introduction to Metamathematics}, year = 1952 }

@techreport{Kleymann98, author = {T. Kleymann}, title = {{Metatheory of Verification Calculi in LEGO: To What Extent Does Syntax Matter?}}, institution = {LFCS}, year = 1998, number = {98-393}, month = {September}, url = {http://www.dcs.ed.ac.uk/lfcsreps/EXPORT/98/ECS-LFCS-98-393/ECS-LFCS-98-393.ps.gz} }

@book{KnuthV1, author = {D. E. Knuth}, title = {{The Art of Computer Programming. Volume 1: Fundamental Algorithms}}, publisher = {{Addison-Wesley}}, year = 1968 }

@book{KnuthV2, author = {D. E. Knuth}, title = {{The Art of Computer Programming. Volume 2: Seminumerical Algorithms}}, publisher = {{Addison-Wesley}}, year = 1969 }

@book{KnuthV3, author = {D. E. Knuth}, title = {{The Art of Computer Programming. Volume 3: Sorting and Searching}}, publisher = {{Addison-Wesley}}, year = 1973 }

@book{Knuth96, author = {D. E. Knuth}, title = {{Selected Papers on Computer Science}}, publisher = {CSLI Publications and Cambridge University Press}, year = 1996 }

@article{KnuthMorrisPratt77, author = {D. E. Knuth and J. H. Morris and V. R. Pratt}, title = {{Fast pattern matching in strings}}, journal = {{SIAM Journal on Computing}}, year = 1977, volume = 6, pages = {323--350} }

@inproceedings{LaunchburyPeytonJones94, author = {J. Launchbury and S. L. Peyton Jones}, title = {{Lazy Functional State Threads}}, booktitle = {{SIGPLAN Symposium on Programming Language Design and Implementation (PLDI'94)}}, year = 1994, month = {June}, pages = {{24--35}}, url = {http://www.dcs.gla.ac.uk/fp/papers/lazy-functional-state-threads.ps.Z} }

@article{LeroyPessaux00, author = {X. Leroy and F. Pessaux}, title = {Type-based analysis of uncaught exceptions}, journal = {{ACM Transactions on Programming Languages and Systems}}, year = 2000, number = 22, volume = 2 }

@inproceedings{LeroyWeis91, author = {X. Leroy and P. Weis}, title = {Polymorphic type inference and assignment}, booktitle = {{Proceedings of the 1991 ACM Conference on Principles of Programming Languages}}, pages = {{291--302}}, year = 1991, url = {http://pauillac.inria.fr/~xleroy/publi/polymorphic-assignment.dvi.gz} }

@techreport{Lillibridge95, author = {M. Lillibridge}, title = {Exceptions {A}re {S}trictly {M}ore {P}owerful {T}han {Call/CC}}, institution = {Carnegie {M}ellon {U}niversity}, year = 1995, month = {July}, number = 178, ftp = {ftp://reports.adm.cs.cmu.edu/usr/anon/1995/CMU-CS-95-178.ps} }

@inproceedings{MasonTalcott89, author = {I. A. Mason and C. L. Talcott}, title = {{Axiomatizing Operational Equivalence in the Presence of Side Effects}}, booktitle = {{Fourth Annual Symposium on Logic in Computer Science}}, pages = {284--293}, year = 1989, publisher = {IEEE}, ps = {http://maths.une.edu.au/~iam/Data/Papers/89lics.ps} }

@article{Milner78, author = {R. Milner}, title = {A theory of type polymorphism in programming}, journal = {Journal of Computing System Science}, year = 1978, volume = 17, pages = {{348--375}} }

@techreport{Moggi89a, author = {E. Moggi}, title = {An abstract view of programming languages}, institution = {Edinburgh University, Department of Computer Science}, year = 1989, month = {June}, number = {ECS-LFCS-90-113}, note = {Lecture Notes for course CS 359, Stanford University}, url = {http://www.disi.unige.it/person/MoggiE/ftp/abs-view.dvi.gz} }

@inproceedings{Moggi89c, author = {E. Moggi}, title = {Computational lambda-calculus and monads}, booktitle = {{IEEE Symposium on Logic in Computer Science}}, year = {1989}, url = {http://www.disi.unige.it/person/MoggiE/ftp/lc88.dvi.gz} }

@article{Moggi91, author = {E. Moggi}, title = {{Notions of computations and monads}}, journal = {{Information and Computation}}, year = 1991, volume = 93, number = 1 }

@book{Monin96, author = {J.-F. Monin}, title = {{Comprendre les méthodes formelles}}, publisher = {Masson}, year = 1996 }

@inproceedings{MoggiPalumbo99, author = {E. Moggi and F. Palumbo}, title = {{Monadic Encapsulation of Effects: a Revised Approach}}, booktitle = {{Third International Workshop on Higher Order Operational Techniques in Semantics}}, year = 1999, ps = {http://www.disi.unige.it/person/MoggiE/ftp/hoots99.ps.gz} }

@book{Morgan90, author = {C. C. Morgan}, title = {{Programming from Specifications}}, publisher = {Prentice Hall}, year = 1990 }

@techreport{MorrisPratt70, author = {J. H. Morris and V. R. Pratt}, title = {{A Linear Pattern Matching Algorithm}}, institution = {Computing Center, University of California, Berkeley}, year = 1970, number = 40 }

@unpublished{Munoz98, author = {C. Mu{\~{n}}oz}, title = {{Supporting the B-method in PVS: An Approach to the Abstract Machine Notation in Type Theory}}, note = {Submitted to FSE-98}, year = 1998, url = {http://www.csl.sri.com/~munoz/Papers/pbs.ps.gz} }

@article{OHearnReynolds97, author = {P. W. O'Hearn and J. C. Reynolds}, title = {From {A}lgol to {P}olymorphic {L}inear {L}ambda-calculus}, journal = {{Journal of the ACM}}, year = 1997, month = {April}, note = {To appear}, ftp = {ftp://ftp.dcs.qmw.ac.uk/lfp/ohearn/AlgolToPolyLin.ps} }

@incollection{Paulin91, author = {C. Paulin-Mohring}, title = {R\'ealisabilit\'e et extraction de programmes}, booktitle = {Logique et informatique : une introduction}, publisher = {INRIA}, year = 1991, pages = {163--180} }

@incollection{Reif95, author = {W. Reif}, title = {{The KIV-approach to software verification}}, booktitle = {{KORSO: Methods, Languages, and Tools for the Construction of Correct Software -- Final Report}}, year = 1995, editor = {M. Broy and S. J\"ahnichen}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 1009, ftp = {ftp://ftp.informatik.uni-ulm.de/pub/PM/kiv/papers/kiv-approach.ps} }

@incollection{KIVCaseStudies, author = {T. Fuchß and W. Reif and G. Schellhorn and K. Stenzel}, title = {{Three Selected Case Studies in Verification}}, booktitle = {{KORSO: Methods, Languages, and Tools for the Construction of Correct Software -- Final Report}}, year = 1995, editor = {M. Broy and S. J\"ahnichen}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 1009, ftp = {ftp://ftp.informatik.uni-ulm.de/pub/PM/kiv/papers/three-selected-case-studies.ps.gz} }

@inproceedings{Schreiber97, author = {T. Schreiber}, title = {{Auxiliary Variables and Recursive Procedures}}, booktitle = {{TAPSOFT'97: Theory and Practice of Software Development}}, publisher = {Springer-Verlag}, volume = 1214, series = {Lecture Notes in Computer Science}, year = 1997, month = {April}, pages = {697--711}, ftp = {ftp://ftp.dcs.ed.ac.uk/pub/tms/tapsoft97-with-page-numbers.ps.gz} }

@book{Sedgewick78, author = {R. Sedgewick}, title = {Quicksort}, publisher = {Garland, New York}, year = 1978, note = {Also appeared as the author's Ph.D. dissertation, Stanford University, 1975} }

@book{Sedgewick88, author = {R. Sedgewick}, title = {Algorithms}, publisher = {{Addison-Wesley}}, year = 1988 }

@inproceedings{SemmelrothSabry99, author = {M. Semmelroth and A. Sabry}, title = {{Monadic Encapsulation in ML}}, booktitle = {{ACM SIGPLAN International Conference on Functional Programming}}, publisher = {ACM}, year = 1999, ps = {http://www.cs.uoregon.edu/~sabry/papers/monadic-encap.ps} }

@inproceedings{Steele94, author = {G. L. Steele Jr.}, title = {Building interpreters by composing monads}, booktitle = {{Symposium on Principles of Programming Languages}}, year = {1994}, month = {January}, publisher = {Association for Computing Machinery}, pages = {472--492} }

@article{Takayama91, author = {Y. Takayama}, title = {{Extraction of Redundancy-free Programs from Constructive Natural Deduction Proofs}}, journal = {Journal of Symbolic Computation}, year = {1991}, volume = {1}, number = {12}, pages = {29-69} }

@article{TalpinJouvelot92, author = {J.-P. Talpin and P. Jouvelot}, title = {{Polymorphic Type, Region and Effect Inference}}, journal = {Journal of Functional Programming}, year = 1992, volume = 2, number = 3, publisher = {Cambridge University Press}, ftp = {ftp://cri.ensmp.fr/pub/Papers/Talpin/jfp92.ps.Z} }

@article{TalpinJouvelot94, author = {J.-P. Talpin and P. Jouvelot}, title = {{The Type and Effect discipline}}, journal = {Information and Computation}, year = 1994, volume = 111, number = 2, pages = {245-296}, publisher = {Academic Press}, ftp = {ftp://cri.ensmp.fr/pub/Papers/Talpin/lics92.ps.Z} }

@phdthesis{Tofte87, author = {M. Tofte}, title = {{Operational Semantics and Polymorphic Type Inference}}, school = {University of Edinburgh}, year = 1987 }

@inproceedings{Tolmach98, author = {A. Tolmach}, title = {{Optimizing ML Using a Hierarchy of Monadic Types}}, booktitle = {{Types in Compilation '98 Workshop}}, pages = {97--113}, year = 1998, address = {Kyoto, Japan}, month = {March}, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 1473, ps = {http://www.cs.pdx.edu/~apt/monad_types_paper.ps} }

@inproceedings{Wadler92a, author = {P. Wadler}, title = {Monads for functional programming}, booktitle = {{Proceedings of the Marktoberdorf Summer School on Program Design Calculi}}, year = {1992}, month = {August} }

@article{Wadler92b, author = {P. Wadler}, title = {Comprehending monads}, journal = {Mathematical Structures in Computer Science}, year = {1992}, pages = {461--493} }

@inproceedings{Wadler92c, author = {D. J. King and P. Wadler}, title = {Combining monads}, booktitle = {{Glasgow Workshop on Functional Programming}}, year = {1992}, month = {July}, publisher = {Springer-Verlag Workshops in Computing Series} }

@incollection{Wadler93, author = {P. Wadler}, title = {Monads for functional programming}, booktitle = {{Program Design Calculi}}, publisher = {Springer Verlag}, year = 1993, editor = {M. Broy}, series = {NATO ASI Series} }

@inproceedings{Wadler98, author = {P. Wadler}, title = {{The marriage of effects and monads}}, booktitle = {{International Conference on Functional Programming}}, year = 1998, publisher = {ACM}, address = {Baltimore}, month = {September}, pages = {63--74} }

@article{Williams64, author = {J. W. J. Williams}, title = {{Algorithm 232: Heapsort}}, journal = {{Communications of the ACM}}, year = 1964, volume = 7, number = 6, month = {June} }

@book{Winskel93, author = {G. Winskel}, title = {The formal semantics of programming languages}, publisher = {The MIT Press}, year = 1993 }

@inproceedings{Wright92, author = {A. K. Wright}, title = {Typing {R}eferences by {E}ffect {I}nference}, booktitle = {{European Symposium on Programming}}, year = 1992, publisher = {Springer-Verlag}, series = {Lecture Notes in Computer Science}, volume = 582, pages = {473--491}, month = {February} }

@article{WrightFelleisen94, author = {A. K. Wright and M. Felleisen}, title = {A syntactic approach to type soundness}, journal = {Information and Computation}, volume = 115, year = 1994, pages = {38--94}, url = {http://www.cs.rice.edu/CS/PLT/Publications/ic94-wf.ps.gz} }

*This file was generated by
bibtex2html 1.97pl3.*