@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.