BNFConv.bib

@STRING{fac = "Formal Aspects of Computing"}
@STRING{amai = "Annals of Mathematics and Artificial Intelligence"}
@STRING{jsl = "Journal of Symbolic Logic"}
@STRING{jsc = "Journal of Symbolic Computation"}
@STRING{jlc = "Journal of Logic and Computation"}
@STRING{jlp = "Journal of Logic Programming"}
@STRING{JFP = "The {J}ournal of {F}unctional {P}rogramming"}
@STRING{jar = "Journal of Automated Reasoning"}
@STRING{sl = "Studia Logica"}
@STRING{ipl = "Information Processing Letters"}
@STRING{tcs = "Theoretical Computer Science"}
@STRING{lnm = "Lecture Notes in Mathematics"}
@STRING{lncs = "LNCS"}
@STRING{lnai = "LNCS"}
@STRING{spv = "Springer-Verlag"}
@STRING{cacm = "Communications of the {ACM}"}
@STRING{jacm = "Journal of the {ACM}"}
@STRING{sc = "Soft Computing---A Fusion of Foundations, Methodologies
		  and Applications"}



@BOOK{ Kern88,
  AUTHOR    = {B.W. Kernighan and D.M. Ritchie},
  TITLE     = {{T}he {C} {P}rogramming {L}anguage},
  SERIES    = {},
  VOLUME    = {},
  PUBLISHER = {Prentice-Hall, Englewood Cliffs, New Jersey, USA},
  YEAR      = 1988,
  NOTE      = {2nd edition},
  CONTENTS  = {Standard book on the programming language C.},
  TOPICS    = {Language Manuals,C}
}

@Article{zephyr,
  author = "D. C. Wang and A. W. Appel and J. L. Korn and C. S. Serra",
  title =  {{The Zephyr Abstract Syntax Description Language}},
  note  = {{USENIX Association}},
  year =   1997
}

@Article{metal,
  author = "G. Kahn and B. Lang and B. Mélèse and E. Morcos",
  title =  "Metal: a formalism to specify formalisms",
  journal = {Science of {C}omputer {P}rogramming},
  year =   1983,
  volume = 3,
  pages =  {151--188}
}

@InCollection{pentus,
  author = "M. Pentus",
  title = "Lambek grammars are context-free",
  booktitle = {{LICS}, {Utrecht}, {The} {Netherlands}},
  year = 1993,
  pages = {35--42}
}


@ARTICLE{lambek,
    AUTHOR = "J. Lambek",
    TITLE = "The mathematics of sentence structure",
    JOURNAL = {{American Mathematical Monthly}},
    VOLUME = {65},
    PAGES = {154-170},
    YEAR = {1958} 
}

@Article{bar-hillel,
  author = "Y. Bar-Hillel",
  title =  "A quasi-arithmetical notation for syntactic description",
  journal = {Language},
  year =   1953,
  volume = 29,
  pages = {27-58}
}


@Book{rosetta,
  author = {M.~T. Rosetta},
  title = 	{Compositional Translation},
  publisher = 	"Kluwer",
  address =     "Dordrecht",
  year = 	1994
}

@Book{lamport-latex,
  author = {L. Lamport},
  title = 	{{\LaTeX\ A Document Preparation System}},
  publisher = 	{Addison-Wesley},
  year = 	1986
}

@Book{hopcroft,
  author = {J. Hopcroft and J. Ullman},
  title = 	{{Introduction to Automata Theory, Languages, and Computation}},
  publisher = 	{Addison-Wesley},
  year = 	1979
}

@Book{jones-partial,
  author = {N.D. Jones and C.K. Gomard and P. Sestoft},
  title = 	{Partial Evaluation and Automatic Program Generation},
  publisher = 	{Prentice-Hall},
  year = 	1993
}


@Article{frost,
  author = "R. Frost and J. Launchbury",
  title =  "Constructing natural language interpreters 
            in a lazy functional language",
  journal = {The {Computer} {Journal}},
  year =   1989,
  volume = 32,
  number = 2,
  pages =  {108--121}
}



@Article{pereira,
  author = 	 {H.~D. Warren and F. Pereira},
  title = 	 {An Efficient Easily Adaptable System for Interpreting Natural 
                  Language Queries},
  year = 	 {1982},
  journal =       {{Computational Linguistics}},
  volume = 8,
  pages = {110-122}
}


@Misc{bnfc,
  author = "Markus Forsberg and Aarne Ranta",
  title = "BNF Converter site",
  howpublished = "Program and documentation, 
                  \verb6http://www.cs.chalmers.se/~markus/BNFC/6", 
  documentURL = "\verb6http://www.cs.chalmers.se/~markus/BNFC/6",
  year = 2002
}

@Misc{huet-sanskrit,
  author = "G. Huet",
  title = "Sanskrit site",
  howpublished = "Program and documentation, 
                  \verb6http://pauillac.inria.fr/~huet/SKT/6", 
  documentURL = "\verb6http://pauillac.inria.fr/~huet/SKT/index.html6",
  year = 2000
}


@Misc{italiano,
  author = "A. Ranta",
  title = {1+n representations of {Italian} morphology},
  howpublished = {Essays dedicated to {Jan von Plato} 
                  on the occasion of his 50th birthday,
                  \verb6http://www.valt.helsinki.fi/kfil/jvp50.htm6}, 
  documentURL = "\verb6http://www.valt.helsinki.fi/kfil/jvp50.htm6",
  year = 2001
}


@Article{hudak,
  author = "P. Hudak",
  title = "Building domain-specific embedded languages",
  journal = "{ACM} {Computing} {Surveys}",
  year =   1996,
  volume = 28,
  number = 4
}

@Article{algol,
  author = "P. Naur",
  title = {{Revised Report of the Algorithmic Language Algol 60}},
  journal = {{Comm.\ ACM}},
  year =   1963,
  volume = 6,
  pages = {1--17}
}

@Book{bescherelle,
  author = "Bescherelle",
  title = "La conjugaison pour tous",
  publisher = "Hatier",
  year = 1997
}


@Book{shieber,
  author = "S. Shieber",
  title = {{An Introduction to Unification-Based Approaches to Grammars}},
  publisher = "University of Chicago Press",
  year = 1986
}

@BOOK{prawitz,
    AUTHOR = "D. Prawitz",
    TITLE = {{Natural Deduction}},
    PUBLISHER = {Almqvist \& Wiksell},
    ADDRESS = {Stockholm},
    YEAR = {1965} }

@BOOK{CAML,
    AUTHOR = "P. Weis and X. Leroy",
    TITLE = {{Le langage Caml}},
    PUBLISHER = {Dunod},
    ADDRESS = "Paris",
    YEAR = {1999} 
 }

@BOOK{ML,
    AUTHOR = "R. Milner and M. Tofte and R. Harper",
    TITLE = {{Definition of Standard ML}},
    PUBLISHER = {MIT Press},
    YEAR = {1990} 
 }

@BOOK{ML-wik,
    AUTHOR = "{Wikstr\"{o}m}, {\AA ke}",
    TITLE = "Functional Programming Using Standard ML",
    PUBLISHER = {Prentice-Hall},
    ADDRESS = {London},
    YEAR = {1987} }

@Article{coquand-typecheck,
  author = "T. Coquand",
  title = "An Algorithm for Type Checking Dependent Types",
  journal = "Science of {Computer} {Programming}",
  year = 1996,
  volume = 26,
  pages = {167-177}
}


@Book{boehm,
  author = "H. Barendregt",
  title = {{The Lambda Calculus. Its Syntax and Semantics}},
  publisher = "North-Holland",
  year = 1981
}


@Article{hutton,
  author = "G. Hutton",
  title = "Higher-order functions for parsing",
  journal = {J. Functional Programming},
  year =   1992,
  volume = 2,
  number = 3,
  pages =  {323--343}
}


@InProceedings{wadler,
  author = "P. Wadler",
  title =  "How to replace failure by a list of successes",
  booktitle = {{Second International Conference on Functional 
               Programming Languages and Computer Architectures}},
  series = lncs,
  year =   1985,
  address = spv
}

@InProceedings{jones-hudak,
  author = "M. Jones and P. Hudak",
  title =  "Using Types to Parse Natural Language",
  booktitle = {{Proceedings of the Glasgow Workshop on Functional Programming}},
  series = {{LNCS}},
  year =   1995,
  address = spv
}

@Article{earley,
  author = "J. Earley",
  title = "An efficient context-free parsing algorithm",
  journal = {Communications of the {ACM}},
  year = 1970,
  volume = 13,
  number = 2,
  pages =  {94--102}
}

@InCollection{joshi,
  author = "A. Joshi",
  title =  {Tree-Adjoining Grammars: How much context-sensitivity is required 
            to provide reasonable structural descriptions},  
  booktitle = {{Natural Language Parsing}},
  year =   1985,
  editor = "D. Dowty and L. Karttunen and A. Zwicky",
  publisher = {Cambridge University Press},
  pages =  {206--250}
}

@Article{Wirth,
  author = "N. Wirth",
  title = "Program Development by Stepwise Refinement",            
  journal = "Communications of the ACM",
  year =   1971,
  volume = 14,
  pages = {221--227}
}


@Article{GF-paper,
  author = "A. Ranta",
  title =  {{Grammatical Framework: A Type-Theoretical Grammar Formalism}}, 
  journal = JFP,
  note =  {To appear}
}

@Article{huet-zipper,
  author = "G. Huet",
  title =  {The {Zipper}}, 
  journal = JFP,
  year =   1997,
  volume = 7,
  number = 5,
  pages =  {549--554}
}

@Article{huet-lang,
  author = {G. Huet and B. Lang},
  title =  {Proving and applying program transformations expressed 
            with second-order patterns}, 
  journal = {{Acta Informatica}},
  year =   1978,
  volume = 11
}

@Article{knuth-attr,
  author = "D. Knuth",
  title = "Semantics of Context-Free Languages",           
  journal = {Mathematical {Systems} {Theory}},
  year =   1968,
  volume = 2,
  pages =  {127--145}
}

@Article{LR,
  author = {D. Knuth},
  title = {On the translation of languages from left to right},           
  journal = {Information and {Control}},
  year =   1965,
  volume = 8,
  pages =  {607--639}
}


@InProceedings{luocall,
  author = {Z. Luo and P. Callaghan},
  title = {Mathematical Vernacular and Conceptual Well-Formedness in Mathematical
           Language},
  booktitle = {{Logical Aspects of Computational Linguistics (LACL)}} ,
  year = 1999,
  editor = {A. Lecomte and F. Lamarche and G. Perrier},
  series = lnai,
  volume = 1582,
  pages = {231--250}
}

@Book{hpsg,
  author = "C. Pollard and I. Sag",
  title = {{Head-Driven Phrase Structure Grammar}},	
  publisher = {University of Chicago Press},
  year = 1994
}


@ARTICLE{dcg,
    AUTHOR = "F. Pereira and D. Warren",
    TITLE = "Definite clause grammars
  for language analysis---a survey of the formalism and a
  comparison with augmented transition networks",
    JOURNAL = {{Artificial Intelligence}},
    VOLUME = {13},
    PAGES = {231--278},
    YEAR = {1980} }








@inproceedings{cayenne,
	 AUTHOR = {L. Augustsson},
	 TITLE = {{Cayenne---a language with dependent types}},
	 BOOKTITLE = {Proc. of {ICFP'98}},
	 PUBLISHER = {ACM Press},
	 MONTH = {September},
	 YEAR = {1998}
 }


@book{nordstrom:book,
	AUTHOR  = {B. Nordstr{\"{o}}m and K. Petersson and J. M. Smith},
	TITLE	= {{Programming in Martin-Löf's Type Theory. An Introduction}},
	YEAR    = {1990},
	PUBLISHER = {Oxford University Press}
}

@book{constable,
        AUTHOR = {R. L. Constable},
	TITLE  = {{Implementing Mathematics with the NuPRL Proof Development System}},
	YEAR   = {1986},
	PUBLISHER = {Prentice-Hall}
}


@book{martin-lof,
	AUTHOR	= {P. Martin-L\"{o}f},
	TITLE	= {{Intuitionistic Type Theory}},
	ADDRESS = {Napoli},
	YEAR	= {1984},
	PUBLISHER = {Bibliopolis}
}

@InProceedings{dymetman,
  author = 	 {M.\ Dymetman and V.\ Lux and A.\ Ranta},
  title = 	 {{XML} and Multilingual Document Authoring: Convergent Trends},
  booktitle = 	 {{COLING}, {Saarbr\"ucken}, {Germany}},
  pages =        {243--249},
  year =	 {2000}
}

@InProceedings{GF-Alfa,
  author = 	 {T.\ Hallgren and A.\ Ranta},
  title = 	 {An Extensible Proof Text Editor},
  editor =       {M. Parigot and A. Voronkov},
  booktitle = 	 {{LPAR-2000}},
  year =	 {2000},
  series =	 {LNAI},
  volume =       {1955},
  publisher =    {Springer},
  pages =        {70--84}
}

@InProceedings{FASE,
  author = 	 {K.\ Johannisson and R.\ Hähnle and A.\ Ranta},
  title = {An Authoring Tool for Informal and Formal Requirements Specifications},
  booktitle = 	 {{FASE}},
  year =	 {2002},
  series =	 {LNCS},
  note =         {To appear},
  publisher =    {Springer}
}


@Misc{Cactus,
  author =       {N. Martinsson},
  title =  {{Cactus (Concrete- to Abstract-syntax Conversion Tool with Userfriendly Syntax) }},
  note = {\verb8http://www.mdstud.chalmers.se/~md6nm/cactus/8},
  howpublished = "Master's Thesis in Computer Science",
  address = "Chalmers University",
  year =         2001
}

@Misc{haskell98-Cactus,
  author =       {T. Hallgren},
  title =  {{The Haskell 98 grammar in Cactus}},
  note = {\verb6http://www.cs.chalmers.se/~hallgren/CactusExample/6},
  address = "Chalmers University",
  year =         2001
}

@Misc{GF-homepage,
  author =       {A. Ranta},
  title =        {{Grammatical Framework Homepage}},
  note = {\verb6www.cs.chalmers.se/~aarne/GF/6},
  url = "http://www.cs.chalmers.se/~aarne/GF/",
  year =         2000
}

@Misc{happy,
  author =       {S. Marlow},
  title =        {{Happy, The Parser Generator for Haskell}},
  note = {\verb6http://www.haskell.org/happy/6},
  year =         2001
}

@Misc{latex,
 author = {Donald Knuth},
 title  = {Latex},
 note   = {\verb6http://www.latex-project.org/6}
}

@Misc{cup,
 author = {Scott E. Hudson},
 title  = {{CUP Parser Generator for Java}},
 note   = {\verb6http://www.cs.princeton.edu/~appel/modern/java/CUP/6},
 year   = 1999
}

@Misc{alex,
 author = {C. Dornan},
 title  = {{Alex: a Lex for Haskell Programmers}},
 note   = {\verb6http://www.cs.ucc.ie/dornan/alex.html6},
 year   = 1997
}

@Misc{jlex,
 author = {E. Berk and C. Ananian},
 title  = {{JLex: A Lexical Analyzer Generator for Java}},
 note   = {\verb6http://www.cs.princeton.edu/~appel/modern/java/JLex/6},
 year   = 2000
}

@inproceedings{magnusson-nordstr,
        AUTHOR = {L. Magnusson and B. Nordstr\"{o}m},
        BOOKTITLE = {{Types for Proofs and Programs}},
        PUBLISHER = {Springer},
        SERIES = {LNCS 806},
        PAGES = {213--237},
        TITLE   = {The {ALF} proof editor and its proof engine}, 
        YEAR = {1994}
        }

@Book{Ranta94,
  author =	 {A. Ranta},
  title = 	 {{Type Theoretical Grammar}},
  publisher = 	 {Oxford University Press},
  year = 	 {1994}
}

@Book{appel,
  author =	 {A. Appel},
  title = 	 {{Modern Compiler Implementation in ML}},
  publisher = 	 {Cambridge University Press},
  year = 	 {1998}
}

@Misc{coq,
  key = {Coq},
  title =	 {Coq Homepage},
  howpublished = {\verb6pauillac.inria.fr/coq/6},
  documentURL = "http://pauillac.inria.fr/coq/",
  year =	 1999
}

@InProceedings{wysiwym,
  author =       {R. Power and D. Scott},
  title =        {Multilingual authoring using feedback texts},
  booktitle =    {{COLING}-{ACL}},
  year =         1998
}

@PhdThesis{fudgets,
  author =   {M. Carlsson and T. Hallgren},
  title =   {{Fudgets---Purely Functional Processes with
                  applications to Graphical User Interfaces}},
  school =   {Department of Computing Science, Chalmers University
                  of Technology},
  year =   1998,
  documentURL = "http://www.cs.chalmers.se/~hallgren/Thesis/"
}

@article{harper-honsell,
        AUTHOR = {R. Harper and F. Honsell and G. Plotkin},
        TITLE = {{A Framework for Defining Logics}},
        JOURNAL = {{JACM}},
        VOLUME = {40},
        NUMBER = {1},
        YEAR = {1993},
        PAGES = {143--184}
}

@InProceedings{CKT95,
  author =       "Y. Coscoy and G. Kahn and L. Thery",
  title =        "Extracting text from proofs",
  series =       lncs,
  volume =       "902",
  pages =        {109--123},
  year =         "1995",
  booktitle =    "Proc.\ {Second} {Int.} {Conf.} on 
                  {Typed} {Lambda} {Calculi} and {Applications}",
  editor =       "M. Dezani-Ciancaglini and G. Plotkin"
}

@Book{WarmerKleppe99,
  author =       "J. Warmer and A. Kleppe",
  title =        "The Object Constraint Language: Precise Modelling with {UML}",
  publisher =    "Addison-Wesley",
  year =         "1999"
}


@InProceedings{HoltEwan99,
  author = 	 {Alexander Holt and Ewan Klein},
  title = 	 {A semantically-derived subset of {E}nglish for 
                  hardware verification},
  booktitle = 	 {Proc.\ Ann.\ Meeting Ass.\ for 
                  Comp.\ Ling.},
  pages =	 {451--456},
  year =	 {1999},
  url = {http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-sds/ps/}
}

@misc{bohlin-trindi,
  author = {P. Bohlin and J. Bos and S. Larsson and 
             I. Lewin and C. Matheson and D. Milward}, 
  year = 1999,
  title = {Survey of Existing Interactive Systems},
  note = {Trindi deliverable D1.3, Gothenburg University}
  }

@Article{teitelbaum,
  author =       "T. Teitelbaum and T. Reps",
  title =        {The {Cornell} {Program} {Synthesizer}: a syntax-directed
                  programming environment},
  journal =      {Commun. {ACM}},
  year =         "1981",
  volume =       "24",
  number =       "9",
  pages =        {563-573}
}


@misc{haskell98,
         author= {S. {Peyton Jones} and J. Hughes},
         title={{Report on the Programming Language Haskell 98, a 
                 Non-strict, Purely Functional Language}},
         year=1999, 
         month={February},
         howpublished={Available from \verb!http://www.haskell.org!}
}

@Manual{UML1.3-specification,
  key = {UML 1.3},
  title = 	 {Unified Modelling Language Specification, version 1.3},
  organization = {Object Modeling Group},
  month =	 mar,
  year =	 2000,
  url  =         {http://cgi.omg.org/cgi-bin/doc?formal/00-03-01.ps.gz},
  note =	 {OMG document formal/00-03-01. {URL:} 
                  \texttt{http://cgi.omg.org/cgi-bin/doc?formal/00-03-01.ps.gz}}
}

@TechReport{LBR00,
  author =       "G. T. Leavens and A. L. Baker and C. Ruby",
  title =        "Preliminary Design of {JML}: A Behavioral Interface
                 Specification Language for {Java}",
  institution =  "Iowa State University, Department of Computer
                 Science",
  year =         "2000",
  number =       "98-06i",
  month =        feb,
  note =         "URL: \texttt{ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz}",
  url =          "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz"
}


@TechReport{johnson-yacc,
  author =       {S. C. Johnson},
  title =        {{Yacc --- yet another compiler compiler}},
  institution =  {{AT \& T Bell Laboratories, Murray Hill, NJ}},
  year =         {1975},
  number = {{CSTR-32}}
}

@TechReport{hallgren-2000,
  author =       {T. Hallgren},
  title =        {The Correctness of Insertion Sort},
  institution =  {Chalmers University of Technology, 
                  Department of Computer Science},
  year =         {2000},
  note = {URL: \verb!http://www.cs.chalmers.se/~hallgren/Papers/insertion_sort.ps!}
}


@InProceedings{power-scott-1998,
  author =       {R. Power and D. Scott},
  title =        {Multilingual authoring using feedback texts},
  booktitle =    {COLING-ACL 98},
  year =         1998,
  address =      {Montreal, Canada}
}

@InProceedings{coquand1999,
  author =       {C. Coquand and T. Coquand},
  title =        {Structured Type Theory},
  booktitle =    {Workshop on Logical Frameworkds and Meta-languages},
  year =         1999,
  address =      {Paris, France}
}

@InProceedings{ranta-cooper,
  author =       {A. Ranta and R. Cooper},
  title =        {Dialogue Systems as Proof Editors},
  booktitle =    {{IJCAR}/{ICoS-3}},
  year =         2001,
  address =      {{Siena}, {Italy}}
}

@InProceedings{curry,
    AUTHOR = "H. B. Curry",
    TITLE = "Some logical aspects of grammatical structure",
    EDITOR = "Jakobson, Roman",
    BOOKTITLE = {{Structure of Language and its
  Mathematical Aspects: Proceedings of the Twelfth Symposium
  in Applied Mathematics}},
    PUBLISHER = {American Mathematical Society},
    YEAR = {1963}, 
    PAGES = {56-68}
}

@inproceedings{bengt-lena1995,
        AUTHOR = {L. Magnusson and B. Nordstr\"{o}m},
        BOOKTITLE = {{ Types for Proofs and Programs}},
        PUBLISHER = {Springer-Verlag},
        SERIES = {LNCS},
        VOL = {806},
        PAGES = {213-237},
        TITLE   = {{The ALF proof editor and its proof engine}}, 
        ADDRESS = {Nijmegen},
        YEAR = {1994}
        }

@article{kay1996,
         AUTHOR = {M. Kay},
         TITLE  = {{The Proper Place of Men and Machines in Language Translation}},
         JOURNAL = {{Machine Translation}},
         YEAR = {1996},
         NUMBER = {},
         PAGES = {}
 }


@unpublished{boeing,
  title   = {{Boeing Simplified English Checker}},
  author  = {{The Boeing Company}},
  howpublished	= {Online document},
  year          = {2001},
  note		= {\verb!http://www.boeing.com/assocproducts/sechecker/!}
  }

@unpublished{XML,
  title   = {{Extensible Markup Language (XML)}},
  author  = {{The World Wide Web Consortium}},
  howpublished	= {Online document},
  year          = {2000},
  note		= {\verb!http://www.w3.org/XML/!}
  }

@unpublished{agda-homepage,
  author  = "C. Coquand",
  title   = "{{AGDA Homepage}}",
  year    = 1998,
  howpublished	= {Online document},
  note		= {\verb!http://www.cs.chalmers.se/~catarina/agda/!} ,
  documenturl	= "http://www.cs.chalmers.se/~catarina/agda/"
  }

@InProceedings{coquand:stt-lfm99,
  author = 	 {C. Coquand and T. Coquand},
  title = 	 {Structured Type Theory},
  booktitle = 	 {Workshop on Logical Frameworkds and Meta-languages},
  year =	 1999,
  address =	 {Paris, France},
  month =	 {Sep}
}

@inproceedings{augustsson:cayenne,
	 AUTHOR = {L. Augustsson},
	 TITLE = {{Cayenne --- a language with dependent types}},
	 BOOKTITLE = {Proc. of the International Conference on Functional Programming (ICFP'98)},
	 PUBLISHER = {ACM Press},
	 MONTH = {September},
	 YEAR = {1998}
 }

@PhdThesis{carlsson98:fudgets_thesis,
  author =   {M. Carlsson and T. Hallgren},
  title =   {{Fudgets --- Purely Functional Processes with
                  applications to Graphical User Interfaces}},
  booktitle =   {{Fudgets --- Purely Functional Processes with
                  applications to Graphical User Interfaces}},
  school =   {Department of Computing Science, Chalmers University
                  of Technology},
  year =   1998,
  address =  {S-412 96 Göteborg, Sweden},
  month =  {March},
  documentURL = "http://www.cs.chalmers.se/~hallgren/Thesis/"
}

@book{martin-lof:padova,
	AUTHOR	= {P. Martin-L\"{o}f},
	TITLE	= {{Intuitionistic Type Theory}},
	ADDRESS = {Napoli},
	YEAR	= {1984},
	PUBLISHER = {Bibliopolis}
}

@book{montague,
	AUTHOR	= {R.\ Montague},
	TITLE	= {{Formal Philosophy}},
	ADDRESS = {New Haven},
	YEAR	= {1974},
	NOTE	= {Collected papers edited by R.\ Thomason},
	PUBLISHER = {Yale University Press}
}

@misc{alfa-homepage,
		  author = {T. Hallgren},
                  year = {2000},
		  title = {{Home Page of the Proof Editor Alfa}},
		  howpublished = {\verb!http://www.cs.chalmers.se/~hallgren/Alfa/!},
                  documentURL = {http://www.cs.chalmers.se/~hallgren/Alfa/}
		  }

@InProceedings{ranta98:regexp,
  author =       {A. Ranta},
  title =        {A Multilingual Natural-Language Interface to Regular Expressions},
  booktitle =    {Proceedings of the International Workshop on Finite State
                  Methods in Natural Language Processing},
  pages =        {79--90},
  year =         1998,
  editor =       {L. Karttunen and K. Oflazer},
  address =      {Ankara},
  organization = {Bilkent University}
}

@Misc{maple-homepage,
  author =	 {Waterloo Maple Inc.},
  title =	 {{Maple Homepage}},
  howpublished = {\verb!http://www.maplesof.com/!},
  documentURL = "http://www.maplesof.com/",
  year =	 2000
}

@Misc{mathematica-homepage,
  author =	 {Wolfram Research, Inc.},
  title =	 {{Mathematica Homepage}},
  howpublished = {\verb!http://www.wolfram.com/products/mathematica/!},
  documentURL = "http://www.wolfram.com/products/mathematica/",
  year =	 2000
}

@Misc{coq-homepage,
  author =	 {Coq Development Team},
  title =	 {{Coq Homepage}},
  howpublished = {\verb!http://pauillac.inria.fr/coq/!},
  documentURL = "http://pauillac.inria.fr/coq/",
  year =	 1999
}

@TechReport{LEGO-homepage,
  author =	 {Z. Luo and R. Pollack},
  title =	 {{LEGO Proof Development System}},
  institution =  {University of {Edinburgh}},
  year =	 1992
}

@Misc{LEGO-new-homepage,
  author =	 {D. Aspinall},
  title =	 {{The LEGO Proof Assistant}},
  howpublished = {\verb!http://www.dcs.ed.ac.uk/home/lego/!},
  documentURL = "http://www.dcs.ed.ac.uk/home/lego/",
  year =	 1999
}

@Misc{Isabelle-homepage,
  author =	 {Isabelle},
  title =	 {{Isabelle Homepage}},
  howpublished = {\verb!http://www.cl.cam.ac.uk/Research/HVG/Isabelle/!},
  documentURL = "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html",
  year =	 2000
}

@TechReport{lesk-lex,
  author = {M. E. Lesk},
  title  = {Lex --- a lexical analyzer generator},
  year   = {1975},
  institution	= {{Bell Laboratories, Murray Hill, N.J.}},
  type		= {Technical Report},
  number	= {39}
}

@Misc{Mizar-homepage,
  author =	 {},
  title =	 {{The Mizar Homepage}},
  howpublished = {\verb!http://mizar.org/!},
  documentURL = "http://mizar.org/",
  year =	 1999
}

@Misc{ALF-family-homepage,
  author =	 {},
  title =	 {{Implementation of Proof Editors}},
  howpublished = 
   {\verb!http://www.cs.chalmers.se/ComputingScience/Research/Logic/!},
  documentURL = "http://www.cs.chalmers.se/ComputingScience/Research/Logic/",
  year =	 1999
}

@incollection{deBruijn:MV,
	 TITLE	= {{Mathematical Vernacular: 
                    a Language for Mathematics with Typed Sets}},
	 AUTHOR = {N. G. de Bruijn},
	 EDITOR = {R. Nederpelt},
	 BOOKTITLE	= {{Selected Papers on Automath}},
	 PUBLISHER = {North-Holland Publishing Company},
	 PAGES = {865--935},
	 YEAR = {1994}
 }

@article{pereira-warren,
         AUTHOR = "F. Pereira and D. Warren",
         TITLE  = "Definite Clause Grammars for Language Analysis",
         JOURNAL = {Artificial {Intelligence}},
         YEAR = {1980},
         NUMBER = {13},
         PAGES = {231--278}
 }

@PhdThesis{coscoy:thesis,
  author = 	 {Y.\ Coscoy},
  title = 	 {Explication textuelle de preuves pour le calcul des
                  constructions inductives},
  school = 	 {{Universit\'e de Nice-Sophia-Antipolis}},
  year = 	 2000
}


@InProceedings{coscoy:textproofs,
        AUTHOR = {Y. Coscoy and G. Kahn and L. Th\'ery},
        TITLE   = {Extracting Text from Proof}, 
        BOOKTITLE = {{Proceedings of the International Conference on Typed Lambda
                     Calculus and Applications (TLCA), Edinburgh}},
         EDITOR = {M. Dezani and G. Plotkin},
         SERIES = {Lecture Notes in Computer Science},
         NUMBER = {902},
         PUBLISHER = {Springer-Verlag},
         YEAR = {1996}
 }

@InProceedings{coscoy:explanation,
  author =       {Y. Coscoy},
  title =        {A natural language explanation of formal proofs},
  booktitle =    {Logical Aspects of Computational Linguistics},
  pages =        {149--167},
  year =         1997,
  editor =       {C. {Retor\'e}},
  address =      {Heidelberg},
  publisher =    {Springer},
  series =       {Lecture Notes in Artificial Intelligence},
  number=        1328
}

@inproceedings{ranta:torino,
        AUTHOR = {A. Ranta},
        TITLE   = {Context-Relative Syntactic Categories 
   and the Formalization of Mathematical Text}, 
        BOOKTITLE = {{Types For Proofs and Programs}},
         EDITOR = {S. Berardi and M. Coppo},
         SERIES = {Lecture Notes in Computer Science},
         NUMBER = {1158},
         PAGES = {231--248},
         PUBLISHER = {Springer-Verlag},
         YEAR = {1996}
 }

@article{ranta:paris,
         AUTHOR = {A. Ranta},
         TITLE  = {{Structures grammaticales dans le fran\c{c}ais math\'ematique}},
         JOURNAL = {{Math\'ematiques, informatique et Sciences Humaines}},
         YEAR = {1997},
         NUMBER = {138, 139},
         PAGES = {5--56, 5--36}
 }

@article{kamp:drt,
         AUTHOR = {H. Kamp},
         TITLE  = {{ A theory of truth and semantic representation}},
         EDITOR = {{J. Groenendijk, T. Janssen, and M. Stokhof}},
         BOOKTITLE = {{Formal Methods in the Study of Language, Part 1}},
         YEAR = {1981},
         PUBLISHER = {{Mathematisch Centrum, Amsterdam}},
         PAGES = {277--322}
 }


@PhdThesis{magnusson:phd,
  author = 	 {L. Magnusson},
  title = 	 {The Implementation of ALF - a Proof Editor based on 
                  Martin-L\"of's Monomorphic Type Theory with Explicit
                  Substitution},
  school = 	 {Department of Computing Science, Chalmers University of
                  Technology and University of G\"oteborg},
  year = 	 {1994}
}

@InProceedings{krijo-aarne,
  author =       "K. Johannisson and A. Ranta",
  title =        "Formal Verification of Multilingual Instructions",
  booktitle =    "The Joint Winter Meeting of Computing Science and
                  Computer Engineering",
  publisher =    "Chalmers University of Technology",
  year =         "2001"
}



















@Manual{JavaCollection,
  title = 	 {The Java Collection Framework}, 
  year =	 {1995--1999},
  author = {{Sun Microsystems Inc.}},
  note = {\texttt{http://java.sun.com/j2se/1.3/docs/guide/collections/}}
  }

@Book{BarstowSandewall,
  author = {Barstow, D.~R., Shrobe, H.~E., and Sandewall, E.},
  title = {Interactive Programming Environments},
  publisher = {McGraw Hill},
  year = 1984
}


@inproceedings{HuetKahn1975,
  author = "V. Donzeau-Gouge and G. Huet and G. Kahn and B. Lang and J.~J. Levy",
  title  = {A structure-oriented program editor: 
            a first step towards computer assisted programming},
  booktitle = {{International Computing Symposium ({ICS'75})}},
  year = {1975}
}



@inproceedings{hughes:type-spec,
                  author={John Hughes},
                  title={Type Specialisation for the Lambda-calculus; or, A
                  New Paradigm for Partial Evaluation based on Type
                  Inference},
                  booktitle={Partial Evaluation},
                  editor={Olivier Danvy and Robert Gl\"uck and Peter Thiemann},
                  publisher={Springer-Verlag},
                  series={LNCS}, 
                  volume={1110},
                  year={1996},
                  month=feb
}

@inproceedings{dussart-hughes-thiemann:icfp97,
                  author={Dirk Dussart and John Hughes and Peter Thiemann},
                  title={Type Specialisation for Imperative Languages},
                  booktitle={Int. Conference on Functional Programming},
                  publisher={ACM Press},
                  month=jun,
                  year={1997}
}

@inproceedings{heldal-hughes:pepm97,
                  author={Rogardt Heldal and John Hughes},
                  title={Partial Evaluation and Separate Compilation},
                  booktitle={Symposium on Partial Evaluation and
                             Semantics-Based Program Manipulation},
                  publisher={ACM SIGPLAN},
                  month=jun,
                  year={1997}
}

@inproceedings{dussart-heldal-hughes:pldi97,
                  author={Dirk Dussart and Rogardt Heldal and John Hughes},
                  title={Module-Sensitive Program Specialisation},
                  booktitle={Conference on Programming Language Design and 
                             Implementation},
                  publisher={ACM SIGPLAN},
                  month=jun,
                  year={1997}
}

@Article{heldal:00:ExtendingPEseparateCompilation,
  author =       {Rogardt Heldal and John Hughes},
  title =        {Extending a partial evaluator which supports separate compilation},
  journal =      {Theoretical Computer Science},
  volume =  {248},
  year =         {2000},
  pages =        {99--145}
}

@Book{Sommerville01,
  author =       "Ian Sommerville",
  title =        "Software Engineering",
  publisher =    "Addison-Wesley",
  year =         "2001",
  edition =      "6th"
}

@inproceedings{hughes:type-spec-surveys,
  author = {John Hughes},
  title = {Type Specialisation},
  booktitle =        {Symposium on Partial Evaluation},
  year =         1998,
  editor =       {Danvy, Olivier and Gl{\"u}ck, Robert and Thiemann, Peter},
  volume =       30,
  number =       5,
  series =       {Computing Surveys},
  month =        sep
  }

@inproceedings{hughes:typespec-tutorial,
  author = {John Hughes},
  title = {A Type Specialisation Tutorial},
  booktitle = {{DIKU} Summer School on Partial Evaluation},
  year = {1998}
}

@inproceedings{hughes:typespec-correctness,
  author={John Hughes},
  title={The Correctness of Type Specialisation},
  booktitle={European Symposium on Programming},
  editor={Gert Smolka},
  publisher={Springer-Verlag},
  series={Lecture Notes in Computer Science},
  year={2000}
}

@inproceedings{heldal:poly-bta,
  author = {Rogardt Heldal and John Hughes},
  title = {Binding-time Analysis for Polymorphic Types},
  booktitle = {Andrei Ershov Fourth International Conference on Perspectives of System Informatics},
  month = jul,
  year={2001},
  editor={Dines Bjorner and  Manfred Broy and Alexandre Zamulin}
}

@InProceedings{HoltEwan99,
  author = 	 {Alexander Holt and Ewan Klein},
  title = 	 {A semantically-derived subset of {E}nglish for 
                  hardware verification},
  booktitle = 	 {Proc.\ 37th Annual Meeting of the Association for 
                  Computational Linguistics: Maryland, USA},
  pages =	 {451-456},
  year =	 {1999},
  publisher =	 {Association for Computational Linguistics},
  url = {\texttt{http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-sds/ps/}}
}

@InProceedings{HKG99,
  author = 	 {Alexander Holt and Ewan Klein and Claire Grover},
  title = 	 {Natural language for hardware verification: 
                  semantic interpretation and model checking},
  booktitle = 	 {Proc.\ ICoS-1: Inference in Computational Semantics, Amsterdam},
  pages =	 {133-137},
  year =	 {1999},
  publisher =	 {Institute for Logic, Language and Computation, 
                  University of Amsterdam},
  url = {http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-nlh/ps/}
}

@Article{Holt99,
  author = 	 {Alexander Holt},
  title = 	 {Formal verification with natural language specifications: 
                  guidelines, experiments and lessons so far},
  journal = 	 {South African Computer Journal},
  year = 	 {1999},
  volume =	 {24},
  pages =	 {253-257},
  month =	 nov,
  url =          {http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-fvn/ps/},
}

@Book{Harrison98,
  author =	 {John Harrison},
  title = 	 {Theorem Proving with the Real Numbers},
  publisher = 	 spv,
  year = 	 {1998},
  series =	 {Distinguished Dissertations},
  note =	 {Revised version of PhD Thesis, Cambridge/UK, 1996},
  isbn_issn =    {3-540-76256-6}
}

@PhdThesis{deNivelle95,
  author = 	 {de Nivelle, Hans},
  title = 	 {Ordering Refinements of Resolution},
  school = 	 {Technical University Delft},
  year = 	 {1995},
  month =        oct,
  url =          {http://www.mpi-sb.mpg.de/~nivelle/documents/proefschrift.ps.gz}
}

@InProceedings{HaehnleRanta01a,
  author = 	 {R.\ H\"{a}hnle and A.\ Ranta},
  title = 	 {Connecting {OCL} with the Rest of the World},
  booktitle = 	 {{ETAPS}/{WTUML},
                  {Genova}, {Italy}},
  year =	 {2001},
  editor =	 {J. Whittle},
  url =          {http://www.cs.chalmers.se/~reiner/papers/wtuml.ps.gz}
}

@Article{BBEHO99,
  author =       "Michael Baentsch and Peter Buhler and Thomas Eirich
                 and Frank H{\"o}ring and Marcus Oestreicher",
  title =        "{JavaCard} --- From Hype to Reality",
  journal =      "IEEE Concurrency",
  volume =       "7",
  number =       "4",
  pages =        "36--43",
  month =        oct # "\slash " # dec,
  year =         "1999",
  url =          "http://www.zurich.ibm.com/technologies/jetz/p4baenCPYRT.lo.pdf"
}

@InProceedings{GogollaRichters98a,
  author =       "Martin Gogolla and Mark Richters",
  title =        "On Constraints and Queries in {UML}",
  pages =        "109--121",
  booktitle =    "The Unified Modeling Language -- Technical Aspects and
                  Applications",
  editor =       "Martin Schader and Axel Korthaus",
  publisher =    "Physica-Verlag, Heidelberg",
  year =         "1998"
}

@InProceedings{HHK98,
  author =       "Ali Hamie and John Howse and Stuart Kent",
  title =        "Interpreting the {Object Constraint Language}",
  booktitle =    "Proceedings 5th Asia Pacific Software Engineering
                  Conference (APSEC '98), Taipei,
                  Taiwan",
  year =         "1998",
  publisher =    "IEEE Computer Society"
}

@Book{HKT00,
  author =	 {David Harel and Dexter Kozen and Jerzy Tiuryn},
  title = 	 {Dynamic Logic},
  publisher = 	 {MIT Press},
  year = 	 2000,
  series =	 {Foundations of Computing},
  month =	 oct,
  isbn_issn =    {0-262-08289-6}
}

@Book{MichalewiczFogel00,
  author =	 {Z. Michalewicz and B. F. Fogel},
  title = 	 {How to solve it: modern heuristics},
  publisher = 	 spv,
  year = 	 {2000},
  isbn_issn =    {3-540-66061-5}
}

@Book{Schumann00,
  author =	 {Johann M. P. Schumann},
  title = 	 {Automated Theorem Proving in Software Engineering},
  publisher = 	 spv,
  year = 	 {2000},
  isbn_issn =    {3-540-67989-8}
}

@Book{HMNS00,
  author =	 {U. Hansmann and L. Merk and M. S. Nicklous and T. Stober},
  title = 	 {Pervasive Computing Handbook},
  publisher = 	 spv,
  year = 	 {2000},
  isbn_issn =    {3-540-67122-6}
}

@Book{Newborn00,
  author =	 {M. Newborn},
  title = 	 {Automated Theorem Proving: Theory and Practice},
  publisher = 	 spv,
  year = 	 {2000},
  isbn_issn =    {3-387-95075-3}
}

@Book{TymoczkoHenle00,
  author =	 {T. Tymoczko and J. Henle},
  title = 	 {Sweet Reason: A Field Guide to Modern Logic},
  publisher = 	 spv,
  year = 	 {2000},
  isbn_issn =    {3-387-98930-7}
}

@Book{HMT99,
  editor =	 {Hatcliff, J. and Mogensen, T. and Thiemann, P.},
  title = 	 {Partial Evaluation. Practice and Theory. 
                  DIKU 1998 International Summer School, Copenhagen, Denmark},
  publisher = 	 spv,
  year = 	 {1999},
  volume =	 {1706},
  series =	 lncs,
  isbn_issn =    {3-540-66710-5}
}

@inproceedings{Giese00,
   author = {Martin Giese},
   title  = {Proof Search without Backtracking using Instance Streams, Position Paper},
   booktitle = {Proc.\ Int.\ Workshop on First-Order Theorem Proving, St.\ Andrews, Scotland},
   year = {2000},
   pages = {227--228},
   editor = {Peter Baumgartner and Hantao Zhang},
   series = {Fachberichte Informatik 5/2000},
   publisher = {University of Koblenz, Institute for Computer Science},
   note = {\href{http://i12www.ira.uka.de/~key/doc/2000/giese00.ps.gz}{\texttt{http://i12www.ira.uka.de/\~{}key/doc/2000/giese00.ps.gz}}}
}

@article{Smullyan63,
   AUTHOR = {Smullyan, Raymond M.},
    TITLE = {A unifying principle in quantification theory},
  JOURNAL = {Proceedings of the National Academy of Sciences of the U.S.A.},
   VOLUME = {49},
   number = {6},
     YEAR = {1963},
    PAGES = {828--832}
}

@InProceedings{BaarHaehnle00a,
  author = 	 {Thomas Baar and Reiner H\"ahnle},
  title = 	 {An Integrated Metamodel for {OCL} Types},
  booktitle = 	 {Proc.\ OOPSLA 2000 Workshop Refactoring the UML:  
                  In Search of the Core, Minneapolis/MI, USA},
  year =	 {2000},
  editor =	 {Robert France and Bernhard Rumpe and Jonathan Whittle},
  month =	 oct
}

@InCollection{RSBMZ98,
  author = 	 {Dirk Riehle and Wolf Siberski and Dirk B\"{a}umer and
                  Daniel Megert and Heinz Z\"{u}llighoven.},
  title = 	 {Serializer},
  booktitle = 	 {Pattern Languages of Program Design 3},
  pages =	 {293--312},
  publisher =	 {Addison-Wesley},
  year =	 {1998},
  editor =	 {Robert Martin and Dirk Riehle and and Frank Buschmann},
  chapter =	 {17},
  url =          {http://www.riehle.org/papers/1996/plop-1996-serializer.pdf}
}

@InProceedings{CIOH00,
  author = 	 {Cristiano Calcagno and Samin Ishtiaq and Peter W. O'Hearn},
  title = 	 {Semantic Analysis of Pointer Aliasing, Allocation and 
                  Disposal in {H}oare Logic},
  booktitle = 	 {Proc.\ 2nd International Conference on Principles
                  and Practice of Declarative Programming, Montral, Canada},
  year =	 {2000},
  editor =	 {Maurizio Gabbrielli and Frank Pfenning},
  series =	 lncs,
  publisher =	 spv,
  url =          {http://www.dcs.qmw.ac.uk/~ccris/ftp/ppdp00.ps}
}

@Book{PalanquePaterno98,
  editor    = {P. Palanque and F. Patern\`{o}},
  title     = {{Formal Methods in Human-Computer Interaction}},
  publisher = spv,
  series    = {{FACIT}},
  year      = {{1998}}
}

@Book{VanDerLinden99a,
  author =       "Peter {van der Linden}",
  title =        "Just {Java} 1.2",
  publisher =    "Prentice-Hall",
  edition =      "Fourth",
  month =        mar,
  year =         "1999",
  ISBN_ISSN =         "0-13-010534-1",
  series =       "SunSoft Press Java series"
}

@Book{VanDerLinden99b,
  author =       "Peter {van der Linden}",
  title =        "Not Just {Java}: a technology briefing",
  publisher =    "Prentice-Hall",
  edition =      "Second",
  year =         "1999",
  ISBN_ISSN =         "0-13-079660-3",
  series =       "SunSoft Press Java series"
}

Book{GoldbergRubin95,
  author =       "Adele Goldberg and Kenneth S. Rubin",
  title =        "Succeeding With Objects: Decision Frameworks for
                 Project Management",
  publisher =    "Addison-Wesley",
  year =         "1995",
  ISBN_ISSN =         "0-201-62878-3"
}

@Book{Goldberg84,
  author =       "Adele Goldberg",
  title =        "Smalltalk-80: the Interactive Programming
                 Environment",
  publisher =    "Addison-Wesley",
  year =         "1984",
  ISBN_ISSN =         "0-201-11372-4"
}

@Book{GoldbergRobson83,
  author =       "Adele Goldberg and David Robson",
  title =        "Smalltalk-80: The Language and its Implementation",
  publisher =    "Addison-Wesley",
  year =         "1983"
}  

@TechReport{Habermalz00,
  author = {Elmar Habermalz},
  title  = {Interactive Theorem Proving with Schematic Theory Specific Rules},
  note   = {URL: \texttt{http://i12www.ira.uka.de/\~{}key/doc/2000/stsr.ps.gz}},
  year   = {2000},
  institution	= {Fakult\"{a}t f\"{u}r Informatik, Universit\"{a}t Karlsruhe},
  type		= {Technical Report},
  number	= {19/00}
}

@inproceedings{Rumpe98a,
        author = {Bernhard Rumpe},
        title = {A Note on Semantics (with an Emphasis on {UML})},
        booktitle = {Proc.\ Second ECOOP Workshop on Precise Behavioral Semantics},
        year = {1998},
        publisher = {Institut f\"{u}r {I}nformatik, 
                     Technische Universit\"{a}t M\"{u}nchen},
        number = {TUM-I9813},
        editor = {Haim Kilov and  Bernhard Rumpe},
        url = {www4.informatik.tu-muenchen.de/papers/RUM98a.html}
}

@TechReport{IOT00,
  author = 	 {Luisa Iturrioz and Ewa Or{\l{}}owska and Esko Turunen},
  title = 	 {{\em (eds.).} Atlas of many-valued structures},
  institution =  {Tampere University of Technology, 
                  Department of Information Technology},
  year = 	 {2000},
  type =	 {Mathematics Report},
  number =	 {75},
  address =	 {Tampere, Finland},
  isbn_issn =    {952-150-386-6}
}

@article {EGHN00,
   AUTHOR = {Esteva, Francesc and Godo, Llu{\'\i}s and H{\'a}jek, Petr and
             Navara, Mirko},
    TITLE = {Residuated fuzzy logics with an involutive negation},
  JOURNAL = {Archive for Mathematical Logic},
   VOLUME = {39},
     YEAR = {2000},
   NUMBER = {2},
    PAGES = {103--124}
}

@InProceedings{MultilevelCell95,
  author = 	 {Bauer, M. and Alexis, R. and Atwood, G. and Baltar, B. and
                  Fazio, A. and Frary, K.  and Hensel, M. and Ishac, M. and
                  Javanifard, J. and Landgraf, M. and Leak, D. and Loe, K.
                  and Mills, D. and Ruby, P. and Rozman, R. and Sweha, S.
                  and Talreja, S. and Wojciechowski, K.},
  title = 	 {A multilevel-cell 32 {M}b flash memory},
  booktitle = 	 {41st Solid-State Circuits Conference, ISSCC. 
                  Digest of Technical Papers},
  pages =	 {132--133, 351},
  year =	 {1995},
  month =	 feb,
  publisher =	 {IEEE CS Press}
}

@Article{CMA00,
  author = 	 {Walter A. Carnielli and Jo{\~{a}}o Marcos and Sandra de Amo},
  title = 	 {Formal inconsistency and evolutionary databases},
  journal = 	 {Logic and Logical Philosophy},
  year = 	 {to appear, 2000}
}

@article {KlawonnKruse94,
   AUTHOR = {Klawonn, Frank and Kruse, Rudolf},
    TITLE = {A {{\L{}}}ukasiewicz logic based {P}rolog},
  JOURNAL = {Mathware \& Soft Computing},
   VOLUME = {1},
     YEAR = {1994},
   NUMBER = {1},
    PAGES = {5--29}
}

@article {Dyckhoff99,
   AUTHOR = {Dyckhoff, Roy},
    TITLE = {A deterministic terminating sequent calculus for
             {G}\"{o}del-{D}ummett logic},
  JOURNAL = {Logic Journal of the IGPL},
   VOLUME = {7},
     YEAR = {1999},
   NUMBER = {3},
    PAGES = {319--326}
}

@article {Avron91b,
   AUTHOR = {Avron, Arnon},
    TITLE = {Hypersequents, logical consequence and intermediate logics for
             concurrency},
  JOURNAL = {Annals of Mathematics and Artificial Intelligence},
   VOLUME = {4},
     YEAR = {1991},
   NUMBER = {3--4},
    PAGES = {225--248}
}

@incollection {Avron96a,
   AUTHOR = {Avron, Arnon},
    TITLE = {The method of hypersequents in the proof theory of
             propositional non-classical logics},
BOOKTITLE = {Logic: from foundations to applications. Proc. 
             Logic Colloquium, Keele, UK, 1993},
    PAGES = {1--32},
PUBLISHER = {Oxford University Press},
  ADDRESS = {New York},
     YEAR = {1996},
   EDITOR = {Hodges, Wilfrid and Hyland, Martin and Steinhorn, Charles and
             Truss, John},
ISBN_ISSN = {0-19-853862-6}
}

@article {Belnap82,
   AUTHOR = {Belnap, Jr., Nuel D.},
    TITLE = {Display logic},
  JOURNAL = {Journal of Philosophical Logic},
   VOLUME = {11},
     YEAR = {1982},
   NUMBER = {4},
    PAGES = {375--417}
}

@article {AFM99,
   AUTHOR = {Avellone, Alessandro and Ferrari, Mauro and Miglioli,
             Pierangelo},
    TITLE = {Duplication-free tableau calculi and related cut-free sequent
             calculi for the interpolable propositional intermediate logics},
  JOURNAL = {Logic Journal of the IGPL},
   VOLUME = {7},
     YEAR = {1999},
   NUMBER = {4},
    PAGES = {447--480}
}

@article{BlokPigozzi89,
   AUTHOR = {Blok, W. J. and Pigozzi, Don},
    TITLE = {Algebraizable logics},
  JOURNAL = {Memoirs of the American Mathematical Society},
   VOLUME = {77},
     YEAR = {1989},
   NUMBER = {396},
    PAGES = {vi+78}
}

@article{BlokPigozzi00,
   AUTHOR = {Blok, W. J. and Pigozzi, Don},
    TITLE = {Abstract algebraic logic and the deduction theorem},
  JOURNAL = {Bulletin of Symbolic Logic},
     YEAR = {to appear, 2000}
}

@article{SetteCarnielli95,
   AUTHOR = {Sette, Antonio Mario and Carnielli, Walter A.},
    TITLE = {Maximal weakly-intuitionistic logics},
  JOURNAL = {Studia Logica},
   VOLUME = {55},
     YEAR = {1995},
   NUMBER = {1},
    PAGES = {181--203}
}

@article{CarnielliConiglio99,
   AUTHOR = {Carnielli, Walter A. and Marcelo E. Coniglio},
    TITLE = {A categorial approach to the combination of logics},
  JOURNAL = {Manuscrito---Revista Internacional de Filosofia},
   VOLUME = {XXII},
     YEAR = {1999},
   NUMBER = {2},
    MONTH = oct,
    PAGES = {69--94}
}

@article{Sette73,
   AUTHOR = {Sette, Antonio Mario},
    TITLE = {On the propositional calculus $P^1$},
  JOURNAL = {Mathematica Japonicae},
   VOLUME = {18},
     YEAR = {1973},
    PAGES = {173--180}
}

@Book{Chen00,
  author =	 {Zhiqun Chen},
  title = 	 {Java Card Technology for Smart Cards: 
                  Architecture and Programmer's Guide},
  publisher = 	 {Addison-Wesley},
  year = 	 {2000},
  series =	 {Java Series},
  month =	 jun,
  isbn_issn =    {0-201-70329-7},
  location =     {D.3 Chen}
}

@Book{BollellaGosling00a,
  author =	 {Greg Bollella and James Gosling and Benjamin Brosgol 
                  and Peter Dibble and Steve Furr and Mark Turnbull},
  title = 	 {The Real-Time Specification for Java},
  publisher = 	 {Addison-Wesley},
  year = 	 {2000},
  series =	 {Java Series},
  month =	 jun,
  isbn_issn =    {0-201-70323-8},
  url =          {http://www.javaseries.com/rtj.pdf},
  note =         {URL: \texttt{www.javaseries.com/rtj.pdf}}
}

@Article{BollellaGosling00b,
  author =	 {Greg Bollella and James Gosling},
  title = 	 {The Real-Time Specification for Java},
  year = 	 {2000},
  month =	 jun,
  journal =      {IEEE Computer},
  pages =        {47--54}
}

@TechReport{HJVB00,
  title =        "A Case Study in Class Library Verification: {Java's}
                  Vector Class",
  author =       "Marieke Huisman and Bart Jacobs and Joachim {van den Berg}",
  year =         "2000",
  institution =  "Computing Science Department, Nijmegen",
  number =       "CSI-R0007",
  type =         "CSI Report",
  url =          "http://www.cs.kun.nl/csi//reports/full/CSI-R0007.ps.Z",
  note =         "URL: \texttt{www.cs.kun.nl/csi//reports/full/CSI-R0007.ps.Z}",
  month =        mar
}

@InProceedings{PVBJ00a,
  title =        "Specification of the {JavaCard} {API} in {JML}",
  author =       "Erik Poll and Joachim {van den Berg} and Bart Jacobs",
  year =         "2000",
  booktitle =    "Fourth Smart Card Research and 
                  Advanced Application Conference (IFIP Cardis)",
  publisher =    "Kluwer Academic Publishers"
}

@InProceedings{GutheryPosegga00a,
  title =        "How to Turn a {GSM} {SIM} into a Web Sever",
  author =       "Joachim Posegga and Scott Guthery",
  year =         "to appear, 2000",
  booktitle =    "Fourth Smart Card Research and 
                  Advanced Application Conference (IFIP Cardis)",
  publisher =    "Kluwer Academic Publishers"
}

@TechReport{PVBJ00b,
  title =        "Specification of the {JavaCard} {API} in {JML}",
  author =       "Erik Poll and Joachim {van den Berg} and Bart Jacobs",
  year =         "2000",
  institution =  "Computing Science Department, Nijmegen",
  number =       "CSI-R0005",
  type =         "CSI Report",
  url =          "http://www.cs.kun.nl/csi//reports/full/CSI-R0005.ps.Z",
  note =         "URL: \texttt{www.cs.kun.nl/csi//reports/full/CSI-R0005.ps.Z}",
  month =        mar
}

@TechReport{LBR00,
  author =       "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  title =        "Preliminary Design of {JML}: A Behavioral Interface
                 Specification Language for {Java}",
  institution =  "Iowa State University, Department of Computer
                 Science",
  year =         "2000",
  number =       "98-06i",
  month =        feb,
  note =         "URL: \texttt{ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz}",
  url =          "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz"
}

@InCollection{LBR99,
  author =       "Gary T. Leavens and Albert L. Baker and Clyde Ruby",
  title =        "{JML}: A Notation for Detailed Design",
  booktitle =    "Behavioral Specifications of Businesses and Systems",
  editor =       "Haim Kilov and Bernhard Rumpe and Ian Simmonds",
  year =         "1999",
  publisher =    "Kluwer Academic Publishers",
  pages =        "175--188",
  note =         "URL: \texttt{ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmlkluwer.ps.gz}",
  url =          "ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmlkluwer.ps.gz"
}

@TechReport{LeinoStata97,
  author = 	 {K. Rustan M. Leino and Raymie Stata},
  title = 	 {Checking Object Invariants},
  institution =  {Digital Systems Research Center},
  year = 	 {1997},
  type =	 {Technical Note},
  number =	 {\#1997-007},
  address =	 {Palo Alto, USA},
  month =	 jan,
  note =         "URL: \texttt{ftp://ftp.digital.com/pub/DEC/SRC/technical-notes/SRC-1997-007.ps.gz}",
  url =          {ftp://ftp.digital.com/pub/DEC/SRC/technical-notes/SRC-1997-007.ps.gz}
}

@TechReport{DLNS98,
  author = 	 {David L. Detlefs and K. Rustan M. Leino and
                  Greg Nelson and James B. Saxe},
  title = 	 {Extended Static Checking},
  institution =  {Compaq Systems Research Center},
  year = 	 {1998},
  type =	 {Research Report},
  number =	 {\#159},
  address =	 {Palo Alto, USA},
  month =	 dec,
  note =         "URL: \texttt{ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-159.ps.gz}",
  url =          {ftp://ftp.digital.com/pub/DEC/SRC/research-reports/SRC-159.ps.gz}
}

@TechReport{LSS99,
  author = 	 {K. Rustan M. Leino and James B. Saxe and Raymie Stata},
  title = 	 {Checking {J}ava programs via guarded commands},
  institution =  {Compaq Systems Research Center},
  year = 	 {1999},
  type =	 {Technical Note},
  number =	 {\#1999-002},
  address =	 {Palo Alto, USA},
  month =	 may,
  note =         "URL: \texttt{ftp://ftp.digital.com/pub/DEC/SRC/technical-notes/SRC-1999-002.ps.gz}",
  url =          {ftp://ftp.digital.com/pub/DEC/SRC/technical-notes/SRC-1999-002.ps.gz}
}

@Book{Gabbay99a,
  author =       "Dov M. Gabbay",
  title =        "Fibring Logics",
  series       = "Oxford Logic Guides",
  volume =       "38",
  publisher =    "Oxford University Press",
  year =         "1999"
}

@Article{BachmairGanzinger98,
  author =       "Leo Bachmair and Harald Ganzinger",
  title =        "Ordered chaining calculi for first-order theories of
                 transitive relations",
  journal =      jacm,
  volume =       "45",
  number =       "6",
  pages =        "1007--1049",
  month =        nov,
  year =         "1998"
}

@Book{KulakGuiney00,
  author =	 {Daryl Kulak and Eamonn Guiney},
  title = 	 {Use Cases: Requirements in Context},
  publisher = 	 {Addison-Wesley},
  year = 	 {2000},
  month =	 may,
  isbn_issn =    {0-201-65767-8}
}

@PhDThesis{Williams00a,
  author = 	 {Laurie Williams},
  title = 	 {The Collaborative Software Process},
  year = 	 {2000},
  school =       {University of Utah Graduate School},
  url       = 	 {http://www.cs.utah.edu/\~{}lwilliam/Papers/dissertation.pdf}
}

@Article{WKCJ00,
  author = 	 {Laurie Williams and Robert R. Kessler and 
                  Ward Cunningham and Ron Jeffries},
  title = 	 {Strengthening the Case for Pair Programming},
  journal = 	 {IEEE Software},
  year = 	 {2000},
  volume =	 {17},
  number =	 {3},
  pages =	 {??--??},
  month =	 {July/August},
  url       = 	 {http://www.cs.utah.edu/\~{}lwilliam/Papers/ieeeSoftware.PDF}
}

@Article{Wegener99,
  author = 	 {Hans Wegener},
  title = 	 {Extreme {A}nsichten},
  journal = 	 {iX},
  year = 	 {1999},
  pages =	 {126--130},
  month =	 dec
}

@Article{WilliamsKessler00,
  author = 	 {Laurie Williams and Robert R. Kessler},
  title = 	 {All I really need to know about Pair Programming I
                  learned in Kindergarten},
  journal = 	 cacm,
  year = 	 {to appear, 2000},
  url       = 	 {http://www.cs.utah.edu/\~{}lwilliam/Papers/Kindergarten.PDF}
}

@Article{ABV00,
  author =       "Roger T. Alexander and James M. Bieman and John
                 Viega",
  title =        "Coping with {Java} Programming Stress",
  journal =      "IEEE Computer",
  volume =       "33",
  number =       "4",
  pages =        "30--38",
  month =        apr,
  year =         "2000"

}

@Unpublished{Jackson00a,
  author = 	 {Daniel Jackson},
  title = 	 {Alloy: A Lightweight Object Modelling Notation},
  institution =  {MIT Lab for Computer Science},
  year = 	 {2000},
  month =	 jul,
  note =	 {URL: 
           \texttt{http://sdg.lcs.mit.edu/\~{}dnj/pubs/alloy-journal.pdf}}
}

@Unpublished{Jackson99a,
  author = 	 {Daniel Jackson},
  title = 	 {A Comparison of Object Modelling Notations: 
                  {A}lloy, {UML} and {Z}},
  note = 	 {URL: 
           \texttt{http://sdg.lcs.mit.edu/\~{}dnj/pubs/alloy-comparison.ps}},
  month =	 aug,
  year =	 {1999}
}

@Unpublished{VasiriJackson99,
  author = 	 {Mandana Vaziri and Daniel Jackson},
  title = 	 {Some Shortcomings of {OCL}, the {O}bject 
                  {C}onstraint {L}anguage of {UML}},
  note = 	 {Response to {O}bject {M}anagement {G}roup's 
                  Request for Information on {UML} 2.0,
                  URL: \texttt{http://sdg.lcs.mit.edu/\~{}dnj/pubs/omg.ps}},
  month =	 dec,
  year =	 {1999}
}

@InProceedings{JSS00,
  author = 	 {Daniel Jackson and Ian Schechter and Ilya Shlyakhter},
  title = 	 {Alcoa: the {A}lloy Constraint Analyzer.},
  booktitle = 	 {Proc. International Conference on Software Engineering, 
                  Limerick, Ireland},
  year =	 {to appear, 2000},
  publisher =	 {IEEE CS Press, Los Alamitos},
  note =	 {URL: \texttt{http://sdg.lcs.mit.edu/\~{}dnj/pubs/alcoa-overview.pdf}}
}

@INPROCEEDINGS{BejarManya00a,
	AUTHOR	= {R. B\'{e}jar and F. Many\`{a}},
	BOOKTITLE= {Proc.\ 17th National Conference on  
                    Artificial Intelligence, AAAI-2000, Austin, USA},
	TITLE= {Solving the Round Robin Problem Using Propositional Logic},
	PAGES={--},
	YEAR= {2000}
}

@Manual{CC2.0,
  title = 	 {Common Criteria for Information Technology 
                  Security Evaluation},
  key =		 {Common Criteria},
  organization = {ISO/IEC Standard 15408},
  edition =	 {version 2.0},
  month =	 nov,
  year =	 {1998},
  note =	 {URL: \texttt{http://www.bsi.de/literat/doc/cc-pdf.zip}}
}

@InCollection{KozenTiuryn90,
  author =       "Dexter Kozen and Jerzy Tiuryn",
  booktitle =    "Handbook of Theoretical Computer Science",
  title =        "Logics of Programs",
  chapter =      "14",
  publisher =    "The MIT Press",
  year =         "1990",
  editor =       "Jan van Leeuwen",
  pages =        "789--840",
  volume =       "B: Formal Models and Semantics"
}

@InProceedings{Hussmann99,
  author =       "Heinrich Hu{\ss{}}mann",
  title = 	 {Formale {B}eschreibungstechniken und praktische 
                  {S}oftwaretechnik --- eine ungl\"{u}ckliche {V}erbindung?},
  booktitle = 	 {Formale Beschreibungstechniken'99, 
                  9.~GI/ITG-Fachgespr\"{a}ch, M\"{u}nchen},
  pages =	 {1--6},
  year =	 {1999},
  editor =	 {K. Spies},
  publisher =	 {Herbert Utz Verlag},
  note =	 {URL: \texttt{www.inf.tu-dresden.de/TU/Informatik/ST2/ST/papers/fbt99.pdf}}
}

@Book{DCC88,
  author =       "E. Downs and P. Clare and I. Coe",
  title =        "Structured systems analysis and design method",
  publisher =    "Prentice-Hall",
  edition =      "second",
  year =         "1992"
}

@Book{Hussmann97,
  author =       "Heinrich Hu{\ss{}}mann",
  title =        "Formal foundations for software engineering methods",
  volume =       "1322",
  publisher =    spv,
  year =         "1997",
  ISBN_ISSN =         "3-540-63613-7",
  series =       lncs
}

@Book{Jia00,
  author =	 {Xiaoping Jia},
  title = 	 {Object-Oriented Software Developing Using Java},
  publisher = 	 {Addison-Wesley},
  year = 	 {2000},
  isbn_issn =    {0-201-35084-X}
}

@Book{BrueggeDutoit00,
  author =	 {Bernd Bruegge and Allen H. Dutoit},
  title = 	 {Object-Oriented Software Engineering: 
                  Conquering Complex and Changing Systems},
  publisher = 	 {Prentice Hall, Upper Saddle River/NJ},
  year = 	 {2000},
  isbn_issn =    {0-13-489725-0}
}

@Book{Stevens00,
  author =	 {Perdita Stevens and Rob Pooley},
  title = 	 {Using UML Software Engineering with Objects and Components},
  publisher = 	 {Addison-Wesley},
  year = 	 {2000},
  series =	 {Object Techology Series},
  edition =	 {updated},
  isbn_issn =    {0-201-64860-1}
}

@Book{Cooper00},
  author =	 {James W. Cooper},
  title = 	 {Java design patterns: a tutorial},
  publisher = 	 {Addison-Wesley},
  year = 	 {2000},
  isbn_issn =    {0-201-48539-7}
}

@Book{Eliens00,
  author =	 {Anton Eli\"{e}ns},
  title = 	 {Principles of Object-Oriented Software Development},
  publisher = 	 {Addison-Wesley},
  year = 	 {2000},
  edition =	 {second},
  isbn_issn =    {0-201-39856-7}
}

@Book{Ranta01a,
  author =       {Sara Negri and Jan von Plato},
  title =        {Structural Proof Theory},
  publisher =    {Cambridge University Press},
  year =         {2001, to appear},
  note =         {Appendix C ``PESCA---A Proof Editor for Sequent Calculus'' 
                  by Aarne Ranta}
}

@Manual{Ranta00a,
  title =        {PESCA---A Proof Editor for Sequent Calculus},
  author =       {Aarne Ranta},
  organization = {Department of Computing Science, 
                  Chalmers University of Technology and University of Gothenburg},
  address =      {Gothenburg},
  month =        mar,
  year =         {2000},
  note =         {Program and documentation.
                  URL: \texttt{www.cs.chalmers.se\~{}aarne/pesca/}}
}

@InProceedings{MaenpaaRanta99,
  author = 	 {P. Mäenpää and A. Ranta},
  title = 	 {The type theory and type checker of {GF}},
  booktitle = 	 {{Colloquium on Principles, Logics, and Implementations of
                  High-Level Programming Languages, 
                  Workshop on Logical Frameworks and Meta-languages, 
                  Paris, France}},
  year =	 {1999}
}


@Article{Ranta88,
  author =       "Aarne Ranta",
  title = 	 {Propositions as games as types},
  journal = 	 {Synthese},
  year = 	 {1988},
  volume =	 {76},
  pages =	 {377--395}
}

@Article{Ranta91b,
  author =       "Aarne Ranta",
  title = 	 {Intuitionistic categorial grammar},
  journal = 	 {Linguistics and Philosophy},
  year = 	 {1991},
  volume =	 {14},
  pages =	 {203--239}
}

@Article{Ranta95c,
  author =       "Aarne Ranta",
  title = 	 {Type-theoretical interpretation and generalization 
                  of phrase structure grammar},
  journal = 	 {Bulletin of the IGPL},
  year = 	 {1995},
  volume =	 {3},
  pages =	 {319--342}
}

@Article{Ranta97a,
  author =       "Aarne Ranta",
  title = 	 {Structures grammaticales dans le fran\c{c}ais math\'{e}matique},
  journal = 	 {Math\'{e}matiques, informatique et Sciences Humaines},
  year = 	 {1997},
  volume =	 {138/139},
  pages =	 {5--56/5--36}
}

@InProceedings{Ranta94a,
  author =       "Aarne Ranta",
  title =        "Type Theory and the Informal Language of Mathematics",
  booktitle =    "Selected papers from TYPES'93: 
                  Int.\ Workshop on Types, Nijmegen, The Netherlands",
  series =       lncs,
  publisher =    spv,
  volume =       "806",
  pages =        "352--365",
  year =         "1994",
  editor =       "Hendrik Barendregt and Tobias Nipkow"
}

@InProceedings{Ranta96a,
  author =       "A. Ranta",
  title =        "Context-Relative Syntactic Categories and the
                 Formalization of Mathematical Text",
  booktitle =    "Selected papers from TYPES'95: Int.\ Workshop on Types for
                 Proofs and Programs, Trento, Italy",
  publisher =    spv,
  editor =       "S. Berardi and M. Coppo",
  series =       lncs,
  volume =       1158,
  pages  =       "231--248",
  year =         "1996"
}

@InProceedings{Ranta95a,
  author =       "Aarne Ranta",
  title =        "Syntactic Categories in the Language of Mathematics",
  series =       lncs,
  volume =       "996",
  pages =        "162--182",
  year =         "1995",
  publisher =    spv,
  booktitle =    "Selected papers from TYPES'94: 
                  Int.\ Workshop on Types for
                 Proofs and Programs, Bastad, Sweden",
  editor =       {Peter Dybjer and Bengt Nordstr\"{o}m and Jan Smith}
}

@Article{Ranta98a,
  author =       "Aarne Ranta",
  title =        "Syntactic Calculus with Dependent Types",
  journal =      "Journal of Logic, Language, and Information",
  year =         "1998",
  volume =       "7",
  number =       "4",
  pages =        "413--431"
}

@InCollection{Ranta98b,
  author =       "Aarne Ranta",
  title =        "A Multilingual Natural Language Interface to Regular
                 Expressions",
  booktitle =    "{FSMNLP'98}: International Workshop on Finite State
                 Methods in Natural Language Processing",
  publisher =    "Bilkent University, Ankara",
  year =         "1998",
  editor =       "Lauri Karttunen and K. Oflazer",
  pages =        "79--90"
}

@Article{Ranta91a,
  author =       "Aarne Ranta",
  title =        "Constructing Possible Worlds",
  journal =      "Theoria",
  volume =       "57",
  number =       "1--2",
  pages =        "77--100",
  year =         "1991"
}

@MastersThesis{Schneider97,
  author = 	 {J\"{o}rg Schneider},
  title = 	 "{Formale Spezifikation eines
		  Autorisierungskonzepts am Beispiel des
		  Berechtigungswesens im SAP R/3-System}",
  school = 	 "Department of Computer Science, University of Karlsruhe",
  year = 	 "1997",
  type =	 {Diplomarbeit}  
}

@InProceedings{MandelCengarle99,
  author =       "Luis Mandel and Mar{\'\i}a Victoria Cengarle",
  title =        "On the Expressive Power of {OCL}",
  booktitle =    "Proc.\ FM'99 -- Formal Methods, World Congress on Formal
                 Methods in the Development of Computing Systems,
                 Toulouse, France",
  year =         "1999",
  volume =       "1708",
  series =       lncs,
  pages =        "854--874",
  publisher =    spv
}
@INCOLLECTION{steedman,
    AUTHOR = "M. Steedman",
    TITLE = "Combinators and grammars",
    EDITOR = "R. Oehrle and E. Bach and D. Wheeler",
    BOOKTITLE = {{Categorial Grammars and Natural Language Structures}},
    PUBLISHER = {D. Reidel},
    ADDRESS = {Dordrecht},
    YEAR = {1988}, 
    PAGES = {417-442}}

@InProceedings{DLR00,
  author = 	 {M.\ Dymetman and V.\ Lux and A.\ Ranta},
  title = 	 {{XML} and Multilingual Document Authoring: Convergent Trends},
  booktitle = 	 {Proc.\ Computational Linguistics COLING, Saarbr\"{u}cken, Germany},
  pages =        {243-249},
  year =	 {2000},
  publisher =    {International Committee on Computational Linguistics}
}

@InProceedings{HallgrenRanta000,
  author = 	 {T. Hallgren and A. Ranta},
  title = 	 {Grammatical Annotations: a Method of Program Documentation},
  booktitle = 	 {Proc.\ International Conference on Functional Programming ICFP},
  year =	 {submitted, 2000},
  note =	 {URL: \texttt{http://www.cs.chalmers.se/\~{}aarne/hallgren-ranta-2000.ps.gz}}
}

@inproceedings{ mccarthy62towards,
    author = "J.\ McCarthy",
    title = "Towards a mathematical science of computation",
    booktitle = "Proceedings of the Information Processing Cong. 62",
    month = "August",
    publisher = "North-Holland",
    address = "Munich, West Germany",
    pages = "21--28",
    year = "1962"
}

@InProceedings{hallgren-ranta:lpar2000,
  author = 	 {T.\ Hallgren and A.\ Ranta},
  title = 	 {An Extensible Proof Text Editor},
  editor =       {M. Parigot \& A. Voronkov},
  booktitle = 	 {Logic for Programming and Automated Reasoning (LPAR'2000)},
  year =	 {2000},
  series =	 {LNCS/LNAI 1955},
  pages =        {70--84}
}

@Book{Jackson95,
  author =       "Michael Jackson",
  title =        "Software Requirements and Specification: a lexicon of
                 practice, principles and prejudices",
  publisher =    "Addison-Wesley",
  year =         "1995"
}

@Book{Davis93,
  author =       "Alan M. Davis",
  title =        "Software Requirements: Objects, Functions and States",
  publisher =    "Prentice-Hall",
  year =         "1993"
}


@Article{ClarkeWing96,
  author	= {Edmund Clarke and Jeanette M. Wing},
  title		= {Formal Methods: State of the Art and Future Directions},
  journal	= {ACM Computing Surveys},
  volume	= {28},
  number	= {4},
  pages		= {626--643},
  year          = {1996}
}

@Book{HincheyBowen95,
  title         = {Applications of Formal Methods},
  editor        = {Michael G. Hinchey and Jonathan P. Bowen},
  publisher     = {Prentice Hall},
  year          = {1995}
}

@Book{BowenHinchey99,
  title         = {High-Integrity System Specification and Design},
  editor        = {Jonathan P. Bowen and Michael G. Hinchey},
  publisher     = spv,
  series        = {Formal Approaches to Computing and Information Technology},
  year          = {1999},
  isbn_issn     = {3-540-76226-4}
}

@Book{BowenHinchey99b,
  title         = {Industrial-Strength Formal Methods in Practice},
  editor        = {Jonathan P. Bowen and Michael G. Hinchey},
  publisher     = {Springer-Verlag, London},
  series        = {Formal Approaches to Computing and Information Technology},
  year          = {1999},
  isbn_issn     = {1-85233-640-4}
}

@MastersThesis{Finger00,
  author = 	 {Frank Finger},
  title = 	 {Design and Implementation of a modular 
                  {OCL} Compiler},
  school = 	 {Technische Universit\"{a}t Dresden, 
                  Fakult\"{a}t f\"{u}r Informatik},
  year = 	 {2000},
  type =	 {Diplomarbeit},
  month =	 mar,
  url = 	 {http://www-st.inf.tu-dresden.de/ocl/download/diplom.pdf}
}

@InProceedings{DahnWolf96,
  author =       "Bernd I. Dahn and Andreas Wolf",
  title =        "Natural Language Representation and Combination of
                 Automatically Generated Proofs",
  editor =       "Franz Baader and Klaus U.~Schulz",
  booktitle =    "Frontiers of Combining Systems: Proc.\ 1st
                 International Workshop, Munich, Germany",
  publisher =    "Kluwer Academic Publishers",
  series =       "Applied Logic",
  month =        mar,
  year =         "1996",
  pages =        "175--192"
}

@Book{Spivey92,
  author        = {J. M. Spivey},
  title         = {The {Z} Notation: A Reference Manual},
  publisher     = {Prentice Hall International Series in Computer Science},
  edition       = {2nd},
  year          = 1992,
  isbn          = {013-978529-9}
}

@InProceedings{Giese01a,
  author        = {Martin Giese},
  title         = {Incremental Closure of Free Variable Tableaux},
  booktitle     = {Proc.\ Intl.\ Joint Conf.\ on Automated Reasoning,
                  Siena, Italy},
  year          = {2001},
  series        = {LNCS},
  editor        = {Rajeev Gor\'{e} and Alexander Leitsch and Tobias Nipkow},
  publisher     = {Springer-Verlag},
  note          = {To appear}
}

@Manual{Ranta99,
  title =        {Grammatical Framework Homepage},
  author =       {Aarne Ranta},
  organization = {Chalmers University of Technology},
  address =      {Gothenburg},
  year =         {2001},
  note =         {URL: \texttt{www.cs.chalmers.se/~aarne/GF}}
}

@Manual{Ranta99a,
  title = 	 {Grammatical Framework Syntax and Semantic},
  author =	 {Aarne Ranta},
  organization = {Xerox Research Centre Europe},
  address =      {Grenoble},
  month =	 feb,
  year =	 {1999},
  note = 	 {URL: \texttt{www.xrce.xerox.com/research/mltt/gf/doc/gf-language/index.html}}
}

@Manual{Ranta99c,
  title = 	 {Grammatical Framework Implementation and Interfaces. 
                  {R}evised for {GF} Version 0.5},
  author =	 {Aarne Ranta},
  organization = {Department of Computing Science,
                  Chalmers University of Technology},
  month =	 jun,
  year =	 {1999},
  note = 	 {URL: \texttt{www.cs.chalmers.se/\~{}aarne/GF/pub/doc/gf-implementation/index.html}}}

@Manual{Ranta99b,
  title = 	 {Grammatical Framework Tutorial},
  author =	 {A. Ranta},
  organization = {Xerox Research Centre Europe},
  address =      {Grenoble},
  month =	 feb,
  year =	 1999,
  note = 	 {URL: \texttt{www.xrce.xerox.com/research/mltt/gf/doc/gf-tutorial/index.html}}
}

@TechReport{KeY00,
  author =       {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert
                  and Martin Giese and Elmar Habermalz and Reiner
                  H\"ahnle and Wolfram Menzel and Peter H. Schmitt},
  title =        {The {KeY} Approach: {I}ntegrating Object Oriented
                  Design and Formal Verification},
  institution =  {University of Karlsruhe, Department of Computer Science},
  type =         {Technical Report},
  number =       {2000/4},
  month =        jan,
  year =         {2000},
  note =         {URL: \texttt{i12www.ira.uka.de/\~{}key/doc/2000/techRep.ps.gz}}
}

@InProceedings{KeY00a,
  author =       {Wolfgang Ahrendt and Thomas Baar and Bernhard Beckert
                  and Martin Giese and Elmar Habermalz and Reiner
                  H\"ahnle and Wolfram Menzel and Peter H. Schmitt},
  booktitle =    {In Proc.\ Java Card Workshop, Cannes, France},
  title =        {The {KeY} Approach: {I}ntegrating Object Oriented
                  Design and Formal Verification},
  month =        sep,
  year =         {2000},
  publisher =    {{INRIA} technical report}
}

@InProceedings{Beckert00a,
  author        = {Bernhard Beckert},
  title         = {A Dynamic Logic for Java Card},
  booktitle     = {Proc.\ 2nd ECOOP Workshop on Formal Techniques for
                   Java Programs, Cannes, France},
  year          = {2000},                 
  note          = {URL: \texttt{http://i12www.ira.uka.de/\~{}key/doc/2000/beckert00.pdf.gz}}
}

@InProceedings{BSHS00,
  author        = {Thomas Baar and Reiner H\"ahnle and Theo Sattler and Peter H. Schmitt},
  title         = {{E}nt\-wurfs\-muster\-gesteuerte {E}rzeugung von {OCL}-{C}onstraints},
  year          = {2000},
  editor        = {Gregor Snelting},
  booktitle     = {Softwaretechnik-Trends},
  publisher     = spv,
  series        = {Informatik Aktuell},                 
  url           = {http://i12www.ira.uka.de/\~{}key/doc/2000/baarsattlerea00.pdf.gz},
  note          = {URL: \texttt{http://i12www.ira.uka.de/\~{}key/doc/2000/baarsattlerea00.pdf.gz}}
}

@InProceedings{Baar00,
  author        = {Thomas Baar},
  title         = {Experiences with the {UML}/{OCL}-Approach to
                   Precise Software Modeling:  A Report from Practice},
  year          = {2000},
  booktitle     = {Proc.\ Net.ObjectDays, Erfurt, Germany},               
  note          = {URL: \texttt{http://i12www.ira.uka.de/\~{}key/doc/2000/baar00.pdf.gz}}             
}

@Book{JTM99,
  author = 	 {Jean-Marc Jezequel and Michel Train and Christine Mingins},
  title = 	 {Design Patterns and Contracts},
  publisher = 	 {Addison-Wesley},
  ISBN_ISSN =    {0-201-30959-9},
  year = 	 {1999}
}

@Book{HuntThomas99,
  author = 	 {Andrew Hunt and David Thomas},
  title = 	 {The Pragmatic Programmer: From Journeyman to Master},
  publisher = 	 {Addison-Wesley},
  ISBN_ISSN =    {0-201-61622-X},
  year = 	 {1999}
}

@InProceedings{KdeJGN97,
       AUTHOR             = {John C. Knight and Colleen L. DeJong and 
                              Mathew S. Gibble and 
                              Lu\'{\i{}}s G. Nakano},
       PAGES              = {1--12},
       TITLE              = {Why Are Formal Methods Not {USED} More Widely?},
        ADDRESS            = {Hampton, Viginia},
        EDITOR             = {C. Michael Holloway and Kelly J. Hayhurst},
        BOOKTITLE          = {Fourth NASA Langley Formal Methods Workshop},
        SERIES             = {NASA Conference Publication},
        NUMBER             = {3356},
        YEAR               = {1997}
}


@Book{BMRSS96,
  author =       "Frank Buschmann and Regine Meunier and Hans Rohnert
                 and Peter Sommerlad and Michael Stal",
  title =        "Pattern-Oriented Software Architecture: {A} System of
                 Patterns",
  publisher =    "John Wiley \& Sons, New York",
  year =         "1996",
  location =     "D.2 Buschmann",
  isbn_issn =    {0-471-95869-7}
}

@mastersthesis{Sattler00,
        AUTHOR             = {Theo Sattler},
        school             = {{F}akult\"{a}t f\"{u}r Informatik, 
                              {U}niversit\"{a}t {K}arlsruhe},
        MONTH              = jan,
        TITLE              = {Einbindung formaler {C}onstraints 
                              in {UML} {S}pezifikationen},
        YEAR               = {2000}
}

@Book{LBSBW98,
  editor =       {Mario Lenz and Brigitte Bartsch-Sp\"{o}rl and Hans-Dieter Burkhard and Stefan Wess},
  title =        "Case-Based Reasoning Technology: From Foundations to Applications",
  series =       lnai,
  volume =       "1400",
  year =         "1998",
  publisher =    spv 
}
	  
@InProceedings{Schmitt00,
  author = 	 {Peter H. Schmitt},
  booktitle =    {??},
  title = 	 {A Model-Theoretic Semantics for {OCL}},
  note = 	 {\texttt{http://www.cs.chalmers.se/\~{}reiner/Lehre/Wien-2001/ocl.ps.gz}},
  month =	 sep,
  year =	 {2000},
  address =      {Department of Computer Science, University of Karlsruhe}
}

@InProceedings{QianKrieg-Brueckner96,
  author =       {Zhenyu Qian and Bernd Krieg-Br{\"u}ckner},
  title =        "Typed Object-Oriented Functional Programming with Late
                 Binding",
  editor =       "Pierre Cointe",
  booktitle =    "{ECOOP}: Object-Oriented Programming",
  series =       lncs,
  publisher =    spv,
  volume =       "1098",
  year =         "1996",
  ISBN_ISSN =    "3-540-61439-7",
  pages =        "48--72"
}
		  
@InProceedings{SLGJ00,
  author =       {Gerson Suny\'{e} and Alain {Le Guennec} and 
                  Jean-Marc J\'{e}z\'{e}quel},
  title =        "Design Patterns Application in {UML}",
  editor =       "Elisa Bertino",
  booktitle =    "Proc.\ 14th {ECOOP}: Object-Oriented Programming,
                  Sophia Antipolis and Cannes, France",
  series =       lncs,
  publisher =    spv,
  volume =       "1850",
  year =         "2000",
  ISBN_ISSN =    "3-540-67660-0",
  pages =        "44--62"
}
		  
@Article{Alexander99,
  author = 	 "Christopher Alexander",
  title = 	 "The Origins of Pattern Theory: The Future of the
		  Theory and the Generation of a Living World",
  journal =	 "IEEE Software",
  year =	 "1999",
  pages =	 "71--82",
  month =	 "September/October",
  note = 	 "Keynote speech at OOPSLA'96"
}

@article{Hughes89,
        AUTHOR = {John Hughes},
        TITLE = {Why Functional Programming Matters},
        JOURNAL = {Computer Journal},
        VOLUME = {32},
        NUMBER = {2},
        PAGES = {98--107},
        YEAR = {1989}
}
		  
@Book{RussellNorvig95,
  author =       "Stuart J. Russell and Peter Norvig",
  title =        "Artificial Intelligence. {A} Modern Approach",
  publisher =    "Prentice-Hall",
  address =      "Englewood Cliffs",
  year =         "1995",
  url = "http://www.cs.berkeley.edu/~russell/aima.html"
}
		  
@inproceedings{Thompson97a,
             author = {Simon Thompson},
             title = {{\em Where do I begin?} 
		  {A} problem solving approach to teaching 
		  functional programming},
             month = sep,
             year = {1997},
             pages = {},
             url = {http://www.cs.ukc.ac.uk/pubs/1997/208},
             booktitle = {First International Conference on Declarative Programming Languages in Education},
             editor = {Krzysztof Apt and Pieter Hartel and Paul Klint},
             publisher = spv,
             volume = "1292",
             pages = "323--337",
             series = lncs
             } 
		  
@InProceedings{DAC98a,
  author =       "Matthew B. Dwyer and George S. Avrunin and James C.
                 Corbett",
  title =        "Property Specification Patterns for Finite-State
                 Verification",
  pages =        "7--15",
  ISBN_ISSN =         "0-89791-954-8",
  editor =       "Mark Ardis",
  booktitle =    "Proc.\ 2nd Workshop on Formal Methods in
                 Software Practice ({FMSP}-98)",
  month =        mar,
  publisher =    "ACM Press",
  address =      "New York",
  year =         "1998"
}

@InProceedings{DAC99a,
  author =       "Matthew B. Dwyer and George S. Avrunin and James C.
                 Corbett",
  title =        "Patterns in Property Specifications for Finite-State
                 Verification",
  booktitle =    "Proc.\ 21st International Conference on
                 Software Engineering",
  year =         "1999",
  publisher =    "IEEE Computer Society Press, ACM Press",
  ISBN_ISSN =    "1-58113-074-0",
  pages =        "411--420"
}
		  
@Article{Fitting98a,
  author =       "Fitting",
  title =        "lean{TAP} Revisited",
  journal =      "jlc",
  volume =       "8",
  number =       "1",
  pages =        "33--47",
  year =         "1998"
}

@TechReport{NeculaLee96,
  author =       "G. C. Necula and P. Lee",
  title =        "Proof-Carrying Code",
  institution =  "School of Computer Science, Carnegie Mellon
                 University, Pittsburgh, USA",
  year =         "1996",
  number =       "CMU-CS-96-165",
  month =        nov,
  url =          "http://www.cs.cmu.edu/~necula/tr96-165.ps.gz"
}

@InProceedings{NeculaLee98,
  author =       "George C. Necula and Peter Lee",
  title =        "Safe, Untrusted Agents using Proof-Carrying Code",
  booktitle =    "Mobile Agents and Security",
  volume =       "1419",
  year =         "1998",
  publisher =    spv,
  series =       lncs,
  editor =       "Giovanni Vigna",
  pages =        "61--91",
  url =          "http://www.cs.cmu.edu/~necula/lncs98.ps.gz",
  ISBN_ISSN =         "0302-9743"
}

@InProceedings{Necula97,
  author =       "G. C. Necula",
  title =        {{Proof-Carrying Code}},
  booktitle =    {{Proc.\ 24th {A}{C}{M} Symposium on Principles of
                 Programming Languages, {Paris}, {France}}},
  year =         "1997",
  url =          "http://www.cs.cmu.edu/~necula/popl97.ps.gz",
  pages =        "106--119",
  publisher =    "ACM Press"
}

@Article{patr,
  author = {L. Karttunen},
  title = {PATR},           
  journal = ???,
  year =   1981,
  volume = 0,
  pages = 0
}

@Misc{hallgren-sort,
  author = "T. Hallgren",
  title = "The correctness of insertion sort",
  howpublished = www,
  documentURL = cs.chalmers,
  year = 2000
}

@Article{discont,
  author = "H. Uszkoreit",
  title = "German word order",            
  journal = ???,
  year =   1988,
  volume = ???,
  pages = ???
}

@Article{hoas,
  author = "J. Despeyroux",
  title = "Higher-Order Abstract Syntax",            
  journal = ???,
  year =   1995,
  volume = ???,
  pages = ???
}



@inproceedings{airline,
	 AUTHOR = {L. Augustsson},
	 TITLE = {{Partial Evaluation in Airline Crew Scheduling}},
	 BOOKTITLE = {???},
	 PUBLISHER = {???},
	 YEAR = {???}
 }