diff --git a/doc/gf-bib.bib b/doc/gf-bib.bib
new file mode 100644
index 000000000..ecdb33462
--- /dev/null
+++ b/doc/gf-bib.bib
@@ -0,0 +1,2099 @@
+@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{KeY2004,
+   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},
+   journal       = {Software and System Modeling},
+   year          = {2004},
+   note          = {Online First issue, to appear in print}
+}
+
+@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}
+}
+
+
+
+
+@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} 
+}
+
+@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{martin-lof,
+        AUTHOR  = {P. Martin-L\"{o}f},
+        TITLE   = {{Intuitionistic Type Theory}},
+        ADDRESS = {Napoli},
+        YEAR    = {1984},
+        PUBLISHER = {Bibliopolis}
+}
+@BOOK{curry,
+    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{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} }
+
+@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
+}
+
+@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{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}
+}
+
+
+@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{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{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}
+}
+
+
+@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 =	 {{LNCS/LNAI}},
+  volume =       {1955},
+  publisher =    {Springer},
+  pages =        {70--84}
+}
+
+@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} }
+
+
+
+@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 =         2002
+}
+
+@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{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
+}
+
+
+
+@PhdThesis{fiedler,
+  author =   {A. Fiedler},
+  title =   {{User-Adaptive Proof Explanation}},
+  school =   {{Universität des Saarlandes}},
+  year =   2001
+}
+
+@PhdThesis{peb,
+  author =   {P. Ljungl\"of},
+  title =   {{Grammatical Framework and Generalized Context-Free Grammars}},
+  school =   {{Dept.\ of Computing Science,
+               Chalmers University of Technology and 
+               Gothenburg University}},
+  year =   {forthcoming}
+}
+
+@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}
+  }
+
+@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}
+}
+
+@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{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}
+}
+
+@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
+}
+
+@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 =	 {},
+  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}
+}
+
+
+
+
+@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{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"
+}  
+
+@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
+}
+@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}
+}
+
+
+@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 = {???}
+ }
diff --git a/examples/gfcc/complin.tex b/examples/gfcc/complin.tex
index abb226617..30b4908ef 100644
--- a/examples/gfcc/complin.tex
+++ b/examples/gfcc/complin.tex
@@ -908,7 +908,7 @@ as an argument.
 
 Fortunately, it is easy to replace the generic, interpreting GF parser
 by a compiled LR(1) parser. GF supports the translation of a concrete
-syntax into the \empha{Labelled BNF} (LBNF) format \cite{lbnf}, 
+syntax into the \empha{Labelled BNF} (LBNF) format, %% \cite{lbnf}, 
 which in turn can be translated to parser generator code
 (Happy, Bison, or JavaCUP), by the BNF Converter \cite{bnfc}.
 The parser we are therefore using in the compiler is a Haskell