@STRING{fac = "Formal Aspects of Computing"}

@STRING{amai = "Annals of Mathematics and Artificial Intelligence"}

@STRING{jsl = "Journal of Symbolic Logic"}

@STRING{jsc = "Journal of Symbolic Computation"}

@STRING{jlc = "Journal of Logic and Computation"}

@STRING{jlp = "Journal of Logic Programming"}

@STRING{JFP = "The {J}ournal of {F}unctional {P}rogramming"}

@STRING{jar = "Journal of Automated Reasoning"}

@STRING{sl = "Studia Logica"}

@STRING{ipl = "Information Processing Letters"}

@STRING{tcs = "Theoretical Computer Science"}

@STRING{lnm = "Lecture Notes in Mathematics"}

@STRING{lncs = "LNCS"}

@STRING{lnai = "LNCS"}

@STRING{spv = "Springer-Verlag"}

@STRING{cacm = "Communications of the {ACM}"}

@STRING{jacm = "Journal of the {ACM}"}

@STRING{sc = "Soft Computing---A Fusion of Foundations, Methodologies

and Applications"}

@BOOK{ Kern88,

AUTHOR = {B.W. Kernighan and D.M. Ritchie},

TITLE = {{T}he {C} {P}rogramming {L}anguage},

SERIES = {},

VOLUME = {},

PUBLISHER = {Prentice-Hall, Englewood Cliffs, New Jersey, USA},

YEAR = 1988,

NOTE = {2nd edition},

CONTENTS = {Standard book on the programming language C.},

TOPICS = {Language Manuals,C}

}

@Article{zephyr,

author = "D. C. Wang and A. W. Appel and J. L. Korn and C. S. Serra",

title = {{The Zephyr Abstract Syntax Description Language}},

note = {{USENIX Association}},

year = 1997

}

@Article{metal,

author = "G. Kahn and B. Lang and B. Mélèse and E. Morcos",

title = "Metal: a formalism to specify formalisms",

journal = {Science of {C}omputer {P}rogramming},

year = 1983,

volume = 3,

pages = {151--188}

}

@InCollection{pentus,

author = "M. Pentus",

title = "Lambek grammars are context-free",

booktitle = {{LICS}, {Utrecht}, {The} {Netherlands}},

year = 1993,

pages = {35--42}

}

@ARTICLE{lambek,

AUTHOR = "J. Lambek",

TITLE = "The mathematics of sentence structure",

JOURNAL = {{American Mathematical Monthly}},

VOLUME = {65},

PAGES = {154-170},

YEAR = {1958}

}

@Article{bar-hillel,

author = "Y. Bar-Hillel",

title = "A quasi-arithmetical notation for syntactic description",

journal = {Language},

year = 1953,

volume = 29,

pages = {27-58}

}

@Book{rosetta,

author = {M.~T. Rosetta},

title = {Compositional Translation},

publisher = "Kluwer",

address = "Dordrecht",

year = 1994

}

@Book{lamport-latex,

author = {L. Lamport},

title = {{\LaTeX\ A Document Preparation System}},

publisher = {Addison-Wesley},

year = 1986

}

@Book{hopcroft,

author = {J. Hopcroft and J. Ullman},

title = {{Introduction to Automata Theory, Languages, and Computation}},

publisher = {Addison-Wesley},

year = 1979

}

@Book{jones-partial,

author = {N.D. Jones and C.K. Gomard and P. Sestoft},

title = {Partial Evaluation and Automatic Program Generation},

publisher = {Prentice-Hall},

year = 1993

}

@Article{frost,

author = "R. Frost and J. Launchbury",

title = "Constructing natural language interpreters

in a lazy functional language",

journal = {The {Computer} {Journal}},

year = 1989,

volume = 32,

number = 2,

pages = {108--121}

}

@Article{pereira,

author = {H.~D. Warren and F. Pereira},

title = {An Efficient Easily Adaptable System for Interpreting Natural

Language Queries},

year = {1982},

journal = {{Computational Linguistics}},

volume = 8,

pages = {110-122}

}

@Misc{bnfc,

author = "Markus Forsberg and Aarne Ranta",

title = "BNF Converter site",

howpublished = "Program and documentation,

\verb6http://www.cs.chalmers.se/~markus/BNFC/6",

documentURL = "\verb6http://www.cs.chalmers.se/~markus/BNFC/6",

year = 2002

}

@Misc{huet-sanskrit,

author = "G. Huet",

title = "Sanskrit site",

howpublished = "Program and documentation,

\verb6http://pauillac.inria.fr/~huet/SKT/6",

documentURL = "\verb6http://pauillac.inria.fr/~huet/SKT/index.html6",

year = 2000

}

@Misc{italiano,

author = "A. Ranta",

title = {1+n representations of {Italian} morphology},

howpublished = {Essays dedicated to {Jan von Plato}

on the occasion of his 50th birthday,

\verb6http://www.valt.helsinki.fi/kfil/jvp50.htm6},

documentURL = "\verb6http://www.valt.helsinki.fi/kfil/jvp50.htm6",

year = 2001

}

@Article{hudak,

author = "P. Hudak",

title = "Building domain-specific embedded languages",

journal = "{ACM} {Computing} {Surveys}",

year = 1996,

volume = 28,

number = 4

}

@Article{algol,

author = "P. Naur",

title = {{Revised Report of the Algorithmic Language Algol 60}},

journal = {{Comm.\ ACM}},

year = 1963,

volume = 6,

pages = {1--17}

}

@Book{bescherelle,

author = "Bescherelle",

title = "La conjugaison pour tous",

publisher = "Hatier",

year = 1997

}

@Book{shieber,

author = "S. Shieber",

title = {{An Introduction to Unification-Based Approaches to Grammars}},

publisher = "University of Chicago Press",

year = 1986

}

@BOOK{prawitz,

AUTHOR = "D. Prawitz",

TITLE = {{Natural Deduction}},

PUBLISHER = {Almqvist \& Wiksell},

ADDRESS = {Stockholm},

YEAR = {1965} }

@BOOK{CAML,

AUTHOR = "P. Weis and X. Leroy",

TITLE = {{Le langage Caml}},

PUBLISHER = {Dunod},

ADDRESS = "Paris",

YEAR = {1999}

}

@BOOK{ML,

AUTHOR = "R. Milner and M. Tofte and R. Harper",

TITLE = {{Definition of Standard ML}},

PUBLISHER = {MIT Press},

YEAR = {1990}

}

@BOOK{ML-wik,

AUTHOR = "{Wikstr\"{o}m}, {\AA ke}",

TITLE = "Functional Programming Using Standard ML",

PUBLISHER = {Prentice-Hall},

ADDRESS = {London},

YEAR = {1987} }

@Article{coquand-typecheck,

author = "T. Coquand",

title = "An Algorithm for Type Checking Dependent Types",

journal = "Science of {Computer} {Programming}",

year = 1996,

volume = 26,

pages = {167-177}

}

@Book{boehm,

author = "H. Barendregt",

title = {{The Lambda Calculus. Its Syntax and Semantics}},

publisher = "North-Holland",

year = 1981

}

@Article{hutton,

author = "G. Hutton",

title = "Higher-order functions for parsing",

journal = {J. Functional Programming},

year = 1992,

volume = 2,

number = 3,

pages = {323--343}

}

@InProceedings{wadler,

author = "P. Wadler",

title = "How to replace failure by a list of successes",

booktitle = {{Second International Conference on Functional

Programming Languages and Computer Architectures}},

series = lncs,

year = 1985,

address = spv

}

@InProceedings{jones-hudak,

author = "M. Jones and P. Hudak",

title = "Using Types to Parse Natural Language",

booktitle = {{Proceedings of the Glasgow Workshop on Functional Programming}},

series = {{LNCS}},

year = 1995,

address = spv

}

@Article{earley,

author = "J. Earley",

title = "An efficient context-free parsing algorithm",

journal = {Communications of the {ACM}},

year = 1970,

volume = 13,

number = 2,

pages = {94--102}

}

@InCollection{joshi,

author = "A. Joshi",

title = {Tree-Adjoining Grammars: How much context-sensitivity is required

to provide reasonable structural descriptions},

booktitle = {{Natural Language Parsing}},

year = 1985,

editor = "D. Dowty and L. Karttunen and A. Zwicky",

publisher = {Cambridge University Press},

pages = {206--250}

}

@Article{Wirth,

author = "N. Wirth",

title = "Program Development by Stepwise Refinement",

journal = "Communications of the ACM",

year = 1971,

volume = 14,

pages = {221--227}

}

@Article{GF-paper,

author = "A. Ranta",

title = {{Grammatical Framework: A Type-Theoretical Grammar Formalism}},

journal = JFP,

note = {To appear}

}

@Article{huet-zipper,

author = "G. Huet",

title = {The {Zipper}},

journal = JFP,

year = 1997,

volume = 7,

number = 5,

pages = {549--554}

}

@Article{huet-lang,

author = {G. Huet and B. Lang},

title = {Proving and applying program transformations expressed

with second-order patterns},

journal = {{Acta Informatica}},

year = 1978,

volume = 11

}

@Article{knuth-attr,

author = "D. Knuth",

title = "Semantics of Context-Free Languages",

journal = {Mathematical {Systems} {Theory}},

year = 1968,

volume = 2,

pages = {127--145}

}

@Article{LR,

author = {D. Knuth},

title = {On the translation of languages from left to right},

journal = {Information and {Control}},

year = 1965,

volume = 8,

pages = {607--639}

}

@InProceedings{luocall,

author = {Z. Luo and P. Callaghan},

title = {Mathematical Vernacular and Conceptual Well-Formedness in Mathematical

Language},

booktitle = {{Logical Aspects of Computational Linguistics (LACL)}} ,

year = 1999,

editor = {A. Lecomte and F. Lamarche and G. Perrier},

series = lnai,

volume = 1582,

pages = {231--250}

}

@Book{hpsg,

author = "C. Pollard and I. Sag",

title = {{Head-Driven Phrase Structure Grammar}},

publisher = {University of Chicago Press},

year = 1994

}

@ARTICLE{dcg,

AUTHOR = "F. Pereira and D. Warren",

TITLE = "Definite clause grammars

for language analysis---a survey of the formalism and a

comparison with augmented transition networks",

JOURNAL = {{Artificial Intelligence}},

VOLUME = {13},

PAGES = {231--278},

YEAR = {1980} }

@inproceedings{cayenne,

AUTHOR = {L. Augustsson},

TITLE = {{Cayenne---a language with dependent types}},

BOOKTITLE = {Proc. of {ICFP'98}},

PUBLISHER = {ACM Press},

MONTH = {September},

YEAR = {1998}

}

@book{nordstrom:book,

AUTHOR = {B. Nordstr{\"{o}}m and K. Petersson and J. M. Smith},

TITLE = {{Programming in Martin-Löf's Type Theory. An Introduction}},

YEAR = {1990},

PUBLISHER = {Oxford University Press}

}

@book{constable,

AUTHOR = {R. L. Constable},

TITLE = {{Implementing Mathematics with the NuPRL Proof Development System}},

YEAR = {1986},

PUBLISHER = {Prentice-Hall}

}

@book{martin-lof,

AUTHOR = {P. Martin-L\"{o}f},

TITLE = {{Intuitionistic Type Theory}},

ADDRESS = {Napoli},

YEAR = {1984},

PUBLISHER = {Bibliopolis}

}

@InProceedings{dymetman,

author = {M.\ Dymetman and V.\ Lux and A.\ Ranta},

title = {{XML} and Multilingual Document Authoring: Convergent Trends},

booktitle = {{COLING}, {Saarbr\"ucken}, {Germany}},

pages = {243--249},

year = {2000}

}

@InProceedings{GF-Alfa,

author = {T.\ Hallgren and A.\ Ranta},

title = {An Extensible Proof Text Editor},

editor = {M. Parigot and A. Voronkov},

booktitle = {{LPAR-2000}},

year = {2000},

series = {LNAI},

volume = {1955},

publisher = {Springer},

pages = {70--84}

}

@InProceedings{FASE,

author = {K.\ Johannisson and R.\ Hähnle and A.\ Ranta},

title = {An Authoring Tool for Informal and Formal Requirements Specifications},

booktitle = {{FASE}},

year = {2002},

series = {LNCS},

note = {To appear},

publisher = {Springer}

}

@Misc{Cactus,

author = {N. Martinsson},

title = {{Cactus (Concrete- to Abstract-syntax Conversion Tool with Userfriendly Syntax) }},

note = {\verb8http://www.mdstud.chalmers.se/~md6nm/cactus/8},

howpublished = "Master's Thesis in Computer Science",

address = "Chalmers University",

year = 2001

}

@Misc{haskell98-Cactus,

author = {T. Hallgren},

title = {{The Haskell 98 grammar in Cactus}},

note = {\verb6http://www.cs.chalmers.se/~hallgren/CactusExample/6},

address = "Chalmers University",

year = 2001

}

@Misc{GF-homepage,

author = {A. Ranta},

title = {{Grammatical Framework Homepage}},

note = {\verb6www.cs.chalmers.se/~aarne/GF/6},

url = "http://www.cs.chalmers.se/~aarne/GF/",

year = 2000

}

@Misc{happy,

author = {S. Marlow},

title = {{Happy, The Parser Generator for Haskell}},

note = {\verb6http://www.haskell.org/happy/6},

year = 2001

}

@Misc{latex,

author = {Donald Knuth},

title = {Latex},

note = {\verb6http://www.latex-project.org/6}

}

@Misc{cup,

author = {Scott E. Hudson},

title = {{CUP Parser Generator for Java}},

note = {\verb6http://www.cs.princeton.edu/~appel/modern/java/CUP/6},

year = 1999

}

@Misc{alex,

author = {C. Dornan},

title = {{Alex: a Lex for Haskell Programmers}},

note = {\verb6http://www.cs.ucc.ie/dornan/alex.html6},

year = 1997

}

@Misc{jlex,

author = {E. Berk and C. Ananian},

title = {{JLex: A Lexical Analyzer Generator for Java}},

note = {\verb6http://www.cs.princeton.edu/~appel/modern/java/JLex/6},

year = 2000

}

@inproceedings{magnusson-nordstr,

AUTHOR = {L. Magnusson and B. Nordstr\"{o}m},

BOOKTITLE = {{Types for Proofs and Programs}},

PUBLISHER = {Springer},

SERIES = {LNCS 806},

PAGES = {213--237},

TITLE = {The {ALF} proof editor and its proof engine},

YEAR = {1994}

}

@Book{Ranta94,

author = {A. Ranta},

title = {{Type Theoretical Grammar}},

publisher = {Oxford University Press},

year = {1994}

}

@Book{appel,

author = {A. Appel},

title = {{Modern Compiler Implementation in ML}},

publisher = {Cambridge University Press},

year = {1998}

}

@Misc{coq,

key = {Coq},

title = {Coq Homepage},

howpublished = {\verb6pauillac.inria.fr/coq/6},

documentURL = "http://pauillac.inria.fr/coq/",

year = 1999

}

@InProceedings{wysiwym,

author = {R. Power and D. Scott},

title = {Multilingual authoring using feedback texts},

booktitle = {{COLING}-{ACL}},

year = 1998

}

@PhdThesis{fudgets,

author = {M. Carlsson and T. Hallgren},

title = {{Fudgets---Purely Functional Processes with

applications to Graphical User Interfaces}},

school = {Department of Computing Science, Chalmers University

of Technology},

year = 1998,

documentURL = "http://www.cs.chalmers.se/~hallgren/Thesis/"

}

@article{harper-honsell,

AUTHOR = {R. Harper and F. Honsell and G. Plotkin},

TITLE = {{A Framework for Defining Logics}},

JOURNAL = {{JACM}},

VOLUME = {40},

NUMBER = {1},

YEAR = {1993},

PAGES = {143--184}

}

@InProceedings{CKT95,

author = "Y. Coscoy and G. Kahn and L. Thery",

title = "Extracting text from proofs",

series = lncs,

volume = "902",

pages = {109--123},

year = "1995",

booktitle = "Proc.\ {Second} {Int.} {Conf.} on

{Typed} {Lambda} {Calculi} and {Applications}",

editor = "M. Dezani-Ciancaglini and G. Plotkin"

}

@Book{WarmerKleppe99,

author = "J. Warmer and A. Kleppe",

title = "The Object Constraint Language: Precise Modelling with {UML}",

publisher = "Addison-Wesley",

year = "1999"

}

@InProceedings{HoltEwan99,

author = {Alexander Holt and Ewan Klein},

title = {A semantically-derived subset of {E}nglish for

hardware verification},

booktitle = {Proc.\ Ann.\ Meeting Ass.\ for

Comp.\ Ling.},

pages = {451--456},

year = {1999},

url = {http://www.ltg.ed.ac.uk/prosper/papers/holt-1999-sds/ps/}

}

@misc{bohlin-trindi,

author = {P. Bohlin and J. Bos and S. Larsson and

I. Lewin and C. Matheson and D. Milward},

year = 1999,

title = {Survey of Existing Interactive Systems},

note = {Trindi deliverable D1.3, Gothenburg University}

}

@Article{teitelbaum,

author = "T. Teitelbaum and T. Reps",

title = {The {Cornell} {Program} {Synthesizer}: a syntax-directed

programming environment},

journal = {Commun. {ACM}},

year = "1981",

volume = "24",

number = "9",

pages = {563-573}

}

@misc{haskell98,

author= {S. {Peyton Jones} and J. Hughes},

title={{Report on the Programming Language Haskell 98, a

Non-strict, Purely Functional Language}},

year=1999,

month={February},

howpublished={Available from \verb!http://www.haskell.org!}

}

@Manual{UML1.3-specification,

key = {UML 1.3},

title = {Unified Modelling Language Specification, version 1.3},

organization = {Object Modeling Group},

month = mar,

year = 2000,

url = {http://cgi.omg.org/cgi-bin/doc?formal/00-03-01.ps.gz},

note = {OMG document formal/00-03-01. {URL:}

\texttt{http://cgi.omg.org/cgi-bin/doc?formal/00-03-01.ps.gz}}

}

@TechReport{LBR00,

author = "G. T. Leavens and A. L. Baker and C. Ruby",

title = "Preliminary Design of {JML}: A Behavioral Interface

Specification Language for {Java}",

institution = "Iowa State University, Department of Computer

Science",

year = "2000",

number = "98-06i",

month = feb,

note = "URL: \texttt{ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz}",

url = "ftp://ftp.cs.iastate.edu/pub/techreports/TR98-06/TR.ps.gz"

}

@TechReport{johnson-yacc,

author = {S. C. Johnson},

title = {{Yacc --- yet another compiler compiler}},

institution = {{AT \& T Bell Laboratories, Murray Hill, NJ}},

year = {1975},

number = {{CSTR-32}}

}

@TechReport{hallgren-2000,

author = {T. Hallgren},

title = {The Correctness of Insertion Sort},

institution = {Chalmers University of Technology,

Department of Computer Science},

year = {2000},

note = {URL: \verb!http://www.cs.chalmers.se/~hallgren/Papers/insertion_sort.ps!}

}

@InProceedings{power-scott-1998,

author = {R. Power and D. Scott},

title = {Multilingual authoring using feedback texts},

booktitle = {COLING-ACL 98},

year = 1998,

address = {Montreal, Canada}

}

@InProceedings{coquand1999,

author = {C. Coquand and T. Coquand},

title = {Structured Type Theory},

booktitle = {Workshop on Logical Frameworkds and Meta-languages},

year = 1999,

address = {Paris, France}

}

@InProceedings{ranta-cooper,

author = {A. Ranta and R. Cooper},

title = {Dialogue Systems as Proof Editors},

booktitle = {{IJCAR}/{ICoS-3}},

year = 2001,

address = {{Siena}, {Italy}}

}

@InProceedings{curry,

AUTHOR = "H. B. Curry",

TITLE = "Some logical aspects of grammatical structure",

EDITOR = "Jakobson, Roman",

BOOKTITLE = {{Structure of Language and its

Mathematical Aspects: Proceedings of the Twelfth Symposium

in Applied Mathematics}},

PUBLISHER = {American Mathematical Society},

YEAR = {1963},

PAGES = {56-68}

}

@inproceedings{bengt-lena1995,

AUTHOR = {L. Magnusson and B. Nordstr\"{o}m},

BOOKTITLE = {{ Types for Proofs and Programs}},

PUBLISHER = {Springer-Verlag},

SERIES = {LNCS},

VOL = {806},

PAGES = {213-237},

TITLE = {{The ALF proof editor and its proof engine}},

ADDRESS = {Nijmegen},

YEAR = {1994}

}

@article{kay1996,

AUTHOR = {M. Kay},

TITLE = {{The Proper Place of Men and Machines in Language Translation}},

JOURNAL = {{Machine Translation}},

YEAR = {1996},

NUMBER = {},

PAGES = {}

}

@unpublished{boeing,

title = {{Boeing Simplified English Checker}},

author = {{The Boeing Company}},

howpublished = {Online document},

year = {2001},

note = {\verb!http://www.boeing.com/assocproducts/sechecker/!}

}

@unpublished{XML,

title = {{Extensible Markup Language (XML)}},

author = {{The World Wide Web Consortium}},

howpublished = {Online document},

year = {2000},

note = {\verb!http://www.w3.org/XML/!}

}

@unpublished{agda-homepage,

author = "C. Coquand",

title = "{{AGDA Homepage}}",

year = 1998,

howpublished = {Online document},

note = {\verb!http://www.cs.chalmers.se/~catarina/agda/!} ,

documenturl = "http://www.cs.chalmers.se/~catarina/agda/"

}

@InProceedings{coquand:stt-lfm99,

author = {C. Coquand and T. Coquand},

title = {Structured Type Theory},

booktitle = {Workshop on Logical Frameworkds and Meta-languages},

year = 1999,

address = {Paris, France},

month = {Sep}

}

@inproceedings{augustsson:cayenne,

AUTHOR = {L. Augustsson},

TITLE = {{Cayenne --- a language with dependent types}},

BOOKTITLE = {Proc. of the International Conference on Functional Programming (ICFP'98)},

PUBLISHER = {ACM Press},

MONTH = {September},

YEAR = {1998}

}

@PhdThesis{carlsson98:fudgets_thesis,

author = {M. Carlsson and T. Hallgren},

title = {{Fudgets --- Purely Functional Processes with

applications to Graphical User Interfaces}},

booktitle = {{Fudgets --- Purely Functional Processes with

applications to Graphical User Interfaces}},

school = {Department of Computing Science, Chalmers University

of Technology},

year = 1998,

address = {S-412 96 Göteborg, Sweden},

month = {March},

documentURL = "http://www.cs.chalmers.se/~hallgren/Thesis/"

}

@book{martin-lof:padova,

AUTHOR = {P. Martin-L\"{o}f},

TITLE = {{Intuitionistic Type Theory}},

ADDRESS = {Napoli},

YEAR = {1984},

PUBLISHER = {Bibliopolis}

}

@book{montague,

AUTHOR = {R.\ Montague},

TITLE = {{Formal Philosophy}},

ADDRESS = {New Haven},

YEAR = {1974},

NOTE = {Collected papers edited by R.\ Thomason},

PUBLISHER = {Yale University Press}

}

@misc{alfa-homepage,

author = {T. Hallgren},

year = {2000},

title = {{Home Page of the Proof Editor Alfa}},

howpublished = {\verb!http://www.cs.chalmers.se/~hallgren/Alfa/!},

documentURL = {http://www.cs.chalmers.se/~hallgren/Alfa/}

}

@InProceedings{ranta98:regexp,

author = {A. Ranta},

title = {A Multilingual Natural-Language Interface to Regular Expressions},

booktitle = {Proceedings of the International Workshop on Finite State

Methods in Natural Language Processing},

pages = {79--90},

year = 1998,

editor = {L. Karttunen and K. Oflazer},

address = {Ankara},

organization = {Bilkent University}

}

@Misc{maple-homepage,

author = {Waterloo Maple Inc.},

title = {{Maple Homepage}},

howpublished = {\verb!http://www.maplesof.com/!},

documentURL = "http://www.maplesof.com/",

year = 2000

}

@Misc{mathematica-homepage,

author = {Wolfram Research, Inc.},

title = {{Mathematica Homepage}},

howpublished = {\verb!http://www.wolfram.com/products/mathematica/!},

documentURL = "http://www.wolfram.com/products/mathematica/",

year = 2000

}

@Misc{coq-homepage,

author = {Coq Development Team},

title = {{Coq Homepage}},

howpublished = {\verb!http://pauillac.inria.fr/coq/!},

documentURL = "http://pauillac.inria.fr/coq/",

year = 1999

}

@TechReport{LEGO-homepage,

author = {Z. Luo and R. Pollack},

title = {{LEGO Proof Development System}},

institution = {University of {Edinburgh}},

year = 1992

}

@Misc{LEGO-new-homepage,

author = {D. Aspinall},

title = {{The LEGO Proof Assistant}},

howpublished = {\verb!http://www.dcs.ed.ac.uk/home/lego/!},

documentURL = "http://www.dcs.ed.ac.uk/home/lego/",

year = 1999

}

@Misc{Isabelle-homepage,

author = {Isabelle},

title = {{Isabelle Homepage}},

howpublished = {\verb!http://www.cl.cam.ac.uk/Research/HVG/Isabelle/!},

documentURL = "http://www.cl.cam.ac.uk/Research/HVG/Isabelle/index.html",

year = 2000

}

@TechReport{lesk-lex,

author = {M. E. Lesk},

title = {Lex --- a lexical analyzer generator},

year = {1975},

institution = {{Bell Laboratories, Murray Hill, N.J.}},

type = {Technical Report},

number = {39}

}

@Misc{Mizar-homepage,

author = {},

title = {{The Mizar Homepage}},

howpublished = {\verb!http://mizar.org/!},

documentURL = "http://mizar.org/",

year = 1999

}

@Misc{ALF-family-homepage,

author = {},

title = {{Implementation of Proof Editors}},

howpublished =

{\verb!http://www.cs.chalmers.se/ComputingScience/Research/Logic/!},

documentURL = "http://www.cs.chalmers.se/ComputingScience/Research/Logic/",

year = 1999

}

@incollection{deBruijn:MV,

TITLE = {{Mathematical Vernacular:

a Language for Mathematics with Typed Sets}},

AUTHOR = {N. G. de Bruijn},

EDITOR = {R. Nederpelt},

BOOKTITLE = {{Selected Papers on Automath}},

PUBLISHER = {North-Holland Publishing Company},

PAGES = {865--935},

YEAR = {1994}

}

@article{pereira-warren,

AUTHOR = "F. Pereira and D. Warren",

TITLE = "Definite Clause Grammars for Language Analysis",

JOURNAL = {Artificial {Intelligence}},

YEAR = {1980},

NUMBER = {13},

PAGES = {231--278}

}

@PhdThesis{coscoy:thesis,

author = {Y.\ Coscoy},

title = {Explication textuelle de preuves pour le calcul des

constructions inductives},

school = {{Universit\'e de Nice-Sophia-Antipolis}},

year = 2000

}

@InProceedings{coscoy:textproofs,

AUTHOR = {Y. Coscoy and G. Kahn and L. Th\'ery},

TITLE = {Extracting Text from Proof},

BOOKTITLE = {{Proceedings of the International Conference on Typed Lambda

Calculus and Applications (TLCA), Edinburgh}},

EDITOR = {M. Dezani and G. Plotkin},

SERIES = {Lecture Notes in Computer Science},

NUMBER = {902},

PUBLISHER = {Springer-Verlag},

YEAR = {1996}

}

@InProceedings{coscoy:explanation,

author = {Y. Coscoy},

title = {A natural language explanation of formal proofs},

booktitle = {Logical Aspects of Computational Linguistics},

pages = {149--167},

year = 1997,

editor = {C. {Retor\'e}},

address = {Heidelberg},

publisher = {Springer},

series = {Lecture Notes in Artificial Intelligence},

number= 1328

}

@inproceedings{ranta:torino,

AUTHOR = {A. Ranta},

TITLE = {Context-Relative Syntactic Categories

and the Formalization of Mathematical Text},

BOOKTITLE = {{Types For Proofs and Programs}},

EDITOR = {S. Berardi and M. Coppo},

SERIES = {Lecture Notes in Computer Science},

NUMBER = {1158},

PAGES = {231--248},

PUBLISHER = {Springer-Verlag},

YEAR = {1996}

}

@article{ranta:paris,

AUTHOR = {A. Ranta},

TITLE = {{Structures grammaticales dans le fran\c{c}ais math\'ematique}},

JOURNAL = {{Math\'ematiques, informatique et Sciences Humaines}},

YEAR = {1997},

NUMBER = {138, 139},

PAGES = {5--56, 5--36}

}

@article{kamp:drt,

AUTHOR = {H. Kamp},

TITLE = {{ A theory of truth and semantic representation}},

EDITOR = {{J. Groenendijk, T. Janssen, and M. Stokhof}},

BOOKTITLE = {{Formal Methods in the Study of Language, Part 1}},

YEAR = {1981},

PUBLISHER = {{Mathematisch Centrum, Amsterdam}},

PAGES = {277--322}

}

@PhdThesis{magnusson:phd,

author = {L. Magnusson},

title = {The Implementation of ALF - a Proof Editor based on

Martin-L\"of's Monomorphic Type Theory with Explicit

Substitution},

school = {Department of Computing Science, Chalmers University of

Technology and University of G\"oteborg},

year = {1994}

}

@InProceedings{krijo-aarne,

author = "K. Johannisson and A. Ranta",

title = "Formal Verification of Multilingual Instructions",

booktitle = "The Joint Winter Meeting of Computing Science and

Computer Engineering",

publisher = "Chalmers University of Technology",

year = "2001"

}