path: root/doc/gf-bib.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 = "Journal 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"}

@article{goldsmith,
 author = {John Goldsmith},
 title = {{An Algorithm for the Unsupervised Learning of Morphology}},
 journal = {{Nat. Lang. Eng.}},
 volume = {12},
 number = {4},
 year = {2006},
 issn = {1351-3249},
 pages = {353--371},
 doi = {http://dx.doi.org/10.1017/S1351324905004055},
 publisher = {Cambridge University Press},
 address = {New York, NY, USA},
 }

@article{creutz,
 author = {Mathias Creutz and Krista Lagus},
 title = {{Unsupervised Models for Morpheme Segmentation and Morphology Learning}},
 journal = {{ACM Trans. Speech Lang. Process.}},
 volume = {4},
 number = {1},
 year = {2007},
 issn = {1550-4875},
 pages = {3},
 doi = {http://doi.acm.org/10.1145/1187415.1187418},
 publisher = {ACM},
 address = {New York, NY, USA},
 }

@article{swadesh,
 author = {Morris Swadesh},
 title = {{Towards Greater Accuracy in Lexicostatistic Dating}},
 journal = {{International Journal of American Linguistics}},
 volume = {21},
 year = {1955},
 pages = {121--137}
 }

@INPROCEEDINGS{isar,
  AUTHOR = {M. Wenzel},
  TITLE = {{Isar - a Generic Interpretative Approach to Readable Formal Proof Documents}},
  BOOKTITLE = {{Theorem Proving in Higher Order Logics, TPHOLs'99}},
  YEAR = {1999},
  series = lncs,
  volume = {1690},
  EDITOR = {Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th\'{e}ry}
}

@INPROCEEDINGS{pollard-hog,
  AUTHOR = {C. Pollard},
  TITLE = {{Higher-Order Categorial Grammar}},
  BOOKTITLE = {{Proceedings of the 
     Conference on Categorial Grammars (CG2004), Montpellier, France}},
  PAGES = {340--361},
  YEAR = {2004},
  EDITOR = {M. Moortgat}
}

@INPROCEEDINGS{muskens-lg,
  AUTHOR = {R. Muskens},
  TITLE = {Lambda {G}rammars and the {S}yntax-{S}emantics
                  {I}nterface},
  BOOKTITLE = {Proceedings of the Thirteenth Amsterdam Colloquium},
  PAGES = {150--155},
  YEAR = {2001},
  EDITOR = {van Rooy, R. and Stokhof, M.},
  PS = {amscoll.ps},
  PDF = {amscoll.pdf},
  ADDRESS = {Amsterdam}
}

@inproceedings{degroote-acg,
  title = {{Towards Abstract Categorial Grammars}},
  author = {Ph. de Groote},
  booktitle = {{Association for Computational Linguistics, 
    39th Annual Meeting and 10th Conference of the European Chapter, Toulouse, France}},
  pages = {148--155},
  year = {2001}
}

@misc{talk-deliv,
  author = {P. Ljungl\"of and G. Amores and R. Cooper and D. Hjelm and O. Lemon and P. Manchón
    and G. Pérez and A. Ranta},
  year = 2006,
  title = {{Multimodal Grammar Library}},
  note = {{TALK. Talk and Look: 
    Tools for Ambient Linguistic Knowledge. IST-507802. Deliverable 1.2b}}
  }

@INCOLLECTION{mar82,
    AUTHOR = "{Martin-L\"{o}f}, Per",
    TITLE = "Constructive mathematics and computer programming",
    EDITOR = "Cohen and Los and Pfeiffer and Podewski",
    BOOKTITLE = "Logic, Methodology and Philosophy of Science VI",
    PUBLISHER = {North-Holland},
    ADDRESS = {Amsterdam},
    YEAR = {1982},
    PAGES = {153-175}}


@inproceedings{wiedijk,
        AUTHOR = {F. Wiedijk},
        BOOKTITLE = {{Types for Proofs and Programs}},
        PUBLISHER = {Springer},
        SERIES = {LNCS 3085},
        editors = {S. Berardi and M. Coppo and F. Damiani},
        PAGES = {378--393},
        TITLE   = {{Formal Proof Sketches}}, 
        YEAR = {2004}
        }

@inproceedings{bender,
  author = {Bender, Emily M. and Flickinger, Dan},
  title = {Rapid Prototyping of Scalable Grammars: 
  Towards Modularity in Extensions to a Language-Independent Core},
  booktitle = {Proceedings of the 2nd International Joint Conference on 
   Natural Language Processing IJCNLP-05 (Posters/Demos)},
  address = {Jeju Island, Korea},
  year = 2005
}

@book{keybook,
        AUTHOR  = {B. Beckert and R. Hähnle and P. Schmitt},
        TITLE   = {{Verification of Object-Oriented Software: The KeY Approach}},
        YEAR    = {2006},
        series  = lncs,
        volume  = {4334}, 
        PUBLISHER = {{Springer-Verlag}}
}

@book{CopestakeLKB,
        AUTHOR  = {A. Copestake},
        TITLE   = {{Implementing Typed Feature Structure Grammars}},
        YEAR    = {2002},
        PUBLISHER = {{CSLI Publications}}
}

@book{stroustrup,
        AUTHOR  = {B. Stroustrup},
        TITLE   = {{The C++ Programming Language, Third Edition}},
        YEAR    = {1998},
        PUBLISHER = {{Addison-Wesley}}
}


@techreport{bringert,
  author = {B. Bringert},
  title = {{Embedded Grammars}},
  institution   = {Department of Computing Science, Chalmers University
		   of Technology},
  type          = {{MSc Thesis}},
  year          = {2004}
}

@techreport{humayoun,
  author = {M. Humayoun},
  title = {{Urdu Morphology, Orthography and Lexicon Extraction}},
  institution   = {Department of Computing Science, Chalmers University
		   of Technology},
  type          = {{MSc Thesis}},
  year          = {2006}
}


@inproceedings{khegai-acl,
  title = {{GF Parallel Resource Grammars and Russian}},
  author = {J. Khegai},
  booktitle = {{Coling/ACL 2006}},
  pages = {475--482},
  year = {2006}
}

@inproceedings{bos-steedman,
  title = {{Wide-Coverage Semantic Representations from a CCG Parser}},
  author = {J. Bos and S. Clark and M. Steedman and J. Curran and J. Hockenmaier},
  booktitle = {{Coling 2004}},
  year = {2004}
}

@inproceedings{FM,
  title = {{Functional Morphology}},
  author = {M. Forsberg and A. Ranta},
  booktitle = {{ICFP 2004, Showbird, Utah}},
  pages = {213-223},
  year = {2004}
}

@inproceedings{ranta-features,
  title = {{Features in Abstract and Concrete Syntax}},
  author = {A. Ranta},
  booktitle = {{NODALIDA Workshop on Typed Feature Structure Grammars, Tartu, 24 May 2007}},
  year = {2007}
}


@inproceedings{eldada,
  title =  {{Implementing an Open Source Arabic Resource Grammar in GF}},
  author = {A. El Dada and A. Ranta},
  booktitle = {{20th Arabic Linguistics Symposium. Western Michigan University March 3-5 2006}},
  year = {2006}

}

@incollection{eldada-book,
  title =  {{Implementing an Open Source Arabic Resource Grammar in GF}},
  author = {A. El Dada and A. Ranta},
  booktitle = {{Perspectives on Arabic Linguistics XX}},
  editor = {M.A. Mughazy},
  publisher = {{John Benjamin's}},
  pages = {209--232},
  year = {2007}

}

@inproceedings{nganga-africa,
  title = {{Multilingual content development for eLearning in Africa}},
  author = {W. Ng'ang'a},
  booktitle = {{1st Pan-African Conference on ICT for Development, Education and Training. 
     24-26 May 2006, Addis Ababa, Ethiopia}},
  year = {2006}

}

@inproceedings{bringert-speechgram,
  title = {{Speech Recognition Grammar Compilation in Grammatical Framework}},
  author = {B. Bringert},
  booktitle = {{SPEECHGRAM 2007: ACL Workshop on Grammar-Based Approaches to Spoken 
   Language Processing, June 29, 2007, Prague}},
  year = {2007}
}

@inproceedings{perera-ranta,
  title = {{Dialogue System Localization with the GF Resource Grammar Library}},
  author = {N. Perera and A. Ranta},
  booktitle = {{SPEECHGRAM 2007: ACL Workshop on Grammar-Based Approaches to Spoken 
   Language Processing, June 29, 2007, Prague}},
  year = {2007}
}



@inproceedings{caprotti,
  title = {{WebALT! Deliver Mathematics Everywhere}},
  author = {O. Caprotti},
  booktitle = {{Proceedings of SITE 2006. Orlando March 20-24}},
  year = {2006}
}

@inproceedings{ranta-kahn,
  title = {{Grammars as Software Libraries}},
  author = {A. Ranta},
  booktitle = {{From Semantics to Computer Science}},
  editor = {Y. Bertot and G. Huet and J-J. L\'evy and G. Plotkin},
  publisher = {{Cambridge University Press}},
  year = {2008}
}



@ARTICLE{landin,
    AUTHOR = "P. Landin",
    TITLE = "The Next 700 Programming Languages",
    JOURNAL = {{Communications of the ACM}},
    VOLUME = {9},
    PAGES = {157--166},
    YEAR = {1966} 
}

@techreport{KeY2003,
   author        = {Wolfgang Ahrendt and Thomas Baar and 
                    Bernhard Beckert and Richard Bubel and
		    Martin Giese and Reiner H\"ahnle and
		    Wolfram Menzel and Wojciech Mostowski and
		    Andreas Roth and Steffen Schlager and
		    Peter H. Schmitt},
   title         = {The KeY Tool},
   institution   = {Department of Computing Science, Chalmers University
		    and G\"oteborg University, G\"oteborg, Sweden},
   type          = {Technical Report in Computing Science No.\ 2003-5},
   month         = feb,		  
   year          = {2003}
}



@PHDTHESIS{muskens-diss,
  AUTHOR = {Muskens, R.},
  YEAR = 1989,
  TITLE = {Meaning and {P}artiality},
  SCHOOL = {University of Amsterdam}
}

@ARTICLE{copestake,
    AUTHOR = "A. Copestake and D. Flickinger",
    TITLE = {{An open-source grammar development environment and broad-coverage English grammar using HPSG}},
    JOURNAL = {{Proceedings of the Second conference on Language Resources and Evaluation (LREC-2000)}},
    YEAR = {2000} 
}

@ARTICLE{multieng,
    AUTHOR = "A. Ranta",
    TITLE = {{Modular Grammar Engineering in GF}},
    JOURNAL = {{Research on Language and Computation}},
    volume = {5},
    pages = {133--158},
    YEAR = {2007} 
}


@book{pereira-shieber,
        AUTHOR  = {F. Pereira and S. Shieber},
        TITLE   = {{Prolog and Natural-Language Analysis}},
        ADDRESS = {Stanford},
        YEAR    = {1987},
        PUBLISHER = {{CSLI}}
}

@book{aho-ullman,
        AUTHOR  = {A. Aho and R. Sethi and J. Ullman},
        TITLE   = {{Compilers: Principles, Techniques, and Tools}},
        YEAR    = {1988},
        PUBLISHER = {{Addison-Wesley}}
}

@book{aho-lam-ullman,
        AUTHOR  = {A. Aho and M. Lam and R. Sethi and J. Ullman},
        TITLE   = {{Compilers: Principles, Techniques, and Tools. Second Edition}},
        YEAR    = {2006},
        PUBLISHER = {{Addison-Wesley}}
}

@book{karttunen-beesley,
        AUTHOR  = {K. Beesley and L. Karttunen},
        TITLE   = {{Finite State Morphology}},
        YEAR    = {2003},
        PUBLISHER = {{CSLI Publications}}
}

@InProceedings{degroote02,
   author = {Ph. de Groote},
   title = {{Tree-Adjoining Grammars as Abstract Categorial Grammars}},
   booktitle = {{TAG+6, Proceedings of the sixth International Workshop
     on Tree Adjoining Grammars and Related Frameworks}},
   pages = {145--150},
   publisher = {Universit\`a di Venezia},
   year = {2002}
}

@InProceedings{saghein-1978,
   author = "Anna {S\aa gvall Hein}",
   title = {{Finnish Morphological Analysis in the Reversible Grammar System}},
   booktitle = {{COLING 78, Information Abstracts}},
   year = {1978}
}

@ARTICLE{saghein-1980,
    AUTHOR = "Anna {S\aa gvall Hein}",
    TITLE = "An Outline of a Computer Model of Finnish Word Recognition",
    JOURNAL = {{Fenno-Ugrica Suecana}},
    VOLUME = {3},
    PAGES = {7--26},
    YEAR = {1980} }

@ARTICLE{koskenniemi-1980,
    AUTHOR = "Kimmo Koskenniemi",
    TITLE = "On Automatic Lemmatization of Finnish",
    JOURNAL = {{Fenno-Ugrica Suecana}},
    VOLUME = {3},
    PAGES = {27--44},
    YEAR = {1980} }


@book{martin-lof,
        AUTHOR  = {P. Martin-L\"{o}f},
        TITLE   = {{Intuitionistic Type Theory}},
        ADDRESS = {Napoli},
        YEAR    = {1984},
        PUBLISHER = {Bibliopolis}
}
@BOOK{curryfeys,
    AUTHOR = "Curry, H. B. and R. Feys",
    TITLE = "Combinatory Logic, Vol. 1",
    PUBLISHER = {North-Holland},
    ADDRESS = {Amsterdam},
    YEAR = {1958} }

@ARTICLE{scott-str,
    AUTHOR = "D. S. Scott and C. Strachey",
    TITLE = "Toward a mathematical semantics for computer languages",
    JOURNAL = {Microwave Research Institute Symposia Series},
    VOLUME = {21},
    PAGES = {19--46},
    YEAR = {1970} }

@ARTICLE{partee,
    AUTHOR = {B. Partee},
    TITLE = {Montague grammar and transformational grammar},
    JOURNAL = {{Linguistic Inquiry}},
    VOLUME = {6},
    PAGES = {203--300},
    YEAR = {1975} }

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

@Book{lyons,
  author =	 {J. Lyons},
  title = 	 {{Introduction to Theoretical Linguistics}},
  publisher = 	 {{Cambridge University Press}},
  year = 	 {1968}
}

@Book{b-b,
  author =	 {P. Blackburn and J. Bos},
  title = 	 {Representation and Inference for Natural Language},
  publisher = 	 {Studies in Logic, Language, and Information, CSLI Press},
  year = 	 {to appear}
}

@Book{cooper,
  author =	 {R. Cooper},
  title = 	 {Quantification and Syntactic Theory},
  publisher = 	 {D. Reidel},
  year = 	 {1981}
}

@Book{jasmin,
  author =	 {J. Meyer and T. Downing},
  title = 	 {{Java Virtual Machine}},
  publisher = 	 {O'Reilly},
  year = 	 {1997}
}

@Misc{gf,
  author =       {A. Ranta},
  title =        {{\mbox{Grammatical Framework Homepage}}},
  howpublished = {\verb!http://www.cs.chalmers.se/~aarne/GF/!},
  documentURL =  {"http://www.cs.chalmers.se/~aarne/GF/"},
  year =         {2000--2003}
}

@Misc{bnfc,
  author =       {M. Forsberg and A. Ranta},
  title =        {{\mbox{BNF Converter Homepage}}},
  howpublished = {\verb!http://www.cs.chalmers.se/~markus/BNFC/!},
  documentURL =  {"http://www.cs.chalmers.se/~markus/BNFC/"},
  year =         {2002--2004}
}

@Misc{twelf,
  author =       {F. Pfenning},
  title =        {{The Twelf Project}},
  howpublished = {\verb!http://www-2.cs.cmu.edu/~twelf!},
  documentURL =  {"http://www-2.cs.cmu.edu/~twelf"},
  year =         {2002}
}

@INCOLLECTION{scott,
    AUTHOR = "D. S. Scott",
    TITLE = "Advice on modal logic",
    booktitle = {Philosophical Problems in Logic},
    EDITOR = {K.\ Lambert},
    publisher = {D. Reidel},
    YEAR = {1970} }

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

@BOOK{grevisse,
    AUTHOR = "Grevisse, Maurice",
    TITLE = "Le bon usage, 13me edition",
    PUBLISHER = {Duculot},
    ADDRESS = {Paris},
    YEAR = {1993} }

@BOOK{diderichsen,
    AUTHOR = "Diderichsen, Paul",
    TITLE = "Elementaer dansk grammatik",
    ADDRESS = {Kobenhavn},
    YEAR = {1962} }

@BOOK{regulus,
    AUTHOR = {Rayner, M. and Hockey, B. A. and Bouillon, P.},
    TITLE = "Putting Linguistics into Speech Recognition: The Regulus Grammar Compiler",
    publisher = {{CSLI Publications}},
    YEAR = {2006} }

@INCOLLECTION{steedman,
    AUTHOR = "Steedman, M.",
    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}}

@INCOLLECTION{friedman,
    AUTHOR = "Friedman, J.",
    TITLE = "Expressing logical formulas in natural language",
    EDITOR = "J. Groenendijk and T. Janssen and M. Stokhof",
    BOOKTITLE = "Formal Methods in the Study of Language, Part 1",
    PUBLISHER = {Mathematisch Centrum},
    ADDRESS = {Amsterdam},
    YEAR = {1981}, 
    PAGES = {113-130}}

@ARTICLE{fri-war,
    AUTHOR = "Friedman, J. and D. Warren",
    TITLE = "A parsing method for {Montague} grammar",
    JOURNAL = {Linguistics and Philosophy},
    VOLUME = {2},
    PAGES = {347-372},
    YEAR = {1978} }

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

@BOOK{gazdar,
    AUTHOR = "Gazdar, G. and E. Klein and G. Pullum and I. Sag",
    TITLE = "Generalized Phrase Structure Grammar",
    PUBLISHER = {Basil Blackwell},
    ADDRESS = {Oxford},
    YEAR = {1985} }

@BOOK{chomsky,
    AUTHOR = "Chomsky, N.",
    TITLE = "Syntactic Structures",
    PUBLISHER = {Mouton},
    ADDRESS = {The Hague},
    YEAR = {1957} }





@Misc{nuance,
  author =       {{Nuance Communications}},
  title =  {{Nuance}},
  note = {\verb6http://www.nuance.com6},
  year =         2002
}

@Article{godis,
  author = "S. Larsson and D. Traum",
  title =  {{Information state and dialogue management in the 
             TRINDI Dialogue Move Engine Toolkit}},
  journal = {{Natural Language Engineering}},
  year =   2000,
  volume = 0,
  pages =  0
}



@BOOK{CLE,
    AUTHOR = "Alshawi, H",
    TITLE = {{The Core Language Engine}},
    PUBLISHER = {{MIT Press}},
    ADDRESS = {Cambridge, Ma},
    YEAR = {1992} }

@BOOK{cle2,
    AUTHOR = {M. Rayner and D. Carter and P. Bouillon and V. Digalakis and 
              M. Wirén},
    TITLE = {{The Spoken Language Translator}},
    PUBLISHER = {{Cambridge University Press}},
    ADDRESS = {Cambridge},
    YEAR = {2000} }


@Article{kaplan-kay,
  author = "R. Kaplan and M. Kay",
  title =  {{Regular Models of Phonological Rule Systems}},
  journal = {{Computational Linguistics}},
  year =   1994,
  volume = 20,
  pages =  {{331--380}}
}


@inproceedings{Dow:Hoc:Gaw:01,
  title = {{Practical Issues in Compiling Typed Unification Grammars 
           for Speech Recognition}},
  author = {J. Dowding and B. A. Hockey and J. M. Gawron
            and C. Culy},
  booktitle = {{ACL 2001}},
  address = {{Toulouse, France}},
  year = 2001
}

@inproceedings{carlson-2005,
  title = {{Inducing a Morphological Transducer from Inflectional Paradigms}},
  author = {Lauri Carlson},
  booktitle = {{Inquiries into Words, Constraints and Contexts.
    Festschrift for Kimmo Koskenniemi on his 60th Birthday}},
  publisher = {{CSLI}},
  year = 2005
}

@BOOK{dowty,
    AUTHOR = "Dowty, D",
    TITLE = "Word Meaning and Montague Grammar",
    PUBLISHER = {D. Reidel},
    ADDRESS = {Dordrecht},
    YEAR = {1979} }


@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{bringert-srg,
    AUTHOR = {Bj\"orn Bringert},
    TITLE = "Speech Recognition Grammar Compilation in Grammatical Framework",
    YEAR = {2007},
    NOTE = {Submitted for publication} 
}

@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{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{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{huet-sanskrit-short,
  author = "G. Huet",
  title = "Sanskrit site",
  howpublished = {\verb6http://pauillac.inria.fr/~huet/SKT/6}, 
  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
}

@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{sml,
    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}
}

@Article{boehm-p,
  author = {C. B\"{o}hm},
  title = {{On a family of Turing machines and the related programming language}},
  journal = {{ICC Bulletine}},
  year = 1964,
  volume = 3,
  pages = {185-194}
}

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

@Article{abrusci,
  author = "M. Abrusci",
  title = {{Noncommutative Intuitionistic Linear Propositional Logic}},
  journal = {{Zeitschrift für Mathematische Logik und Grundlagen der Mathematik}},
  year =   1990,
  volume = 36,
  pages =  {297--398}
}


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

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

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

@Book{prolog,
  author =       {W. F. Clocksin and C. S. Mellish},
  title =        {{Programming in Prolog}},
  publisher =    {Springer},
  year =         {1984}
}

@Article{hockett,
  author = {C. F. Hockett},
  title = "Two Models of Grammatical Description",            
  journal = "Word",
  year =   1954,
  volume = 10,
  pages = {210--233}
}

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


@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{TomitaCarbobell,
  author    = {Masaru Tomita and
               Jaime G. Carbonell},
  title     = {The Universal Parser Architecture for Knowledge-based Machine
               Translation},
  booktitle = {IJCAI},
  year      = {1987},
  pages     = {718-721},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@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 = {{LNCS/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
}

@Book{lfg,
  editor = "J. Bresnan",
  title = {{The Mental Representation of Grammatical Relations}},	
  publisher = {{MIT Press}},
  year = 1982
}


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


@ARTICLE{mcfg,
  author= {H. Seki and T. Matsumura and M. Fujii and T. Kasami},
  title = "On Multiple Context-Free Grammars", 
  journal = {{Theoretical Computer Science}}, 
  volume = 88, 
  pages = {191--229}, 
  year = 1991
}





@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{morrill,
	AUTHOR  = {G. Morrill},
	TITLE	= {{Type Logical Grammar}},
	YEAR    = {1994},
	PUBLISHER = {Kluwer}
}

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


@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{butt,
  author = 	 {M. Butt and H. Dyvik and T. Holloway King and  H. Masuichi 
                  and C. Rohrer},
  title = 	 {{The Parallel Grammar Project}},
  booktitle = {{COLING 2002, Workshop on Grammar Engineering and Evaluation}},
  pages =        {1--7},
  year =	 {2002}
}

@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 =	 {{LNCS/LNAI}},
  volume =       {1955},
  publisher =    {Springer},
  pages =        {70--84}
}

@InProceedings{burke-johannisson,
  author = 	 {D. A. Burke and K. Johannisson},
  title = {{Translating Formal Software Specifications to Natural 
    Language / A Grammar-Based Approach}},
  booktitle = 	 {{Logical Aspects of Computational Linguistics (LACL 2005)}},
  editor =       {{P. Blache and E. Stabler and J. Busquets and R. Moot}},
  year =	 {2005},
  series =	 {{LNCS/LNAI}},
  volume =       {3402},
  pages =        {51--66},
  publisher =    {Springer}
}

@InProceedings{FASE,
  author = 	 {R.\ Hähnle and K.\ Johannisson and A.\ Ranta},
  title = {{An Authoring Tool for Informal and Formal Requirements Specifications}},
  booktitle = 	 {{Fundamental Approaches to Software Engineering}},
  editor =       {R.-D. Kutsche and H. Weber},
  year =	 {2002},
  series =	 {LNCS},
  volume =       {2306},
  pages =        {233--248},
  publisher =    {Springer}
}

@InProceedings{khegai,
  author = 	 {J.\ Khegai and B.\ Nordström and A.\ Ranta},
  title =        {{Multilingual Syntax Editing in GF}},
  booktitle = 	 {{Intelligent Text Processing and Computational Linguistics
                 (CICLing-2003), Mexico City, February 2003}},
  year =	 {{2003}},
  series =	 {LNCS},
  volume =       {2588},
  editor =       {A. Gelbukh},
  pages =        {453--464},
  publisher =    {Springer-Verlag}
}

@ARTICLE{gf-jfp,
    AUTHOR = "A. Ranta",
    TITLE = {{Grammatical Framework: A Type-Theoretical Grammar Formalism}},
    JOURNAL = {{The Journal of Functional Programming}},
    pages={145--189},
    volume={14(2)},
    YEAR = {2004} }

@ARTICLE{huet-2005,
    AUTHOR = "Gerard Huet",
    TITLE = {{A Functional Toolkit for Morphological and Phonological Processing, Application to a Sanskrit Tagger}},
    JOURNAL = {{The Journal of Functional Programming}},
    pages={573--614},
    volume={15(4)},
    YEAR = {2005} }

@InProceedings{extract-2006,
    AUTHOR = {M. Forsberg and H. Hammarstr\"{o}m and A. Ranta},
    TITLE = {{Morphological Lexicon Extraction from Raw Text Data}},
    booktitle = 	 {{FinTAL 2006}},
    year =	 {{2006}},
    series =	 {{LNCS/LNAI}},
    volume =       {4139},
    editor =       {T. Salakoski}
  }

@InProceedings{numerals,
    AUTHOR = {H. Hammarstr\"{o}m and A. Ranta},
    TITLE = {{Cardinal Numerals Revisited in GF}}, 
    booktitle = {{Workshop on Numerals in the World's Languages, 
      Dept. of Linguistics, Max Planck Institute for Evolutionary Anthropology, 
      Leipzig}},
    year =	 {{2004}}
  }

@misc{minnen95offline,
  author = "G. Minnen and D. Gerdemann and T. Gotz",
  title = "Off-line optimization for Earleystyle hpsg processing",
  text = "G. Minnen, D. Gerdemann, and T. Gotz. Off-line optimization for Earleystyle
    hpsg processing. In Proc. of the 7th Conference of the eacl, Dublin, 1995.",
  year = "1995",
  url = "citeseer.ist.psu.edu/article/minnen95offline.html" }

@Misc{Happy-GLR,
  author =       {P. Callaghan and B. Medlock},
  title =        {{Happy-GLR}},
  note = {\verb6http://www.dur.ac.uk/p.c.callaghan/happy-glr/6},
  year =         2004
}

@Misc{XLE-homepage,
  author =       {R. Kaplan and J. Maxwell},
  title =        {{XLE Project Homepage}},
  note = {\verb6http://www2.parc.com/isl/groups/nltt/xle/6},
  year =         2007
}



@Misc{GF-homepage,
  author =       {A. Ranta},
  title =        {{Grammatical Framework Homepage}},
  note = {\verb6digitalgrammars.com/gf6},
  url = "digitalgrammars.com/gf",
  year =         2008
}

@Misc{kotus-wordlist,
  author =       "{Kotimaisten Kielten Tutkimuskeskus}",
  title =        {{KOTUS Wordlist}},
  note = {\verb6kaino.kotus.fi/sanat/nykysuomi6},
  year =         2006
}

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

@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{nssk,
  editor =	 {M. Sadeniemi},
  title = 	 {{Nykysuomen sanakirja}},
  publisher = 	 {{WSOY}},
  year = 	 {1961}
}

@Book{hellberg,
  author =	 {S. Hellberg},
  title = 	 {{The Morphology of Present-Day Swedish}},
  publisher = 	 {{Almqvist \& Wiksell}},
  year = 	 {1978}
}

@Book{karlsson-1977,
  author =	 {F. Karlsson},
  title = 	 {{Finsk grammatik}},
  publisher = 	 {{Suomalaisen Kirjallisuuden Seura}},
  year = 	 {1977}
}

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

@Misc{coq,
  author =       {{The Coq Development Team}},
  title =	 {{The Coq Proof Assistant Reference Manual}},
  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
}

@InProceedings{brodda-karlsson,
  author =       {B. Brodda and F. Karlsson},
  title =        {{An Experiment with Automatic Morphological Analysis of Finnish}},
  series =       {{Papers from the Institute of Linguistics, University of Stockholm}},
  volume =       40,
  year =         1978
}



@PhdThesis{fiedler,
  author =   {A. Fiedler},
  title =   {{User-Adaptive Proof Explanation}},
  school =   {{Universität des Saarlandes}},
  year =   2001
}

@PhdThesis{koskenniemi-1983,
  author =   {Kimmo Koskenniemi},
  title =   {{Two-Level Morphology: A General Computational Model for 
              Word-Form Recognition and Production}},
  school =   {{University of Helsinki}},
  year =   1983
}

@PhdThesis{peb,
  author =   {P. Ljungl\"of},
  title =   {{The Expressivity and Complexity of Grammatical Framework}},
  school =   {{Dept.\ of Computing Science,
               Chalmers University of Technology and 
               Gothenburg University}},
  year =   {2004}
}

@PhdThesis{forsberg-2007,
  author =   {Markus Forsberg},
  title =   {{Three Tools for Language Processing: BNF Converter, 
             Functional Morphology, and Extract}},
  school =   {{Dept.\ of Computer Science and Engineering,
               Chalmers University of Technology and 
               Gothenburg University}},
  year =   {2007}
}

@InProceedings{peb-parsing,
  author =   {P. Ljungl\"of},
  title =   {{Grammatical Framework and Multiple Context-Free Grammars}},
  booktitle = {{Proceedings of Formal Grammar, Nancy, August 2004}},
  editor = {G. Jaeger and P. Monachesi and G. Penn and S. Wintner},
  pages = {77--90},
  year =   {2004}
}

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

@misc{cooper-anna,
  author = {R. Cooper},
  year = 2008,
  title = "The Abstract-Concrete Syncat Distinction and Unification in Multilingual Grammar",
  note = {to appear}
  }

@misc{fracas,
  author = {H. Kamp and R. Crouch and J. van Genabith and R. Cooper and M. Poesio 
            and J. van Eijck and J. Jaspars and M. Pinkal and E. Vestre and S. Pulman}, 
  year = 1994,
  title = "Specification of Linguistic Coverage",
  note = {{FRACAS Deliverable D2}} 
  }



@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"
}

@inproceedings{nlyacc,
 author = {Masayuki Ishii and Kazuhisa Ohta and Hiroaki Saito},
 title = {An efficient parser generator for natural language},
 booktitle = {Proceedings of the 15th conference on Computational linguistics},
 year = {1994},
 pages = {417--420},
 location = {Kyoto, Japan},
 doi = {http://dx.doi.org/10.3115/991886.991959},
 publisher = {Association for Computational Linguistics},
 address = {Morristown, NJ, USA},
 }

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

@book{mueller,
  author =       {Stefan Müller},
  title =        {{Deutsche Syntax Deklarativ}},
  year =         1999,
  publisher =      {{Max Niemeyer Verlag}}
}

@article{ranta-cooper,
  author =       {A. Ranta and R. Cooper},
  title =        {{Dialogue Systems as Proof Editors}},
  journal =      {{Journal of Logic, Language and Information}},
  year =         2004
}

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


@inproceedings{gf-srg,
 author = {Bj\"orn Bringert},
 title = {{Speech Recognition Grammar Compilation in Grammatical Framework}},
 booktitle = {{Proceedings of the Workshop on Grammar-Based Approaches to Spoken Language Processing}},
 month = jun,
 year = {2007},
 pages = {1--8},
 location = {{Prague, Czech Republic}},
 publisher = {{Association for Computational Linguistics}}
}

@inproceedings{mm-grammars-dialor05,
  author = {Bj\"orn Bringert and Robin Cooper 
            and Peter Ljungl\"of and Aarne Ranta},
  title = {Multimodal Dialogue System Grammars},
  booktitle = {Proceedings of DIALOR'05, Ninth Workshop on 
               the Semantics and Pragmatics of Dialogue},
  month = {June},
  year = {2005},
  pages = {53--60},
  location = {Nancy, France},
  url = {http://www.cs.chalmers.se/~bringert/publ/mm-grammars-dialor/mm-grammars-dialor.pdf}
}


@InProceedings{ranta-nancy,
  author =       {A. Ranta},
  title =        {Resource Grammars for Dialogue Systems and Grammar Writing by Examples},
  booktitle =    {{TALK Meeting}},
  year =         2005,
  address =      {{Nancy}}
}

@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{kay1997,
         AUTHOR = {M. Kay},
         TITLE  = {{The Proper Place of Men and Machines in Language Translation}},
         JOURNAL = {{Machine Translation}},
         YEAR = {1997},
         NUMBER = {1--2},
         VOLUME = {12},
         PAGES = {3--23}
 }


@unpublished{together,
  title   = {{Together}},
  author  = {{Borland Software Corporation}},
  howpublished	= {Online document},
  year          = {2004},
  note		= {\verb!http://www.borland.com/together/!}
  }

@unpublished{lkb,
  title   = {{The LKB System}},
  author  = {Ann Copestake},
  howpublished	= {Online document},
  year          = {2002},
  note		= {Available on-line in \verb!http://www-csli.stanford.edu/~aac/lkb.html!}
  }

@unpublished{eclipse,
  title   = {{Eclipse Homepage}},
  author  = {{Eclipse.org}},
  howpublished	= {Online document},
  year          = {2004},
  note		= {\verb!http://www.eclipse.org/!}
  }

@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{huet-trie,
  author = {G. Huet},
  title  = {{The Zen Computational Linguistics Toolkit}}, 
  howpublished	= {{ESSLLI Summer School, Trento}},
  note		= {\verb!http://pauillac.inria.fr/~huet/!},
  year = 2002
}

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


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

@Misc{Isabelle-Paulson,
  author =	 "L. Paulson",
  title =	 {{The Isabelle Reference Manual}},
  note =         {{With contributions by T. Nipkow and M. Wenzel}},
  howpublished = {Available at the Isabelle homepage \verb!http://www.cl.cam.ac.uk/Research/HVG/Isabelle/!},
  documentURL = "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/Isabelle2002/doc/ref.pdf",
  year =	 2002
}

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

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




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


@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/},
}

@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{KRC,
  author =	 {Brian Kernighan and Dennis Ritchie},
  title = 	 {{The C Programming Language}},
  publisher = 	 {{Prentice Hall}},
  year = 	 1988,
  note =	 {Second Edition}
}

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

@BOOK{rei48,
    AUTHOR = "Reichenbach, Hans",
    TITLE = "Elements of Symbolic Logic",
    PUBLISHER = {The MacMillan Company},
    ADDRESS = {New York},
    YEAR = {1948} }


@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{LindholmYellinJVM,
  editor    = {T. Lindholm and F. Yellin},
  title     = {{The Java Virtual Machine Specification Second Edition}},
  publisher = {{Addison-Wesley}},
  year      = {{1999}}
}

@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"
}  

@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 = 	 {{PLI-1999: 
                  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"
}

@InProceedings{semBNF,
  author =       {{P. M\"aenp\"a\"a}},
  title =        {{Semantic BNF}},
  booktitle =    "Types for Proofs and Programs, TYPES'96", 
  series =       lncs,
  publisher =    spv,
  volume =       "1512",
  pages =        "196--215",
  year =         "1998",
  editor =       "E. Gimenez and C. Paulin-Mohring"
}


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

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


@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"
}


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


@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 = {???}
 }

@Article{Parnas,
  author =       {D. Parnas},
  title =        {{On the Criteria To Be Used in Decomposing Systems into Modules}},
  journal =      {{Communications of the ACM}},
  volume =       {15},
  pages =        {1053--1058},
  year =         {1972}
}

@Article{ranta:compsem,
  author =       {A. Ranta},
  title =        {{Computational Semantics in Type Theory}},
  journal =      {{Mathematics and Social Sciences}},
  volume =       {165},
  pages =        {31--57},
  year =         {2004}
}


@inproceedings{jonson-2006,
	 AUTHOR = {Rebecca Jonson},
	 TITLE = {{Generating statistical language models from interpretation grammars in dialogue system}},
	 BOOKTITLE = {{Proceedings of EACL'06, Trento, Italy}},
	 YEAR = {2006}
 }

@inproceedings{gf-esslli,
	 AUTHOR = {A. Ranta},
	 TITLE = {{Grammatical Framework Tutorial}},
	 BOOKTITLE = {{ESSLLI 2003 Course Material I}},
	 PUBLISHER = {{Kurt G\"odel Society}},
         pages = {1--86},
	 YEAR = {2004}
 }

@Article{mccarthy,
  author =       {J. McCarthy},
  title =        {{Recursive Functions of Symbolic Expressions and their
                 Computation by Machine, part I}},
  journal =      {{Communications of the ACM}},
  volume =       {3},
  pages =        {184--195},
  year =         {1960}
}