@BOOK{HarrisonThesis,
        author          = "John Harrison",
        title           = "Theorem Proving with the Real Numbers",
        publisher       = "Springer-Verlag",
        year            = 1998}

@inproceedings{HOL-light,
  author    = {John Harrison},
  title     = {HOL Light: A Tutorial Introduction.},
  booktitle = {FMCAD},
  year      = {1996},
  pages     = {265-269},
  crossref  = {DBLP:conf/fmcad/1996},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@article{IEEE754,
author="IEEE",
title = "{IEEE} Standard for Binary Floating-Point Arithmetic",
journal = "SIGPLAN Notices",
volume = 22,
number = 2,
pages = "9--25",
year= 1987
}

@inproceedings{DBLP:conf/ac/BentonHM00,
  author    = {Nick Benton and
               John Hughes and
               Eugenio Moggi},
  title     = {Monads and Effects.},
  booktitle = {APPSEM},
  year      = {2000},
  pages     = {42-122},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2395/23950042.htm},
  crossref  = {DBLP:conf/ac/2000appsem},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/fmcad/1996,
  editor    = {Mandayam K. Srivas and
               Albert John Camilleri},
  title     = {Formal Methods in Computer-Aided Design, First International
               Conference, FMCAD '96, Palo Alto, California, USA, November
               6-8, 1996, Proceedings},
  booktitle = {FMCAD},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {1166},
  year      = {1996},
  isbn      = {3-540-61937-2},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@Phdthesis{Niqui04,
author = "Milad Niqui",
title = "Formalising Exact Arithmetic: Representations, Algorithms and Proofs",
school = "Radboud University, Nijmegen",
year = 2004,
month = sep
}

@book{JMMuller,
  author = {Jean-Michel Muller},
  title = {Elementary Functions, Algorithms and implementation},
  publisher = {Birkhauser},
  year = 1997
}

@inproceedings{theryTPHOLs03,
 crossref = "tphols03",
 title = "Proving Pearl: Knuth's algorithm for prime numbers",
 author = "Laurent Th{\'e}ry"
}

@inproceedings{theryTPHOLs03short,
 editor = {David Basin and Burkhart Wolff},
 booktitle = {Theorem Proving in Higher Order Logics (TPHOLs 2003)},
 title = "Proving Pearl: Knuth's algorithm for prime numbers",
 author = "Laurent Th{\'e}ry",
 volume = 2758,
 series = {LNCS},
 publisher = {Springer-Verlag},
 year = 2003
}

@proceedings{tphols03,
 editor = {David Basin and Burkhart Wolff},
 booktitle = {Proceedings of the 16th International Conference on Theorem
    Proving in Higher Order Logics (TPHOLs 2003)},
 title = {Proceedings of the 16th International Conference on Theorem
    Proving in Higher Order Logics (TPHOLs 2003)},
 volume = 2758,
 series = {LNCS},
 publisher = {Springer-Verlag},
 year = 2003
}

@article{ BurstallDarlington77,
    author = "Rod M. Burstall and John Darlington",
    title = "A Transformation System for Developing Recursive Programs",
    journal = "Journal of the ACM",
    volume = "24",
    number = "1",
    pages = "44-67",
    year = "1977",
    url = "citeseer.ist.psu.edu/burstall77transformation.html" }


@InProceedings{Casteran2000,
  author         ="Pierre Cast\'eran and Davy Rouillard",
  title          = "Reasoning about Parametrized Automata",
  booktitle =    "Proceedings, 8-th International Conference on Real-Time System",
  volume =         "8",
  pages  =         "107-119",
  year   =         "2000",
}

@article{Coupet2003,
 author="Solange Coupet-Grimal",
 title="An axiomatization of Linear Temporal Logic in The Calculus of Inductive Constructions",
 journal="Journal of Logic and Computation",
 publisher = "Oxford University Press",
 year="2003",
 volume = 13,
 number = 6,
 pages = "801--813"
}

@MANUAL{Hudak92,
  AUTHOR       = {P. Hudak and S. Peyton Jones and P. Wadler and others},
  TITLE        = {{R}eport on the {P}rogramming {L}anguage {H}askell},
  ORGANIZATION = {Yale University},
  ADDRESS      = {New Haven, Connecticut, USA},
  EDITION      = {},
  YEAR         = 1992,
  NOTE         = {Version 1.2},
  CONTENTS     = {},
  TOPICS       = {Haskell,Language Manuals}
}

@inproceedings{BolDauThe03,
author = {Sylvie Boldo and Marc Daumas and Laurent Th{\'e}ry},
address = {Roma, Italy},
booktitle = {Proceedings of the 11th Symposium on the Integration of Symbolic Computation and Mechanized Reasoning},
title = {Formal proofs and computations in finite precision arithmetic},
year = 2003,
pages = {101-111},
url = {http://ftp.lip6.fr/lip6/reports/2003/lip6.2003.010.pdf} 
}


@ARTICLE{BolDauMorThe02,
  author =       {Sylvie Boldo and Marc Daumas and Claire Moreau-Finot
                  and Laurent Th{\'e}ry},
  journal =      {Journal of the ACM},
  title =        {Computer validated proofs of a toolset for adaptable
                  arithmetic},
  note =         {Submitted},
  url =          {http://arxiv.org/abs/cs.MS/0107025},
  year =         {2002}
}

@article{Russinoff99,
   author = "David M. Russinoff",
   title = "{A} {M}echanically {C}hecked {P}roof of {IEEE} {C}ompliance of the
            {AMD} {K5} {F}loating-{P}oint {S}quare {R}oot {M}icrocode",
   JOURNAL = "Formal Methods in System Design",
   YEAR = {1999},
   VOLUME = {14},
   NUMBER = {1},
   PAGES = {75--125},
   MONTH = {January}
}

@inproceedings{DauRidThe01,
  author =       {Marc Daumas and Laurence Rideau and Laurent
                  Th{\'e}ry},
  crossref = "tphols2001",
  title =        {A generic library of floating-point numbers and its
                  application to exact computing},
  pages =        {169-184},
}

@inproceedings{DauRidThe01short,
  author =       {Marc Daumas and Laurence Rideau and Laurent
                  Th{\'e}ry},
  title =        {A generic library of floating-point numbers and its
                  application to exact computing},
  pages =        {169-184},
        editor          = "Richard J. Boulton and Paul B. Jackson",
        booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 2001)",
        series          = "LNCS",
        volume          = 2152,
        year            = 2001,
        publisher       = "Springer-Verlag",
}

@inproceedings{DBLP:conf/mkm/Cruz-FilipeGW04,
  author    = {Lu\'{\i}s Cruz-Filipe and
               Herman Geuvers and
               Freek Wiedijk},
  title     = {C-CoRN, the Constructive Coq Repository at Nijmegen.},
  booktitle = {MKM},
  year      = {2004},
  pages     = {88-103},
  ee        = {http://springerlink.metapress.com/openurl.asp?genre=article{\&}issn=0302-9743{\&}volume=3119{\&}spage=88},
  crossref  = {DBLP:conf/mkm/2004},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/mkm/2004,
  editor    = {Andrea Asperti and
               Grzegorz Bancerek and
               Andrzej Trybulec},
  title     = {Mathematical Knowledge Management, Third International Conference,
               MKM 2004, Bialowieza, Poland, September 19-21, 2004, Proceedings},
  booktitle = {MKM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {3119},
  year      = {2004},
  isbn      = {3-540-23029-7},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@techreport{DauMorThe01,
  author =       {Daumas, Marc and Moreau-Finot, Claire and Thery,
                  Laurent},
  address =      {Le Chesnay, France},
  institution =  INRIA:INST,
  number =       4095,
  title =        {Computer validated proofs of a toolset for adaptable
                  arithmetic},
  type =         {Research report},
  year =         2001,
  crindex =      {Fichier},
  location =     {http://www.inria.fr/RRRT/RR-4095.html}
}

@INPROCEEDINGS{chicli03quotients,
  AUTHOR = {Chicli, Laurent and Pottier, Lo\"{\i}c and Simpson, Carlos},
  TITLE = {Mathematical quotients and quotient types in {Coq}},
  BOOKTITLE = {Types for Proofs and Programs},
  PAGES = {95-107},
  YEAR = 2003,
  EDITOR = {H. Geuvers and F. Wiedijk},
  NUMBER = 2646,
  SERIES = {LNCS},
  PUBLISHER = {Springer}
}


@book{Davie92,
  author = "Antony J. T. Davie",
  title = "An introduction to functional programming systems using {H}askell",
  series = "Cambridge Computer Science texts",
  publisher = "Cambridge University Press",
  year = 1992
}

@manual{Turner76,
  author = "David A. Turner",
  title = "{SASL} Language Manual",
  organization = "St. Andrews University Department of Computer Science",
  number = "Report TR/75/1, revised 1976",
  year = 1976
}
 
@book{coqart,
 title = " Interactive Theorem Proving and Program Development, Coq'Art:the Calculus of Inductive Constructions",
  author = "Yves Bertot and Pierre Cast{\'e}ran",
  year = 2004,
  publisher = "Springer-Verlag"
}

@book{Krivine,
title="Lambda Calcul, types et modèles",
author="Jean-Louis Krivine",
year=1990,
publisher="Masson"
}

@book{Girard,
title="Proofs and types",
author="Jean-Yves Girard and Yves Lafont and Paul Taylor",
year=1989,
publisher={Cambridge University Press},
}

@book{Lalement,
title="Logique, réduction, résolution",
author="René Lalement",
year=1990,
publisher="Masson"
}

@book{CousineauMauny98,
title="The Functional Approach to Programming",
author="Guy Cousineau and Michel Mauny",
year=1998,
publisher="Cambridge University Press"
}

@book{texbook,
title="The {\TeX}book",
author="Donald E. Knuth",
publisher="Addison-Wesley",
year=1993
}

@book{Thompson,
author="Simon Thompson",
title="Type Theory and functional Programming",
publisher="Addison-Wesley",
year = 1991
}

@book{sedgewick,
title = "Algorithms",
author = "Robert Sedgewick",
year = 1988,
publisher = "Addison-Wesley"
}

@Book{PreparataShamos1985,
  author =       {F.P. {\sc Preparata} et M.I. {\sc Shamos}},
  title =        {Computational Geometry : an introduction},
  publisher =    {Springer-Verlag},
  year =         {1985}
}


@Book{BoissonnatYvinec1998,
  author =       {Jean-Daniel Boissonnat and Mariette Yvinec},
  title =        "Algorithmic geometry",
  publisher =    "Cambridge University Press",
  year =         1995
}

@book{CormenLeisersonRivest1990,
  author = "Thomas H. Cormen and Charles E. Leiserson and Ronald L. Rivest", 
  title = "Introduction to algorithms",
  publisher = "MIT-Press",
  year=1990
}
  

@INPROCEEDINGS{tphols2000-Balaa,
        crossref        = "tphols2000",
        title           = "Fix-point Equations for Well-Founded Recursion in Type Theory",
        author          = "Antonia Balaa and Yves Bertot",
        pages           = "1--16"}

@inproceedings{tphols2002-BertotCaprettaDasBarman,
   author= "Yves Bertot and Venanzio Capretta and Kuntal Das Barman",
   title = "Type-theoretic functional semantics",
   booktitle = {Theorem Proving in Higher Order Logics (TPHOLS'02)},
   year = 2002,
   month = aug,
   location = "Hampton, Va",
  series = "LNCS",
  publisher = "Springer-Verlag",
  number = 2410
}

@INPROCEEDINGS{tphols2000-Barras,
        crossref        = "tphols2000",
        title           = "Programming and computing in {HOL}",
        author          = "Bruno Barras",
        pages           = "17--37"}

@INPROCEEDINGS{tphols2000-Berghofer,
        crossref        = "tphols2000",
        title           = "Proof terms for simply typed higher order logic",
        author          = "Stefan Berghofer and Tobias Nipkow",
        pages           = "38--52"}

@INPROCEEDINGS{tphols2000-Bhargavan,
        crossref        = "tphols2000",
        title           = "Routing Information Protocol in {HOL}/{SPIN}",
        author          = "Karthikeyan Bhargavan and Carl A. Gunter and Davor Obradovic",
        pages           = "53--72"}

@INPROCEEDINGS{tphols2000-Capretta,
        crossref        = "tphols2000",
        title           = "Recursive Families of Inductive Types",
        author          = "Venanzio Capretta",
        pages           = "73--89"}

@INPROCEEDINGS{tphols2000-Carreno,
        crossref        = "tphols2000",
        title           = "Aircraft Trajectory Modeling and Alerting Algorithm Verification",
        author          = "V{\'{\i}}ctor Carre{\~n}o and C{\'{e}}sar Mu{\~{n}}oz",
        pages           = "90--105"}

@INPROCEEDINGS{tphols2000-Colwell,
        crossref        = "tphols2000",
        title           = "Intel's Formal Verification Experience on the {W}illamette Development",
        author          = "Bob Colwell",
        pages           = "106--107"}

@INPROCEEDINGS{tphols2000-Denney,
        crossref        = "tphols2000",
        title           = "A Prototype Proof Translator from {HOL} to {C}oq",
        author          = "Ewen Denney",
        pages           = "108--125"}

@INPROCEEDINGS{tphols2000-Dubois,
        crossref        = "tphols2000",
        title           = "Proving {ML} Type Soundness Within {C}oq",
        author          = "Catherine Dubois",
        pages           = "126--145"}

@INPROCEEDINGS{tphols2000-Fleuriot,
        crossref        = "tphols2000",
        title           = "On the Mechanization of Real Analysis in {I}sabelle/{HOL}",
        author          = "Jacques D. Fleuriot",
        pages           = "146--162"}

@INPROCEEDINGS{tphols2000-Geuvers,
        crossref        = "tphols2000",
        title           = "Equational Reasoning via Partial Reflection",
        author          = "H. Geuvers and F. Wiedijk and J. Zwanenburg",
        pages           = "163--179"}

@INPROCEEDINGS{tphols2000-Gordon,
        crossref        = "tphols2000",
        title           = "Reachability programming in {HOL} using {BDD}s",
        author          = "Michael J.~C.~Gordon",
        pages           = "180--197"}

@INPROCEEDINGS{tphols2000-Gottliebsen,
        crossref        = "tphols2000",
        title           = "Transcendental Functions and Continuity Checking in {PVS}",
        author          = "Hanne Gottliebsen",
        pages           = "198--215"}

@INPROCEEDINGS{tphols2000-Grundy,
        crossref        = "tphols2000",
        title           = "Verified Optimizations for the {I}ntel {IA-64} Architecture",
        author          = "Jim Grundy",
        pages           = "216--233"}

@INPROCEEDINGS{tphols2000-Harrison,
        crossref        = "tphols2000",
        title           = "Formal verification of {IA-64} division algorithms",
        author          = "John Harrison",
        pages           = "234--251"}

@INPROCEEDINGS{tphols2000-Hickey,
        crossref        = "tphols2000",
        title           = "Fast Tactic-based Theorem Proving",
        author          = "Jason Hickey and Aleksey Nogin",
        pages           = "252--266"}

@INPROCEEDINGS{tphols2000-Hofmann,
        crossref        = "tphols2000",
        title           = "Implementing a Program Logic of Objects in a Higher-Order Logic Theorem Prover",
        author          = "Martin Hofmann and Francis Tang",
        pages           = "267--282"}

@INPROCEEDINGS{tphols2000-Holmes,
        crossref        = "tphols2000",
        title           = "A Strong and Mechanizable Grand Logic",
        author          = "M. Randall Holmes",
        pages           = "283--300"}

@INPROCEEDINGS{tphols2000-Huisman,
        crossref        = "tphols2000",
        title           = "Inheritance in Higher Order Logic: Modeling and Reasoning",
        author          = "Marieke Huisman and Bart Jacobs",
        pages           = "301--319"}

@INPROCEEDINGS{tphols2000-Jackson,
        crossref        = "tphols2000",
        title           = "Total-Correctness Refinement for Sequential Reactive Systems",
        author          = "Paul B. Jackson",
        pages           = "320--337"}

@INPROCEEDINGS{tphols2000-Kaivola,
        crossref        = "tphols2000",
        title           = "Divider circuit verification with model checking and theorem proving",
        author          = "Roope Kaivola and Mark D. Aagaard",
        pages           = "338--355"}

@INPROCEEDINGS{tphols2000-Kerboeuf,
        crossref        = "tphols2000",
        title           = "Specification and Verification of a Steam-Boiler with {S}ignal-{C}oq",
        author          = "Micka{\"e}l Kerb{\oe}uf and David Nowak and Jean-Pierre Talpin",
        pages           = "356--371"}

@INPROCEEDINGS{tphols2000-Laibinis,
        crossref        = "tphols2000",
        title           = "Functional Procedures in Higher-Order Logic",
        author          = "Linas Laibinis and Joakim von Wright",
        pages           = "372--386"}

@INPROCEEDINGS{tphols2000-Letouzey,
        crossref        = "tphols2000",
        title           = "Formalizing {S}t{\aa}lmarck's algorithm in {C}oq",
        author          = "Pierre Letouzey and Laurent Th{\'e}ry",
        pages           = "387--404"}

@INPROCEEDINGS{tphols2000-Lueth,
        crossref        = "tphols2000",
        title           = "{TAS} --- A Generic Window Inference System",
        author          = "Christoph L{\"u}th and Burkhart Wolff",
        pages           = "405--422"}

@INPROCEEDINGS{tphols2000-Merz,
        crossref        = "tphols2000",
        title           = "Weak Alternating Automata in {I}sabelle/{HOL}",
        author          = "Stephan Merz",
        pages           = "423--440"}

@INPROCEEDINGS{tphols2000-Milner,
        crossref        = "tphols2000",
        title           = "Graphical theories of interactive systems: can a proof assistant help?",
        author          = "Robin Milner",
        pages           = "441"}

@INPROCEEDINGS{tphols2000-Mokkedem,
        crossref        = "tphols2000",
        title           = "Formal verification of the {A}lpha 21364 network protocol",
        author          = "Abdel Mokkedem and Tim Leonard",
        pages           = "442--460"}

@INPROCEEDINGS{tphols2000-Pollack,
        crossref        = "tphols2000",
        title           = "Dependently Typed Records for Representing Mathematical Structure",
        author          = "Robert Pollack",
        pages           = "461--478"}

@INPROCEEDINGS{tphols2000-Reus,
        crossref        = "tphols2000",
        title           = "Towards a Machine-Checked {J}ava Specification Book",
        author          = "Bernhard Reus and Tatjana Hein",
        pages           = "479--496"}

@INPROCEEDINGS{tphols2000-Slind,
        crossref        = "tphols2000",
        title           = "Another Look at Nested Recursion",
        author          = "Konrad Slind",
        pages           = "497--517"}

@INPROCEEDINGS{tphols2000-Wos,
        crossref        = "tphols2000",
        title           = "Automating the Search for Answers to Open Questions",
        author          = "Larry Wos and Branden Fitelson",
        pages           = "518--532"}

@PROCEEDINGS{tphols2000,
        editor          = "J. Harrison and M. Aagaard",
        booktitle = "Theorem Proving in Higher Order Logics:
                           13th International Conference, TPHOLs 2000",
        title       = "Theorem Proving in Higher Order Logics:
                           13th International Conference, TPHOLs 2000",
        series          = "Lecture Notes in Computer Science",
        volume          = 1869,
        year            = 2000,
        publisher       = "Springer-Verlag"}

@inproceedings{Richardson95,
  author = "Julian Richardson",
  title= "Automating Changes of Data Type in Functional Programs",
  booktitle = "Proceedings of KBSE-95",
  publisher = "IEEE Computer Society",
  year = 1995
}

@INPROCEEDINGS{Boutin97b,
  title = {Using reflection to build efficient and certified decision procedures},
  author = {S. Boutin},
  booktitle = {TACS'97},
  editor = {Martin Abadi and Takahashi Ito},
  publisher = {LNCS, Springer-Verlag},
  volume = {1281},
  year = {1997},
}

@inproceedings{PichardieBertot01,
crossref= "tphols2001",
 title = "Formalizing Convex Hull Algorithms",
author = "David Pichardie and Yves Bertot",
pages = "346--361",
}

@inproceedings{PichardieBertot01short,
        editor          = "Richard J. Boulton and Paul B. Jackson",
        booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 2001)",
        series          = "LNCS",
        volume          = 2152,
        year            = 2001,
        publisher       = "Springer-Verlag",
 title = "Formalizing Convex Hull Algorithms",
author = "David Pichardie and Yves Bertot",
pages = "346--361",
}

@inproceedings{capretta:2001,
  crossref   = "tphols2001",
  author     = "Venanzio Capretta",
  title      = "Certifying the Fast Fourier Transform with Coq",
  pages      = "154--168"
}


@article{BoveUnif,
  title = "Simple General Recursion in Type Theory",
  author = "Ana Bove",
  journal = "Nordic Journal of Computing",
  volume = 8,
  number = 1,
  pages = "22-42",
  year = 2001
}

@INPROCEEDINGS{letouzey2002types,
  AUTHOR = {Pierre Letouzey},
  TITLE = {A New Extraction for {Coq}},
  TOPICS = {team},
  CROSSREF = {types02}
}

@PROCEEDINGS{types02,
  TITLE = {Types for Proofs and Programs
Second International Workshop, TYPES 2002, Berg en Dal, The Netherlands, April 24-28, 2002, Selected Papers},
  BOOKTITLE = {TYPES 2002},
  YEAR = 2003,
  EDITOR = {Herman Geuvers and Freek  Wiedijk},
  VOLUME = 2646,
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer-Verlag}
}
@InProceedings{bove:tutorial,
  author =    {A. Bove},
  title =     {General Recursion in Type Theory},
  booktitle = {Types for Proofs and Programs, 
               International Workshop TYPES 2002, The Netherlands},
  pages =     {39--58},
  year =      {2003},
  editor =    {H. Geuvers and F. Wiedijk},
  number =    {2646},
  series =    {Lecture Notes in Computer Science},
  month =     {March},
}

@inproceedings{BoveCapretta01,
crossref = "tphols2001",
title = "Nested General Recursion and Partiality in Type Theory",
author = "Ana Bove and Venanzio Capretta",
pages = "121--135"
}


@PROCEEDINGS{tphols2001,
        editor          = "Richard J. Boulton and Paul B. Jackson",
        booktitle = "Theorem Proving in Higher Order Logics:
                           14th International Conference, TPHOLs 2001",
        title       = "Theorem Proving in Higher Order Logics:
                           14th International Conference, TPHOLs 2001",
        series          = "Lecture Notes in Computer Science",
        volume          = 2152,
        year            = 2001,
        month           = sep,
        publisher       = "Springer-Verlag"}

@inproceedings{Madden,
title ="The specialization and transformation of constructive existence proofs",
author= "Peter Madden",
booktitle= "Proceedings of the Eleventh International Joint Conference on Artificial Intelligence",
pages = "131--148",
publisher = "Morgan Kaufmann",
year = 1989,
editor = "N.S. Sridharan",
}

@inproceedings{Qian99,
author="Z. Qian",
title="A formal specification of {Java} {Virtual} machine instructions
for objects, methods, and subroutines",
booktitle="Formal Syntax and Semantics of Java",
volume=1523,
series="Lecture Notes in Computer Science",
publisher="Springer-Verlag",
year=1999
}


@inproceedings{boutin97,
title= "Using reflection to build efficient and certified decision procedures",
author="Samuel Boutin",
booktitle = "Theoretical Aspects of Computer Science",
editors = "T. Ito and M. Abadi",
series = "Lecture Notes in Computer Science",
number = 1281,
publisher = "Springer-Verlag",
year = 1997
}

@inproceedings{Goldberg98,
title="A specification of {Java} loading and bytecode verification",
author="A. Goldberg",
booktitle="Proceedings of 5th ACM Conference on Computer and Communication
Security",
year=1998
}

@inproceedings{Callahn99,
author="R. O'Callahn",
title="A simple, comprehensive type system for Java bytecode subroutines",
booktitle="ACM Symposium on Principles of Programming Languages",
pages="70--78",
publisher="ACM Press",
year=1999
}

@inproceedings{NuprlRecursive,
   author= {Robert L. Constable and Nax P. Mendler},
   title={Recursive definitions in type theory},
   booktitle={Logics of {P}rograms},
   editor= "Rohit Parikh",
   pages="61--78",
   location="Brooklyn",
   month=jun,
   year=1985,
   publisher= "Springer Verlag",
   series= "{LNCS}",
   volume=193
}

@misc{Kahn-geom,
  author = "Gilles Kahn",
  title = "Elements of Constructive Geometry Group Theory and Domain Theory",
  year = 1995,
  note = "available as a Coq user contribution at {\tt http://coq.inria.fr\-/contribs-eng.html}"
}

@misc{BertotPons:Graphs,
  author = "Yves Bertot and Olivier Pons",
  title = {Dependency graphs in theorem provers},
  year = 2000,
  note = {To appear as INRIA Research Report, also visible as http://www-sop.inria.fr/lemme/graphs/}
}
  
@inproceedings{FreundMitchell98,
  author = {Stephen N. Freund and John C. Mitchell},
   title = {{A Type System for Object Initialization in the Java Bytecode
             Language}},
  booktitle = "ACM Conference on Object-Oriented Programming:
               Systems, Languages, and Applications",
  month = oct,
  year = 1998
}

@article{MW99,
  author = "Erica Melis and Jon Whittle",
  title = "Analogy in inductive theorem proving",
  journal = "Journal of Automated Reasoning",
  volume = 22,
  pages = "117--147",
  year = 1999
}

@misc{MPFR,
  author = "Guillaume Hanrot and Vincent Lef{\`e}vre and Patrick P{\'e}lissier and Paul Zimmermann",
  title = "The MPFR Library",
  year = 2000,
  note = "available at {\tt http://www.mpfr.org}"
}

@article{SQRT02,
  author = "Yves Bertot and Nicolas Magaud and Paul Zimmermann",
  title = "A proof of {GMP} square root",
  journal = "Journal of Automated Reasoning",
  volume = 22,
  number = "3--4",
  pages = "225--252",
  year = 2002
}

@article{FreundMitchell2000,
  author = {Stephen N. Freund and John C. Mitchell},
   title = {{A Type System for Object Initialization in the Java Bytecode
             Language}},
  journal = {ACM Transactions on Programming Languages and Systems},
  month = sep,
  year = 2000,
}
  
@inproceedings{FreundMitchell99,
  author= {Stephen N. Freund and John C. Mitchell},
  title ={{A Formal Framework for the Java Bytecode Language and Verifier}},
  booktitle="ACM Conference on Object-Oriented Programming: Systems, Languages
             and Applications",
  month=nov,
  year=1999
}

@ARTICLE{PaulinWerner93,
  author = {Christine Paulin-Mohring and Benjamin Werner},
  journal = {Journal of Symbolic Computation},
  title = {{Synthesis of ML programs in the system Coq}},
  volume = {15},
  year = {1993},
  pages = {607--640}
}

@phdthesis{huisman2001,
  author = "Marieke Huisman",
  title = "Java program verification in Higher-order logic with PVS and Isabelle",
  school = {University of Nijmegen},
  year = 2001
}

@PHDTHESIS{coquand-th,
  author = {Thierry Coquand},
  title = {Une th\'eorie des {C}onstructions},
  school= {Universit\'e de {Paris} {VII}},
  year = 1985
}

@article{coquand-huet,
  author = {Thierry Coquand and G\'erard Huet},
  title = {{The Calculus of Constructions}},
  journal = "Information and Computation",
  volume = 76,
  year = 1988
}


@article{PRESS,
   title = "Using Meta-level Inference for Selective Application of Multiple
            Rewrite Rule Sets in Algebraic Manipulation",
   author= "Alan Bundy and Bob Welham",
   journal = "Artificial Intelligence",
   volume = 16,
   year = 1981,
   pages = "189--212"
}

@inproceedings{Parent95,
   author = "Catherine Parent",
   title = "Synthesizing proofs from programs in the {C}alculus of {I}nductive
           {C}onstructions",
   booktitle = "Mathematics of {P}rogram {C}onstruction",
   location = "Kloster Irsee, Germany",
   year = 1995,
   month = jul,
   volume = 947,
   publisher = "Springer-Verlag",
   series = "Lecture Notes in Computer Science"
}

@article{thery01,
  author = "Laurent Th{\'e}ry",
title = "A Machine-Checked Implementation of {B}uchberger's Algorithm",
  journal = "Journal of Automated Reasoning",
  volume = 26,
  pages = "107--137",
  year = 2001
}

@inproceedings{thery98,
   author = "Laurent Th{\'e}ry",
   title = "A certified version of {B}uchberger's algorithm",
   booktitle = "Automated Deduction ({CADE-15})",
   location = "Passau, Germany",
   year = 1998,
   month = jul,
   series = "Lecture Notes in Artificial Intelligence",
   publisher = "Springer-Verlag",
   volume = 1421
}

@article{OppenPretty,
  title = "Prettyprinting",
  author = "Derek C. Oppen",
  journal = "ACM Transactions on Programming Languages and Systems",
  volume = 2,
  number = 4,
  year = 1980,
  pages = "465--483"
}

@article{rippling,
   title = "Rippling: a Heuristic for Guiding Inductive Proofs",
   author = "Alan Bundy and A. Stevens and F. van Harmelen and Andrew Ireland 
             and Alan Smaill",
   journal = "Artificial Intelligence",
   year = 1993,
   volume = 62,
   number = 2,
   pages = "185--253"
}

@inproceedings{Anderson,
 author = "Penny Anderson",
 title = "Representing proof transformations for program optimization",
 booktitle = "International Conference on Automated Deduction",
 volume = 814,
 series = "LNAI",
 publisher = "Springer-Verlag",
 year = 1994
}

@InProceedings{PrettypLangRepNestStruct,
   author = "R. J. Boulton",
   title = "A Pretty-Printer Specification Language with Support for
            Repetitive Nested Structures",
   booktitle = "Proceedings of the International Conference on
                Technical Informatics (ConTI'94)",
   year = "1994",
   volume = "5",
   pages = "226--235",
   address = "Timi\c{s}oara, Romania",
   month = "November"}

@InProceedings{MorcosConchon,
  author = "Elham Morcos-Chounet and Alain Conchon",
  title = "PPML: A general formalism to specify pretty-printing",
  booktitle = "Information Processing 86 (Proceedings of IFIP Congress)",
  location = "Dublin",
  year = 1986,
  publisher = "IFIP, Elservier Science Publishers B.V. (North-Holland)",
  editor= "H.-J. Kugler"
}

@phdthesis{Ritchie:thesis,
        author = {Brian Ritchie},
        title = "The design and implementation of an interactive proof
                  editor",
        school = {{U}niversity of {E}dinburgh},
        year = 1988
}


@article{Caferra95,
   title = "A Generic Graphic Framework for Combining Inference Tools
                  and Editing Proofs and Formulae",
   author = "Ricardo Caferra and Michel Herment",
   journal = "{J}ournal of {S}ymbolic {C}omputation ",
   volume = 19,
   pages = "217--243",
   year = 1995
}


@book{ousterhout94,
  title= "Tcl and the Tk Toolkit",
  author = "John K. Ousterhout",
  publisher = "Addison-Wesley",
  series = "Professional Computing series",
  year = 1994,
}

@article{mathspad,
   title = "MathSpad: a system for on-line preparation of mathematical documents",
   author = "Roland C. Backhouse and Richard Verhoeven and O. Weber",
   journal = "Software -- Concepts and Tools",
   volume = 18,
   pages = "80--89",
   year = 1997
}

@techreport{Barwise90,
   title = "The language of First-Order Logic",
   author = "Jon Barwise and John Echemendy",
   Institution = "Centre for the Study of Language and Information",
   year = 1990
}

@techreport{Jape,
   title = "Jape: a literal, lightweight, interactive proof assistant",
   author = "Richard Bornat and Bernard Sufrin",
   type = "Technical Report",
   number = 641,
   institution = "Queen Mary and Westfield College, University of London",
   year = 1994
}

@techreport{leroy95,
title ="Le système Caml Special Light: modules et compilation efficace en Caml",
author = "Xavier Leroy",
number= "RR-2721",
year = 1995,
institution = "INRIA"
}

@techreport{bertot98,
  author = "Yves Bertot",
  title = "A certified compiler for an imperative language",
  type = "Research Report",
  number = "RR-3488",
  institution = "INRIA",
  year = 1998
}

@inproceedings{BartheCourtieu,
  author = 	 {Gilles Barthe and Pierre Courtieu},  
  title = {{Efficient reasoning about executable specifications in Coq}},
  booktitle={Proceedings of TPHOLs'02},
  editor={V. Carreño and C. Muñoz and S. Tahar},
  series="Lecture Notes in Computer Science",  
  year = {2002},
  Publisher="Springer-Verlag",
  volume={2410},
  pages={31--46}}

@inproceedings{g+01:esop,
   author = 	 {G. Barthe and G. Dufay and L. Jakubiec and S. Melo
                   de Sousa and B. Serpette},
   title = 	 {{A Formal Executable Semantics of the JavaCard Platform}},
   year = 	 {2001}
, Booktitle={Proceedings of ESOP'01}
, Publisher={Springer-Verlag}
, series= {LNCS}
, volume= {2028}
, Editor= {D. Sands}
, pages={302--319}}


@techreport{bertot00,
  author = "Yves Bertot",
  title = "A Coq Formalization of a
      Type Checker for Object Initialization
      in the Java Virtual Machine",
  type = "Research Report",
  number = "RR-4047",
  institution = "INRIA",
  year = 2000
}

@techreport{Zimmermann99,
  author = "Paul Zimmermann",
  title = "Karatsuba Square Root",
  type = "Research Report",
  number = "RR-3805",
  institution = "INRIA",
  year = 1999
}

@inproceedings{bertot00a,
  author = "Yves Bertot",
  title = "Formalizing a JVML Verifier for Initialization in a Theorem Prover",
  pages = "14--24",
  volume = 2102,
  year = 2001,
  series = "LNCS",
  publisher = "Springer-Verlag",
  booktitle = "Computer Aided Verification (CAV'2001)"
}

@techreport{CtCoqManual,
  author= "Janet Bertot and Yves Bertot and Yann Coscoy and Healfdene
           Goguen and Francis Montagnac",
  title = "User Guide to the {CtCoq} Proof Environment",
  type = "Rapport technique",
  institution = "INRIA",
  number = "RT0210",
  year = 1997,
  URL = "http://www.inria.fr/RRRT/RT-0210.html"
}

@techreport{bertot97a,
  author= "Yves Bertot",
  title = "Programming Language Specifications and Environments",
  type = "Rapport technique",
  institution = "INRIA",
  number = "RT0212",
  year = 1997,
  URL = "http://www.inria.fr/RRRT/RT-0212.html"
}

@techreport{RideauTheryCtCaml,
  title = "Interactive Programming Environment for ML",
  author = "Laurence Rideau and Laurent Th{\'e}ry",
  type = "Rapport de Recherche",
  institution = "INRIA",
  number = "RR-3139",
  year = 1997,
  month = Mar
}

@book{Stoy77,
title = "Denotational Semantics --- The scott-Starchey Apprach to language theory",
author = "Joseph E. Stoy",
publisher = "MIT Press",
location = "Cambridge, Ma",
year = 1977
}

@book{KnuthAxiomsHulls,
  author = "Donald Knuth",
  title = "Axioms and Hulls",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  number = 606,
  year = 1991
}


@book{chou94,
  author = "S.C. Chou and X.S. Gao and J.Z. Zhang", 
  title = "Machine Proofs in Geometry",
  publisher =  "World Scientific, Singapore",
  year =  "1994"
}

@MISC{hales-flyspeck,
  AUTHOR = {Hales, Thomas},
  TITLE = {The Flyspeck Project Fact Sheet},
  year = 2004,
  NOTE = {\\http://www.math.pitt.edu/\~{}thales/flyspeck/index.html},
  URL = {http://www.math.pitt.edu/~thales/flyspeck/index.html}
}

@article{Hales00,
  author = "Thomas C. Hales",
  title = "Cannonballs and Honeycombs",
  journal = "Notices of the AMS",
  publisher = {American Mathematical Society},
  year = 2000,
  volume = 47,
  number = 4,
  pages = "440-449"
}

@inproceedings{RantaHallgren2000,
author="Thomas Hallgren and Aarne Ranta",
title={An Extensible Proof Text Editor},
booktitle="Logic for Programming and Automated Reasoning",
volume="1955",
series="LNCS",
publisher="Springer Verlag",
year = 2000,
pages = "70--84"
}

@inproceedings{puitg-dufourd1998,
  author = "Fran\c{c}ois Puitg and Jean-Fran\c{c}ois Dufourd",
  title = "Formal Specification and Theorem Proving Breakthroughs in Geometric
           Modeling",
  booktitle = "Theorem Proving in Higher-Order Logics",
  year = "1998",
  series = "Lecture Notes in Computer Science",
  volume= 1479,
  publisher = "Springer-Verlag",
  pages = "410--422",
}

@article{plato1998,
 author = "Jan von Plato",
 title = "A constructive theory of ordered affine geometry",
 journal = "Indagationes Mathematicae",
 volume = 9,
 year = 1998,
 pages = "549--562"
}

@article{prisme-3316a,
 author =  "Pierre Alliez and Olivier Devillers and Jack  Snoeyink",
 title =       "Removing Degeneracies by Perturbing the Problem or the World",
 journal =     "Reliable Computing",
 note = "Special Issue on Computational Geometry",
 volume =      6,
 year =        2000,
 pages =       "61--79"
}

@techreport{BKS,
title= "Implementing Proof by Pointing without a Structure Editor",
author = "Yves Bertot and Thomas Kleymann-Schreiber and Dilip Sequeira",
type = "Technical Report",
                  institution={University of Edinburgh},
                  number = "ECS-LFCS-97-368",
                  note = "également rapport de recherche INRIA 3286",
                  year = 1997,
                  URL = "http://www.inria.fr/RRRT/RR-3286.html"
}

@inproceedings{Suppes84,
   author = "Patrick Suppes",
   title = {The Next Generation of Interactive Theorem Provers},
   booktitle = "Automated Deduction ({CADE-7})",
   location = "Napa, California, USA",
   year = 1984,
   month = may,
   series = "Lecture Notes in Computer Science",
   volume = 170,
   publisher = "Springer-Verlag"
}


@inproceedings{Kajler:CASPI,
   author = "Norbert Kajler",
   title = "{CAS/PI}: A Portable and Extensible Interface for Computer
                  Algebra System",
   booktitle = "International Symposium on Symbolic and Algebraic
                  Computation ({ISSAC'92})",
   publisher = "ACM",
   pages = "376--386",
   location = "Berkeley, California",
   year = 1992
}

@inproceedings{TacticSimplification,
    author = "Yves Bertot",
    title = "Head-Tactics Simplification",
    booktitle = "Algebraic Methodology and Software Technology",
    publisher = "Springer Verlag",
    series = "Lecture Notes in Computer Science",
    volume = 1349,
    location = "Sydney, Australia",
    year = 1997
}

            
@inproceedings{Opons97,
        AUTHOR = {Olivier Pons},
        TITLE = {Undoing and Managing a proof},
        BOOKTITLE = {Electronic Proceedings of "User Interfaces for Theorem Provers 
1997"},
        ADDRESS = {Sophia-Antipolis, France},
        DATE = Sep,
        YEAR =  1997,
        URL={http://www.inria.fr\-/croap/\-events/\-uitp97-papers.html}
}

@inproceedings{Eastaughffe98,
        author = {Katherine Eastaughffe},
        title = {Support for Interactive Theorem Proving: Some design principles
                 and their application},
       BOOKTITLE = {Informal Proceedings of "User Interfaces for Theorem Provers 1998"},
       ADDRESS= {Eindhoven University of Technology},
       DATE = Jul,
       YEAR = 1998
}        

@inproceedings{Pons98,
       AUTHOR = {Olivier Pons and Yves Bertot and Laurence Rideau},
       TITLE = {Notions of dependency in proof assistants},
       BOOKTITLE = {User Interfaces for Theorem Provers 1998},
       ADDRESS= {Eindhoven University of Technology},
       DATE = Jul,
       YEAR = 1998
}


@book{Mural,
    author="C.B. Jones and K.D. Jones and P.A. Lindsay and R. Moore",
    title="MURAL: A Formal Development Support System",
    publisher="Springer-Verlag",
    year=1991
}

@inproceedings{WadlerForest,
    author = "Philip Wadler",
    title = "Deforestation: Transforming Programs to Eliminate Trees",
    booktitle = "European Symposium on Programming (ESOP'88)",
    editor = "Harald Ganzinger",
    pages="344--358",
    location = "Nancy",
    month = mar,
    year = 1988,
    publisher = "Springer Verlag",
    series = "{LNCS}",
    volume = 300
}


@@inproceedings{windowinference,
title = "Window Inference in the {HOL} System",
author = "Jim Grundy",
booktitle = "Proceedings of the International Workshop on the HOL Theorem
Proving System and its applications",
location = "Davis, California",
year = 1991,
month = {August},
publisher = "{IEEE} Computer Society Press",
pages = "177-189",
}

@inproceedings{DamasMilner,
  title= "Principal type-schemes for functional programs",
  author = "Lu{\'{\i}}s Damas and Robin Milner",
  booktitle = "ninth {ACM} symposium on {P}rinciples of {P}rogramming {L}anguages",
  publisher = "{ACM}",
  year = 1982,
  pages = "207-212"
}

@book{MLdef,
  title = "The Definition of Standard ML",
  author = "Robin Milner and Mads Tofte and Robert Harper",
  year = 1990,
  publisher = "MIT Press",
  note = "ISBN 0-262-63132-6"
}

@book{Emacs,
  title = "Learning {GNU} {E}macs",
  author = {Debra Cameron and Bill Rosenblatt},
  year = 1991,
  publisher = {O'Reilly \& Associates, Inc.}
}

@inproceedings{reasonningexecutable,
  title = "{R}easoning with {E}xecutable {S}pecifications",
  author = "Yves Bertot and Ranan Fraer",
  volume = 915,
  pages = "531--545",
  location = "Aarhus, Denmark",
  year = 1995,
  series = "Lecture Notes in Computer Science",
  journal = "Springer-Verlag LNCS",
  booktitle = "Proceedings of the International Joint Conference on Theory
		  and Practice of Software Development (TAPSOFT'95)"
}

@inproceedings{Inversion,
  author = "Christina Cornes and Delphine Terrasse",
  title = "Automatizing Inversion of Inductive Predicates in Coq",
  booktitle = "Types for Proofs and Programs",
  location = "Torino",
  volume = 1158,
  series = "Lecture Notes in Computer Science",
  publisher = "Springer-Verlag",
  year = 1995
}
		  
@inproceedings{Huang:assertion,
author = "X. Huang",
year = 1994,
title = "Reconstructing proofs at the assertion level",
volume = 814,
series = "Lecture Note in Artificial Intelligence",
publisher = "Springer-Verlag",
booktitle = "CADE-12"
}

@misc{DuboisDonzeau1998,
  author = "Catherine Dubois and V{\'e}ronique Vigui{\'e} Donzeau-Gouge",
  title = "A step towards the mecha\-ni\-zation of partial functions: domains as inductive predicates",
  booktitle = "Electronic Proceedings to the CADE-workshop on Mechanization of partial functions",
  note = "{\tt www.cs.bham.ac.uk\-/\~{\ }mmk/cade98-partiality}",
  month = jul,
  year = 1998
}

@inproceedings{Aczel77,
title = "An introduction to inductive definitions",
year= 1977,
editor = "J. Barwise",
author = "Peter Aczel",
publisher = "North Holland",
volume = "90",
series = "Studies in Logic and the Foundations of Mathematics",
booktitle = "{H}andbook of {M}athematical {L}ogic"
}

@article{nordstrom88,
 author = {Bengt Nordstr\"{o}m},
 title = {Terminating General Recursion},
 journal = {BIT},
 volume = 28,
 pages = "605--619",
 year = 1988
}

@inproceedings{magnussonnordstrom:alf,
	AUTHOR = {Lena  Magnusson and Bengt Nordstr\"{o}m},
	BOOKTITLE = {{ Types for Proofs and Programs}},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes Computer Science},
	VOLUME = {806},
        PAGES = {213--237},
	TITLE	= {{The ALF proof editor and its proof engine}}, 
        ADDRESS = {Nijmegen},
	YEAR = {1994}
	}


@phdthesis{magnusson:thesis,
	AUTHOR = {Lena Magnusson},
	TITLE	= {{The Implementation of ALF - a Proof Editor based
	on Martin-L\"{o}f's Monomorphic Type Theory with Explicit Substitution}},
	SCHOOL = {Department of Computing Science, G\"{o}teborg
	University and Chalmers University of Technology},
	ADDRESS = {G\"{o}teborg, Sweden},
	MONTH = {January},
	YEAR = {1995}
}

@article{Clement:DistributedEnvironment,
  author = "Dominique {Clément}",
  title =  "A Distributed Architecture for Programming Environments",
  note = "{\sl Proceedings of the 4th Symposium on Software Development
		  Environments}",
  location = "Irvine, California",
  year = 1990,
  journal =  "Software Engineering Notes",
  volume = 15,
  number = 5
}

@inproceedings{ClementMontagnacPrunet:IntegratedComponents,
  author = "Dominique {Clément} and Francis Montagnac and Vincent
		  Prunet",
  title = "Integrated Software Components: a Paradigm for Control
	Integration",
  booktitle = "Proceedings of the European Symposium on Software Development
Environments and {CASE} Technology",
  location = "{Königswinter}", 
  series = "Lecture Notes in Computer Science",
  volume =  509,
  year = 1991,
  month = "June"
}

@inproceedings{CassetLanet99,
title="How to formally specify the Java Byte code semantics using the B method",
author="Ludovic Casset and Jean-Louis Lanet",
booktitle="proceedings of the Workshop on Formal Techniques for Java Programs at
{ECOOP 99}",
month=jun,
url="http://www.gemplus.fr/smart/r_d/publications/art13.htm",
year=1999
}

@book{Paulson:Isabelle,
  title = "Isabelle : a generic theorem prover",
  author = "Lawrence C. Paulson and Tobias Nipkow",
  publisher = "Springer-Verlag",
  series = "Lecture Notes in Computer Science",
  volume = 828,
  year = 1994
}

@book{Paulson:ML,
  title = "{ML} for the working programmer",
  author = "Lawrence C. Paulson",
  publisher = "Cambridge University Press",
  year = 1991
}

@book{Paulson:programmingML,
  title = "{ML} for the working programmer",
  author = "Lawrence C. Paulson",
  publisher = "Cambridge University Press",
  year = 1991
}

@article{Paulson-Inductive,
  author = "Lawrence C. Paulson",
  title = "Mechanizing Coinduction and Corecursion in Higher-order Logic",
  journal = "Journal of Logic and Computation",
  volume = 7,
  month = mar,
  year = 1997,
  pages = "175--204"
}

@article{VLISP,
   title = "Special issue on {VLISP}",
   author = "Joshua D. Guttman and Mitchell Wand (eds.)",
   publisher = "Kluwer Academic Publishers",
   journal = "Lisp and Symbolic Computation",
   year = 1995,
   Volume = 8,
   number = "1/2"
}

@article{Moore89,
  title = "A Mechanically Verified Language Implementation",
  author = "J Strother Moore",
  publisher = "Kluwer Academic Publishers",
  journal = "Journal of Automated Reasoning",
  volume = 5,
  pages = "461--492",
  year = 1989
}

@article{Young89,
  title = "A Mechanical Verified Code Generator",
  author = "William D. Young",
  publisher = "Kluwer Academic Publishers",
  journal = "Journal of Automated Reasoning",
  volume = 5,
  pages = "493--518",
  year = 1989
}

@inproceedings{filliatre98,
  author = {Jean-Christophe Filli{\^a}tre},
  title = {Proof of Imperative Programs in Type Theory},
  booktitle = {International Workshop {TYPES'98}},
  location = {Kloster Irsee, Germany},
  volume = 1657,
  series = {Lecture Notes in Computer Science},
  publisher = {Pringer-Verlag},
  month = mar,
  year = 1998
}

@INPROCEEDINGS{CoPa89,
  author = {Thierry Coquand and Christine Paulin-Mohring},
  booktitle = {Proceedings of Colog'88},
  editor = {P. Martin-L{\"o}f and G. Mints},
  series = {Lecture Notes in Computer Science},
  volume = {417},
  publisher = {Springer-Verlag},
  title = {Inductively defined types},
  year = {1990},
}

@INPROCEEDINGS{Moh93,
  author = {Christine Paulin-Mohring},
  booktitle = {Proceedings of the conference Typed Lambda Calculi and
  Applications},
  editor = {M. Bezem and J.-F. Groote},
  institution = {LIP-ENS Lyon},
  note = {LIP research report 92-49},
  number = {664},
  series = {Lecture Notes in Computer Science},
  title = {{Inductive Definitions in the System {Coq} - Rules and
            Properties}},
  type = {research report},
  year = {1993},
}

@inproceedings{HannanPfenning,
  title = "Compiler verification in LF",
  author = "John Hannan and Frank Pfenning",
  booktitle = "Seventh Annual IEEE Symposium on Logic in Computer Science",
  pages = "407--418",
  location = "Santa Cruz, Cal",
  year = 1992
}

@inproceedings{CoquandPersson98,
  title = "Gr{\"o}bner Bases in Type Theory",
  author = "Thierry Coquand and Henrik Persson",
  booktitle = "Types'98",
  publisher = "Springer-Verlag",
  series = {Lecture Notes in Computer Science},
  volume = {1658},
  year = 1998
}

@INPROCEEDINGS{PfPa89,
  author = {Frank Pfenning and Christine Paulin-Mohring},
  booktitle = {Proceedings of Mathematical Foundations of Programming Semantics},
  note = {technical report CMU-CS-89-209},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {442},
  title = {Inductively defined types in the {Calculus of Constructions}},
  year = {1990},
}

@inproceedings{sisal96,
  title = "Optimizing Sisal Programs: a formal approach",
  author = "Isabelle Attali and Denis Caromel and Romain Guider and Andrew L. Wendelborn",
  booktitle = "Euro-Par'96: International Conference on Parallel Processing",
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {1123},
  location = "Lyon",
  year = 1996,
  month = Aug
}

@techreport{martin-lof,
  title = "An Intuitinistic Theory of Types",
  author = "Per Martin-L{\"o}f",
  institution = "University of stockholm",
  year = 1972
}

@inproceedings{AbadiStataJvm,
  title = "A Type System for {J}ava Bytecode Subroutines",
  author = " Raymie Stata and Mart{\'\i}n Abadi",
  booktitle = "Proceedings of the 25th Annual ACM Symposium on Principles of
               Programming Languages",
  publisher = "{ACM} Press",
  location = "San Diego (CA)",
  year = 1998,
  month = jan,
  pages = "149--160"
}

@incollection{Oheimb-NipkowJava-LNCS,
  author = "Oheimb, David von and Nipkow, Tobias",
  title = "Machine checking the {J}ava Specification: Proving Type-Safety",
  booktitle = {Formal Syntax and Semantics of {J}ava},
  editor = {Jim Alves-Foss},
  url = {http://www.in.tum.de/~isabelle/bali/doc/Springer98.html},
  publisher = {Springer},
  series = {LNCS},
  year = 1998,
  note = {To appear},
}

@techreport{Boutin-ML,
  title = "Preuve de correction de la compilation de min-{ML} en code {CAM} dans
           le syst{\`e}me d'aide {\`a} la d{\'e}monstration {COQ}",
  author = "Boutin, Samuel",
  year = 1995,
  type = "Rapport de recherche",
  institution = "INRIA",
  number = "RR2536",
  month = apr
}

@book{ACL2book,
title="Computer-aided reasoning: an approach",
author="Matt Kaufmann and Panagiotis Manolios and J. Strother Moore",
publisher="Kluwer Academic Publishing",
year=2000,
isbn="0-7923-7744-3",
url="http://www.cs.utexas.edu/users/moore/acl2"
}

@inproceedings{nqthm,
   author = "Robert S. Boyer and J Strother Moore",
   title = "A Theorem Prover for a Computational Logic",
   publisher = "Springer-Verlag",
   series = "Lecture Notes in Computer Science",
   number = 449,
   year = 1990,
   month = jul,
   booktitle = "10th Conference on Automated Deduction"
}

@article{Eiffel96,
  title = "A Natural Semantics for {Eiffel} Dynamic Binding",
  author = "Isabelle Attali and Denis Caromel and Sidi Ould Ehmety",
  journal = "{ACM} Transactions on Programming Languages and Systems",
  volume = 18,
  number = 5,
  year = 1996,
  month = nov
}

@inproceedings{vis-par-OO96,
  title = "Semantics-Based Visualization of Parallel Object-Oriented Programming",
  author = "Isabelle Attali and Denis Caromel and Sidi Ould Ehmety and Sylvain Lippi",
  booktitle = "Object Oriented Programming: Systems, Languages, and Applications ({OOPSLA}'96)",
  publisher = "ACM Press",
  series = "Sigplan Notices",
  number = "31(10)",
  location = "San Jose, Ca",
  month = oct,
  year = 1996
}

@article{realinterfaces,
  title = "{R}eal {T}heorem {P}rovers {D}eserve {R}eal {U}ser-{I}nterfaces",
  author = "Laurent {Th\'ery} and Yves Bertot and Gilles Kahn",
  note = "Proceedings of the 5th Symposium on Software Development Environments",
  location = "Tyson's Corner, Virginia",
  year = 1992,
  journal = "Software Engineering Notes",
  volume = 17,
  number = 5
}

@TechReport{LuoPollack92,
  author = 	"Zhaohui Luo and Robert Pollack",
  title = 	"{LEGO} Proof Development System: User's Manual",
  institution = "LFCS, Computer Science Dept., University of Edinburgh",
  year = 	1992,
  number = 	"ECS-LFCS-92-211",
  address = 	"The King's Buildings, Edinburgh EH9 3JZ",
  month = 	"May",
  note = 	"Updated version.  Available by anonymous ftp with
		  {LEGO} distribution"
}

@article{hascoet88,
  author = "Laurent Hasco{\"et}",
  title = "Partial evaluation with inference rules",
  note = "Selected Papers of the Workshop on Partial Evaluation
          and Mixed Computation, Gammel Averneas, Denmark",
  editor = "Dines Bj{\"o}rner and Andrei P. Ershov and Neil D. Jones",
  journal = "New Generation Computing Journal",
  volume = "6 (2 \& 3)",
  pages = "187--209",
  year = 1988
}

@inproceedings{hascoet88b,
   author = "Laurent Hasco{\"et}",
   title = "A tactic-driven system for building proofs",
   booktitle = "actes du 7e S{\'e}minaire de Programmation en
      Logique",
   location = "Tr\'egastel, France",
   year = 1988,
   note = "also INRIA Research Report 770 (1987)"
}

@inproceedings{Syme:TkHOL95,
  author = "Donald Syme",
  title = "A New Interface for HOL - Ideas, Issues, and
                  Implementation", 
  booktitle = "Higher Order Logic Theorem Proving and Its
                  Applications: 8th International Workshop",
  location =  "Aspen Grove, Utah",
  year = 1995,
  month = sep,
  series = "Lecture Notes in Computer Science",
  publisher = "Springer-Verlag",
  volume = "971",
  pages = "324--339",
}

@inproceedings{BKT,
  author = "Yves Bertot and Gilles Kahn and Laurent Th\'ery",
  title = "Proof by Pointing",
  booktitle = "{T}heoretical {A}spects of {C}omputer {S}oftware",
  location = "Sendai, Japan",
  series = "Lecture Notes in Computer Science",
  volume = "789",
  pages = "141--160",
  year = 1994
}

@book{winskel93,
   title = "The Formal Semantics of Programming Languages, an 
            introduction",
   author = "Glynn Winskel",
   publisher = "The MIT Press",
   year = 1993,
   series = "Foundations of Computing"
}

@inbook{metal,
   title = "Centaur 1.2",
   editor = "Ian Jacobs and Janet Bertot",
   chapter = "The Metal Manual",
   publisher = "Inria Sophia--Antipolis",
   year = 1993
}

@inbook{TYPOL1.2,
   title = "Centaur 1.2",
   editor = "Ian Jacobs and Janet Bertot",
   chapter = "The Typol Manual",
   publisher = "Inria Sophia--Antipolis",
   year = 1993
}

@inproceedings{Typol,
   title = "{E}xecutable {S}pecifications of {S}tatic {S}emantics",
   author = "Thierry Despeyroux",
   booktitle = "{I}nternational {S}ymposium on {S}emantics of {D}ata {T}ypes",
   year = 1984,
   publisher = "Springer-Verlag",
   Volume = 173,
   Series = "Lecture Notes in Computer Science",
}

@techreport{StanfordVerifier,
  author = "{Stanford Verifier Group}",
  title = "Stanford Pascal Verifier User Manual",
  institution = "Stanford Verification Group",
  number = 11,
  year = 1979
}

@inproceedings{McCarthyPainter,
  author = "John {McCarthy} and James Painter",
  title = "correctness of a compiler for arithmetic expressions",
  booktitle = "Mathematical Aspects of Computer Science 1",
  year = 1967,
  series = "Proceedings of Symposia in Applied Mathematics",
  volume = 19}

@inproceedings{Slind96,
  author = "Konrad Slind",
  title = "Function definition in higher order logic",
  booktitle = "Theorem {P}roving in {H}igher {O}rder {L}ogics",
  volume = 1125,
  series = "Lecture Notes in Computer Science",
  location = "\aAbo, Finland",
  year = "1996",
  month = aug,
  publisher = "Sprinter {V}erlag"
}

@inproceedings{Melham-Inductive,
  title = "A Package for Inductive Relation Definitions in {HOL}",
  Author = "Thomas F. Melham",
  booktitle = "Proceedings of the 1991 International Workshop on the {HOL}
      Theorem Proving system and its Applications",
  Location = "Davis",
  publisher = "IEEE Computer Society Press",
  pages = "350--357",
  year = 1992
}
@inbook{PPML,
   title = "Centaur 1.2",
   editor = "Ian Jacobs and Janet Bertot",
   chapter = "The PPML Manual",
   publisher = "Inria Sophia--Antipolis",
   year = 1993
}

@inproceedings{ia89,
   title = "Compiling TYPOL with Attribute Grammars",
   author = "Isabelle Attali",
   booktitle = "International Worksop on Programming Language Implementation and
                Logic Programming",
   location = "{Orl\'eans}, France",
   year = 1988,
   publisher = "Springer Verlag LNCS",
   month = "May"
}

@inproceedings{jd86,
   title = "Proof of Translation in Natural Semantics",
   author = "{Jo\"{e}lle} Despeyroux",
   booktitle = "Symposium on Logic in Computer Science",
   location = "Cambridge, Massachusetts",
   year = 1986,
   pages = "193--205",
   publisher = "IEEE Computer Society",
   month = "June"
}




@inproceedings{Natural,
   author = "Gilles Kahn",
   title = "{N}atural {S}emantics", 
   booktitle = "{P}rogramming of {F}uture {G}eneration {C}omputers",
   editor = "K. Fuchi and Maurice Nivat",
   publisher = "North-Holland",
   year = 1988,
   note = "(also appears as INRIA Report no. 601)"
}

@manual{Mathplus,
   title = "Math {P}lus, {L}earning guide and {R}eference manual",
   organization = "Waterloo Maple Sofware",
   year = 1995
}

@manual{Occam,
   title = "{OCCAM} {P}rogramming {M}anual",
   organization = "INMOS Limited",
   note = "{P}rentice {H}all",
   year = 1984
}

@inproceedings{bertot91,
   author = "Yves Bertot",
   title = "{O}ccurrences in {D}ebugger {S}pecifications",
   booktitle = "{ACM} {SIGPLAN} {C}onference on {P}rogramming {L}anguage {D}esign
                and {I}mplementation",
   location = "Toronto, Canada",
   year = 1991
}

@inproceedings{bertot92,
   author = "Yves Bertot",
   title = "{O}rigin {F}unctions in {$\lambda$-calculus}
                and {T}erm {R}ewriting {S}ystems",
   booktitle = "{CAAP'92}",
   location = "Rennes, France",
   note = "Springer Verlag LNCS 581",
   year = 1992
}

@inproceedings{fraer96,
   author = "Ranan Fraer",
   title = "Tracing the Origins of Verification Conditions",
   booktitle = "Algebraic Methodology and Software Technology",
   location = "Munich, Germany",
   publisher = "Springer Verlag",
   series = "{LNCS}",
   volume = 1101,
   year = 1996
}

@inproceedings{Orthogonal,
   author = "Luc Maranget",
   title = "{O}ptimal {D}erivations in {W}eak {L}ambda-{C}alculi
                and in {O}rthogonal {T}erms {R}ewriting {S}ystems",
   booktitle = "{P}rinciples {O}f {P}rogramming {L}anguages",
   location = "Orlando, Florida",
   year = 1991
}

@book{abrial96,
   title = "The B-Book. Assigning Programs to Meanings",
   author = "Jean-Raimond Abrial",
   publisher = "Cambridge University Press",
   year = 1996
}

@inproceedings{floyd66,
   title = "Assigning Meanings to Programs",
   author = "Robert W. Floyd",
   editor = "J. T. Schwartz",
   booktitle = "Mathematical Aspects of Computer Science : 19th
        symposium on Applied Mathematics",
   pages = "19--31",
   location = "Providence, United States",
   year = 1966
}

@book{Gentzen,
   author = "M. E. Szabo",
   title = "The Collected papers of {G}erhard {G}entzen",
   publisher = "North-Holland",
   year = 1969
}

@inproceedings{Substitutions,
   author = "Martin Abadi and Luca Cardelli and Pierre-Louis Curien and
                Jean-Jacques L\'evy",
   title = "Explicit Substitutions",
   booktitle = "{P}rinciples {O}f {P}rogramming {L}anguages",
   location = "San Francisco, California",
   year = 1990
}


@article{despeyroux:theo,
title = "Theo: an interactive proof development system",
author = "Jo{\"e}lle Despeyroux",
journal = "{S}candinavian {J}ournal on {C}omputer {S}cience and
{N}umerical {A}nalysis, {BIT}",
volume = 32,
pages = "15--29",
year = 1992
}

		  
@article{klint93,
   title = "A Meta-environment for Generating Programming
            Environments",
   author = "Paul Klint",
   journal = "ACM Transaction on Software Engineering and
              Methodology",
   volume = 2,
   pages = "176--201",
   year = 1993
}
 


@article{deursen93,
   title = "{O}rigin {T}racking",
   author = "Arie van Deursen and Paul Klint and Franz Tip",
   journal = "{J}ournal of {S}ymbolic {C}omputation ",
   volume = 15,
   pages = "523--545",
   year = 1993,
   note = "Special issue on automatic programming"
}

@book{dijkstra76,
   title = "A discipline of Programming",
   author = "Edsger W. Dijkstra",
   publisher = "Prentice Hall",
   year = 1976
}

@article{hoare69,
   title ="An Axiomatic Basis for Computer Programming",
   author = "Charles Anthony Richard Hoare",
   journal = "Communications of the ACM",
   month = oct,
   year = 1969,
}

@phdthesis{deursenPhD,
   title = "{E}xecutable {L}anguage {D}efinitions",
   author = "Arie van Deursen",
   school = "{U}niversity of {A}msterdam",
   year = 1994,
}


@ARTICLE{CtCoqDesign,
TITLE="The {CtCoq} System: Design and Architecture",
author="Yves Bertot",
journal="Formal Aspects of Computing",
volume=11,
pages="225--243",
year=1999
}

@ARTICLE{Esterel:BerryGonthier,
TITLE = "The {Esterel} Synchronous Programming Language: 
         Design, Semantics, Implementation",
AUTHOR =  "G. Berry and G. Gonthier",
JOURNAL = "Science Of Computer Programming",
VOLUME = 19,
NUMBER = 2,
YEAR = 1992,
PAGES = "87--152"
}

@ARTICLE{BerryLevy,
TITLE = "Minimal and Optimal Computations of Recursive Programs",
AUTHOR =  "G. Berry and J.-J. {L\'evy}",
JOURNAL = "Journal of the Assocation for Computing Machinery",
VOLUME = 26,
NUMBER = 1,
YEAR = 1979,
PAGES = "148--175"
}

@book{Supercompilers,
   author = "H. Zima and B. Chapman",
   title = "Supercompilers for Parallel and Vector Computers",
   series = "Frontier Series",
   publisher = "{ACM} Press",
   year = 1990
}

@phdthesis{Optimal,
   author = "Jean-Jacques {L\'evy}",
   title = "{R\'eductions} {C}orrectes et {O}ptimales dans le {L}ambda-{C}alcul",
   school = "University of Paris VII",
   year = 1978
}



@inproceedings{Inductive-Coq,
   title = "Inductive Definitions in the System Coq: Rules and Properties",
   author = "Christine Paulin-Mohring",
   booktitle = "Typed Lambda Calculi and Applications",
   location = "Utrecht, the Netherlands",
   editor = "Mark Bezem and Jan-Friso Groote",
   year = 1993,
   pages = "328--345",
   publisher = "Springer-Verlag",
   series = "{LNCS}",
   volume = 664,
   month = "March"
}

@techreport{DeryRideau:MessageProtocol,
   title = "Distributed programming Environments: an example of
		  message protocol",
   author = "Anne-Marie {Déry} and Laurence Rideau",
   type = "Rapport Technique",
   number = 165,
   institution = "INRIA",
   year = 1994
}

@techreport{PVS:Tutorial,
   title = "A Tutorial on Specification and Verification Using {PVS}",
   author = "Natarajan Shankar and Sam Owre and John M. Rushby",
   institution = "Computer Science Laboratory, SRI International,
		  Menlo Park, CA",
   note = "(Beta Release)",
   year = 1993
}

@techreport{Camilleri-Melham,
   title = "Reasoning with Inductively Defined Relations in the {HOL}
            Theorem Prover",
   author = "Juanito Camilleri and Tom Melham",
   type = "Technical Report",
   institution = "University of Cambridge",
   year = 1992
}

@unpublished{TYPOL-Coq,
   title = "Traduction from {TYPOL} to {Coq}",
   author = "Delphine Terrasse",
   note = "to appear as an INRIA Report",
   year = 1994
}

@phdthesis{Automatisation,
   title = "{U}ne {A}utomatisation du {C}alcul des {R}\'esidus en {S}\'emantique
           {N}aturelle",
   author = "Yves Bertot",
   school = "University of Nice-Sophia Antipolis",
   year = 1991,
   note = "(In french)"
}

@inproceedings{pbp,
  author = "Yves Bertot and Gilles Kahn and Laurent Th\'ery",
  title = "{P}roof by {P}ointing",
  booktitle = "{I}nternational {S}ymposium on {T}heoretical {A}spects of
               {C}omputer {S}cience",
  location = "Sendai, Japan",
  year = 1994
}

@book{Synte,
author = {Tom W. Reps  and Tim Teitelbaum},
year = 1988,
title = "The {Synthesizer} generator : a system for constructing 
                language-based editors",
publisher = "Springer-Verlag"}


@phdthesis{InterfacesDistribuees,
  author = "Laurent Th\'ery",
  title = "Une m\'ethode distribu\'ee de cr\'eation d'interfaces et ses
           applications aux d\'emonstrateurs de th\'eor\`emes",
  school = "University of Paris VII",
  year = 1994,
}

		  
@phdthesis{TerrassePhD,
  author = "Delphine Terrasse",
  title = "Vers un Environnement d'Aide au D\'eveloppement de Preuves
           en S\'emantique Naturelle",
  school = {Ecole Nationale des Ponts et Chauss\'ees},
  year = 1995,
}

@phdthesis{Curien,
  author = "R{\'e}gis Curien",
  title = "Outils pour la preuve par analogie",
  school = {Universit{\'e} Henri Poincar{\'e}, Nancy I,},
  year = 1995
}

@inproceedings{Canonical,
  author = "Yves Bertot",
  title = "{A} {C}anonical {C}alculus of {R}esiduals",
  booktitle = "Logical Environments",
  publisher = "Cambridge University Press",
  editor = "{G\'erard} Huet and Gordon Plotkin",
  pages = "147--163",
  year = 1993,
  note = "(Also appears as INRIA Report no. 1542, Oct. 1991)"
}

@inproceedings{jd94,
   title = "Higher-order Syntax with Induction in {Coq}",
   author = "{Jo\"{e}lle} Despeyroux and {Andr\'e} Hirshowitz",
   booktitle = "Fifth International Conference on Logic Programming and Automated
                Reasonning",
   location = "Kiev, Ukraine",
   year = 1994
}

@manual{Centaur1.2,
   title = "Centaur 1.2",
   organization = "INRIA",
   year = 1993
}

@inproceedings{Centaur,
   title = "Centaur: the system",
   author = "Patrick Borras and Dominique {Clément} and Thierry
		  Despeyroux and Janet Incerpi and Gilles Kahn and
		  Bernard Lang and {Valérie} Pascual",
   booktitle = "Third Symposium on {S}oftware {D}evelopment {E}nvironments",
   location = "Boston, Massachusetts",
   year = 1988,
   note = "(Also appears as INRIA Report no. 777)"
}

@inproceedings{Confluent,
   author = "{Th\'er\`ese} Hardin and Jean-Jacques {L\'evy}",
   title = "{A} {C}onfluent {C}alculus of {S}ubstitutions",
   booktitle = "{F}rance-{J}apan {A}rtificial {I}ntelligence and {C}omputer
                {S}cience {S}ymposium",
   location = "Izu, Japan",
   year = 1989
}


@inproceedings{Esterel,
   author = "{G\'erard} Berry and Laurent Cosserat",
   title = "{T}he synchronous {P}rogramming {L}anguage {ESTEREL} and its
                 {M}athematical {S}emantics",
   booktitle = "Seminar on Concurrency",
   publisher = "Springer Verlag",
   note =  "LNCS 197",
   year =  1984
}


@book{HOL,
   author = "Michael J. C. Gordon and Thomas F. Melham",
   title = "Introduction to {HOL} : a theorem proving environment for
                higher-order logic",
   publisher = "Cambridge University Press",
   year = 1993
}

@inproceedings{bertot90,
   author = "Yves Bertot",
   title = "{I}mplementation of an {I}nterpreter for a {P}arallel {L}anguage in
            {C}entaur",
   booktitle = "{E}uropean {S}ymposium {O}n {P}rogramming",
   location = "Copenhagen, Denmark",
   publisher = "Springer Verlag",
   note = "LNCS 432",
   year = 1990
}


@techreport{Interfaces,
   author = "Luca Cardelli",
   title =  "{B}uilding {U}ser {I}nterfaces by {D}irect {M}anipulation", 
   institution = "Digital Equipment Corp. Systems Research Center",
   note = "Research Report 22",
   year = 1987
}

@book{Lambda,
   author =  "Henk Barendregt",
   title = "{T}he {L}ambda {C}alculus, {I}ts {S}yntax and {S}emantics",
   series = "Studies in Logic",
   publisher = "North-Holland",
   year = 1984
}

@inproceedings{Pelletier,
author = "A. Edgar and F. J. Pelletier",
title = "{Natural} language explanation of {Natural} {Deduction}
		  proofs",
booktitle = "{F}irst {Conference} of the {P}acific {A}ssociation for
{C}omputational {L}inguistics",
year = 1993,
location = "Simon Fraser University"
}


@manual{coq-8.0,
  title = "The Coq Proof Assistant Reference Manual, version 8.0",
  organization = "Coq development team",
  year = 2004
}

@manual{coq6-1,
   title = "The Coq Proof Assistant Reference Manual",
   organization = "INRIA",
   year = 1996,
   month = "December",
   note = "Version 6.1"
}
@TECHREPORT{CoqMan96,
  author = {B. Barras  and 
                              S. Boutin  and 
                              C. Cornes  and 
                              J. Courant and 
                              J.C. Filliatre and 
                              E. Gim\'enez    and 
                              H. Herbelin and 
                              G. Huet and 
                              C. Mu{\~{n}}oz and 
                              C. Murthy and
                              C. Parent and 
                              C. Paulin and 
                              A. Sa\"{\i}bi and 
                              B. Werner},
  institution = {INRIA},
  number = {RT-0203},
  title = {{The Coq Proof Assistant Reference Manual -- Version V6.1}},
  year = {1997},
  month = {August},
  note = "revised version distributed with Coq"
}

 
@ARTICLE{PaWe92,
  author = {C. Paulin-Mohring and B. Werner},
  journal = {Journal of Symbolic Computation},
  title = {{Synthesis of ML programs in the system Coq}},
  volume = {15},
  year = {1993},
  pages = {607--640},
}

@misc{pbp-emacs,
   author = "Yves Bertot and Thomas Schreiber and Dilip Sequeira",
   title = "Proof by pointing in a weakly structured context",
   note = "ftp://ftp.dcs.ed.ac.uk/pub/lego/pbp/main.ps"
}
@manual{coq,
   title = "The Coq Proof Assistant User's Guide",
   organization = "INRIA",
   year = 1993,
   month = May,
   author = "Gilles Dowek and Amy Felty and Hugo Herbelin and {G\'erard} Huet
             and Chet Murthy and Catherine Parent and Christine Paulin-Mohring
             and Benjamin Werner",
   note = "Version 5.8"
}



@manual{coq5.10,
   title = "The Coq Proof Assistant User's Guide",
   organization = "INRIA",
   year = 1995,
   month = May,
   author = "Christina Cornes and Judica{\"e}l Courant and
		  Jean-Christophe Filli{\^a}tre and G{\'e}rard Huet
		  and Pascal Manoury and C{\'e}sar Mu{\~n}oz and
		  Chetan Murthy and Catherine Parent and Christine
		  Paulin-Mohring and Amokrane Sa{\"\i}bi and Benjamin Werner",
   note = "Version 5.10"
}

@inproceedings{PPT,
  title = "Proof of Program Transformations",
  author = "Rachel Roxas and Malcolm Newey",
  booktitle = "HOL'91, HOL Theorem Proving System and its Applications",
  location = "Davis, California",
  year = 1991,
  publisher = "IEEE Computer Society Press",
  pages = "223--230"
}



@techreport{sos,
   title = "Structural Operational Semantics",
   author = "Gordon Plotkin",
   institution = "Aarhus University",
   year = 1981,
   type = "lecture notes",
   number = "DAIMI FN-19",
   note = "(reprinted 1991)"
}

@inproceedings{reps,
   title = "Optimal-time incremental semantic analysis for
            syntax-directed editors",
   author = "Thomas Reps",
   booktitle = "Ninth ACM Conference on Principles of Programming
                Languages",
   location = "Albuquerque, New Mexico",
   year = 1982
}

@book{thimbleby,
  author = "Harold Thimbleby",
  title = "User Interface Design",
  publisher = "ACM Press",
  series = "Frontier Series",
  year = {1990},
}

@book{TeitelbaumReps,
   title = "The Synthesizer Generator: a system for constructing
            language based editors",
   author = "Thomas Reps and Tim Teitelbaum",
   publisher = "Springer Verlag",
   year = 1988,
   note = "(third edition)"
}

@inproceedings{Ter95,
   author = "D. Terrasse",
   title = "Encoding Natural Semantics in {Coq}",
   booktitle = "Proceedings of
	     the Fourth International Conference on
	     Algebraic Methodology and Software Technology, AMAST'95",
   series = "Springer-Verlag {LNCS}",
   month = {July},
   year = {1995}
}

@Article{FarmerEtAl93,
  author =      "W. M. Farmer and J. D. Guttman and F. J. Thayer",
  title =       "{\sc imps}: An {I}nteractive {M}athematical {P}roof {S}ystem",
  journal =     "Journal of Automated Reasoning",
  year =        "1993",
  volume =      "11",
  OPTnumber =   "2",
  pages =       "213--248",
  OPTmonth =    "October"
}

@article{BertotTheryGeneric,
  title = "A Generic Approach to Building User Interfaces for Theorem Provers",
  author = "Yves Bertot and Laurent Th{\'e}ry",
  journal = "Journal of Symbolic Computation",
  year = 1998,
  volume = 25,
  pages = "161--194"
}

@article{ReviewEducationLogic93,
author = "Doug Goldson and Steve Reeves and Richard Bornat",
title = "A Review of Several Programs for the Teaching of Logic",
pages = "374--386",
journal = "The Computer Journal",
volume = "36",
number = 4,
year = 1993
}

@article{thery-felty,
  title = "Interactive Theorem Proving with Temporal Logic",
  author = "Amy Felty and Laurent Th{\'e}ry",
  journal = "Journal of Symbolic Computation",
  year = 1997,
  volume = 23,
  pages = "367--397"
}


@inproceedings{FH97,
 author = "Amy P. Felty and Douglas J. Howe",
 title = "Hybrid interactive theorem proving using Nuprl and Hol",
 booktitle = "International Conference on Automated Deduction",
 series = "LNAI",
 number = 1249,
 publisher = "Springer-Verlag",
 year = 1997
}


@inproceedings{felty-howe:tactic,
  title = "Tactic theorem proving with refinement-tree proofs and
          metavariables",
  author = "Amy Felty and Douglas Howe",
  booktitle = "Automated Deduction({CADE-12})",
  location = "Nancy, France,",
  year = 1995,
  month = jun,
  series = "Lecture Notes in Computer Science",
  publisher = "Springer-Verlag",
  volume = 814
}

  

@inproceedings{CTCOQ,
  author ="Janet Bertot and Yves Bertot",
  title = "{CtCoq}: A System Presentation",
  pages= "231--234",
  booktitle = "Automated Deduction ({CADE-13})",
  location = "New Brunswick, New Jersey,",
  year = 1996,
  month = jul,
  series = "Lecture Notes in Artificial Intelligence",
  publisher = "Springer-Verlag",
  volume = 1104
}
		  
@inproceedings{XIsabelle,
  author ="Maris A. Ozols and Katherine A. Eastaughffe and Antony Cant",
  title = "XIsabelle: A system description",
  pages= "400--403",
  booktitle = "Automated Deduction ({CADE-14})",
  location = "Townsville, North Queensland, Australia",
  year = 1997,
  month = jul,
  series = "Lecture Notes in Artificial Intelligence",
  publisher = "Springer-Verlag",
  volume = 1249
}
		  
@inproceedings{XBarnacle,
  title ="XBarnacle: making theorem provers more accessible",
  author = "Helen Lowe and D. Duncan",
  pages= "404--407",
  booktitle = "Automated Deduction ({CADE-14})",
  location = "Townsville, North Queensland, Australia",
  year = 1997,
  month = jul,
  series = "Lecture Notes in Artificial Intelligence",
  publisher = "Springer-Verlag",
  volume = 1249
}
		  
@inproceedings{cHOL,
  author = "Laurent Th{\'e}ry",
  title = "A proof development system for the {HOL} theorem prover",
  booktitle = " Higher Order Logic theorem proving and its applications",
  location = "Vancouver, Canada",
  year = 1993,
  month = aug,
  series = "Lecture Notes in Computer Science",
  publisher = "Springer-Verlag",
  volume = 780
}

@Misc{LEGO,
  title =        "The {LEGO} {W}orld {W}ide {W}eb page",
  key          = "lego",                   
  organisation = "Laboratory for Foundations of Computer Science,
                  University of Edinburgh",
  note = "url {\tt http://www.dcs.ed.ac.uk/home/lego}"}

@inproceedings{ALF,
        AUTHOR = {Lena  Magnusson and Bengt Nordstr\"{o}m},
        BOOKTITLE = {{ Types for Proofs and Programs}},
        PUBLISHER = {Springer-Verlag},
        SERIES = {Lecture Notes in Computer Science},
        VOLUME = {806},
        PAGES = {213--237},
        TITLE   = {{The ALF proof editor and its proof engine}}, 
        YEAR = {1994}
        }

@book{Polak,
  author="Wolfgang Polak",
  title = "Compiler Specification and Verification",
  year = 1981,
  series = "Lecture Notes in Computer Science",
  volume = 124,
  publisher = "Springer-Verlag"}

@book{NUPRL,
  author = "Robert Constable and S. F. Allen and H. M. Bromley and
                  W. R. Cleaveland and J. F. Cremer and R. W. Harber and
                  D. J. Howe and T. B. Knoblock and N. P. Mendler and
                  P. Panangaden and J. T. Sasaki and S. F. Smith",
  title = "Implementing mathematics with the {Nuprl} proof development
                  system",
  year = 1986,
  publisher = "Prentice-{H}all"
}


@book{Paulson:LCF,
   title = "Logic and computation, {I}nteractive proof with {C}ambridge {LCF}",
   author = "Lawrence C. Paulson",
   publisher = "Cambridge University Press",
   year = 1987
}
@phdthesis{Griffin:thesis,
        author = {Timothy Griffin},
        title = {Notational definition and top-down refinement for
                  interactive proof development systems},
        school = {{C}ornell {U}niversity},
        year = 1988
}

@phdthesis{Felty:thesis,
        author = {Amy Felty},
        title = {Specifying and Implementing Theorem Provers in a
                  Higher-Order Logic Programming Language},
        school = "University of Pennsylvania",
        year = 1989
}

@book{Gordon-Melham:HOL,
  author = "Michael Gordon and Thomas Melham",
  title = "Introduction to HOL : A theorem proving environment for
    higher order logic",
  publisher = "Cambridge University Press",
  year = "1993"
}

@book{martin-lof:typetheory,
  title = "Intuitionistic type theories",
  author = "Per Martin-L{\"o}f",
  publisher = "Bibliopolis",
  year = 1984
}

@INPROCEEDINGS{NaciriR,
        title           = "Affichage interactif, bidimensionnel et incrémental de formules mathématiques",
        author          = "H. Naciri and L. Rideau",
        booktitle       = "CARI'2000, Antanarivo (Madagascar)",
        year            = 2000,
        note = {in French}}

@inproceedings{CKT95,
   author = {Y. Coscoy and G. Kahn and Laurent Th\'ery},
   booktitle = {Proceedings of the international conference {TLCA} 
    on typed lambda-calculi and applications, Edimbourg},
   title = {Extracting text from proofs},
   editor = {M. Dezani and G. Plotkin},
   series = "Springer-Verlag {LNCS}",
   volume = "902",
   year = {1995},
   month = apr
}

		  
@techreport{PaulsonRecursion,
  author = {Lawrence C. Paulson},
  title = {Constructing recursion operators in intuitionistic type theory},
  institution = {University of Cambridge, Computer Laboratory},
  type={Technical report},
  number = 57,
  year = 1984,
  month = oct
}

@techreport{Sophtalk,
  author = {Ian Jacobs and Francis Montagnac and Janet Bertot and Dominique Cl{\'ement} and Vincent Prunet},
  title = {the {S}ophtalk reference manual},
  institution = {INRIA},
  type = {Rapport Technique},
  number = {150},
  year = 1993,
  month = feb
}

@inproceedings{Newberry89,
  author="Frances J. Newberry",
  title="Edge Concentration: A Method for Clustering Directed Graphs",
  booktitle="2nd international workshop on software configuration management",
  year=1989,
  location = "Princeton, N.J."
}

@InProceedings{WW:hug95,
  author =       "Wai Wong",
  title =        "Recording and checking {HOL} proofs",
  editor =       "E.~Thomas Shubert, Phillip J.~Windley and James Alves-Foss",
  volume =       "971",
  series =       "Lecture Notes in Computer Science",
  pages =        "353-368",
  booktitle =    "Higher Order Logic Theorem Proving
                  and Its Applications: 8th International Workshop",
  year =         "1995",
  publisher =    "Springer-Verlag"
}

@techreport{wong93,
  author="Wai Wong",
  title="Recording HOL Proofs",
  institution = "University of Cambridge Computer Laboratory",
  year = 1993,
  number = 306,
  month = jul
}

@inproceedings{mini-ml,
  author= "Dominique Cl{\'e}ment and Jo{\"e}lle Despeyroux and Thierry Despeyroux
           and Gilles Kahn",
  title = "A Simple Applicative Language: {M}ini-{ML}",
  booktitle ="proceedings of the 1986 ACM Conference on Lisp and Functional
             Programming",
  location = "Cambridge, Ma., USA",
  month = aug,
  year = 1986
}

@inproceedings{PaulinLeclerc93,
  author = "Fran{\c{c}}ois Leclerc and Christine Paulin-Mohring",
  title = "Programming with streams in Coq.  {A} case study:
           the sieve of {E}ratosthenes",
  booktitle = "Types for Proofs and Progams",
  year = 1993,
  editor = "Henk Barendregt and Tobias Nipkow",
  pages = "191--212",
  publisher = "Springer Verlag",
  series = "LNCS",
  volume = "806"
}

@misc{ConDom,
  author = "Gilles Kahn",
  title = "Elements of Domain Theory (3rd revision)",
  note = "User Contributions to the Coq system",
  year = 1996
}

@inproceedings{KahnMcQueen77,
  author = "Gilles Kahn and David B. MacQueen",
  title = "Coroutines and networks of parallel processes",
  year = 1977,
  pages = "993--998",
  publisher = "North-Holland",
  booktitle = "IFIP Congress 77"
}
@inproceedings{Jape98a,
  author = "Richard Bornat and Bernard Sufrin",
  title = "Using gestures to disambiguate unification",
  booktitle = {Informal proceedings of the Workshop on User Interfaces for
  Theorem  Provers},
  address = {Eindhoven University of Technology},
  year = 1998,
  month = jul,
  note = "Report 98-08"
}

@inproceedings{Jape98b,
  author = "Bernard Sufrin and Richard Bornat",
  title = "User Interfaces for Generic Proof Assistants Part II: Displying Proofs",
  booktitle = {Informal proceedings of the Workshop on User Interfaces for
  Theorem  Provers},
  address = {Eindhoven University of Technology},
  year = 1998,
  month = jul,
  note = "Report 98-08"
}

@inproceedings{Ditmarsch98,
  author = "Hans van Ditmarsch",
  title = "User interfaces in natural deduction programs",
  booktitle = {Informal proceedings of the Workshop on User Interfaces for
  Theorem  Provers},
  address = {Eindhoven University of Technology},
  year = 1998,
  month = july,
  note = "Report 98-08"
}



@inproceedings{bertot96,
   author = {Janet Bertot and Yves Bertot},
   title = {The CtCoq Experience},
   booktitle = {Electronic proceedings for the conference UITP'96},
   address = {University of York},
   year = 1996,
   month = jul,
   URL = {http://www.cs.york.ac.uk/~nam/uitp/proceedings.html }
}

@inproceedings{MerriamUitp97,
   author = {Nicholas A. Merriam and Michael D. Harrison},
   title = "What is Wrong with GUIs for Theorem Provers?",
   booktitle = {Electronic proceedings for the conference UITP'97},
   address={Sophia Antipolis},
   year = {1997},
   month = Sep,
   URL={http://www.inria.fr/croap/events/uitp97-papers.html}
}

@inproceedings{dad97,
   author = {Yves Bertot},
   title = {Direct Manipulation of Algebraic Formulae in Interactive
                  Proof Systems},
   booktitle = {Electronic proceedings for the conference UITP'97},
   address={Sophia Antipolis},
   year = {1997},
   month = Sep,
   URL={http://www.inria.fr/croap/events/uitp97-papers.html}
}

@inproceedings{HarrisonInductive,
  title = "Inductive Definitions: Automation and Application",
  author = "John Harrison",
  booktitle = " Higher Order Logic Theorem Provoing and Its Applications: Proceedings of the 8th  International Workshop",
   volume = 971,
   series = "Lecture Notes in Computer Sciences",
   publisher = "Springer-Verlag",
   year = 1995,
   editor = "P. J. Windley and  T. Schubert and J. Alves-Foss"
}

@inproceedings{Regensburger95,
  title = "{HOLCF}: Higher Order Logic of Computable Functions",
  author = "Franz Regensburger",
  booktitle = " Higher Order Logic Theorem Provoing and Its Applications: Proceedings of the 8th  International Workshop",
   volume = 971,
   series = "Lecture Notes in Computer Sciences",
   publisher = "Springer-Verlag",
   year = 1995,
   editor = "P. J. Windley and  T. Schubert and J. Alves-Foss"
}

@book{guttmanWand95,
  author = {Joshua D. Guttman and Mitchell Wand},
  title = "Vlisp: A Verified Implementation of Scheme",
  publisher = "Kluwer, Boston",
  year = 1995
}


@unpublished{Nipkow00,
author={Tobias Nipkow},
title={Verified Bytecode Verifiers},
institution={TU M\"unchen, Institut f\"ur Informatik},
note={unpublished, available at URL
{\tt http://www.in.tum.de/\~{}nipkow/pubs/bcv2.html}},
year=2000}

@inproceedings{Kildall73,
author= "G. A. Kildall",
title = "A unified approach to global program optimization",
booktitle = "Proceedings of the ACM Symposium on Principles of Programming Languages",
pages={194--206},
year=1973
}

@misc{Rouyer92, 
title="Développement de l'algorithme d'unification dans
le Calcul des Constructions avec types inductifs",
author={Joseph Rouyer},
month=Sep,
year=1992,
note={(In french), available at URL
{\tt http://coq.inria.fr/contribs/unification.html}}
}


@article{Huet97,
author="G{\'e}rard Huet",
title="The Zipper",
journal= "Journal of Functional Programming",
volume=7,
number=5,
month=Sep,
year = 1997,
pages = "549--554"
}
@inproceedings{Nipkow-Oheimb-Pusch,
        author = {Tobias Nipkow and  David von Oheimb and  Cornelia Pusch},
        title = {{$\mu$Java}: Embedding a Programming Language in a Theorem Prover},
        booktitle = {Foundations of Secure Computation},
        series= {NATO Science Series F: Computer and Systems Sciences},
        volume = {175},
        year = {2000},
        publisher = {IOS Press},
        editor = {Friedrich L. Bauer and Ralf Steinbr{\"u}ggen},
        abstract = {This paper introduces the subset $micro$Java of Java,
essentially by omitting everything but classes.
The type system and semantics of this language
(and a corresponding abstract Machine $micro$JVM)
are formalized in the theorem prover Isabelle/HOL.
Type safety both of $micro$Java and the $micro$JVM
are mechanically verified.

To make the paper self-contained, it starts with
introductions to Isabelle/HOL and the art of
embedding languages in theorem provers.},
        CRClassification = {D.3.1, F.3.2},
        CRGenTerms = {Languages, Reliability, Theory, Verification},
        url = {\url{http://isabelle.in.tum.de/Bali/papers/MOD99.html}},
        pages = {117--144}
}

@Book{Nipkow-Paulson-Wenzel:2002,
  author	= {Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel},
  title		= {Isabelle/HOL --- A Proof Assistant for Higher-Order Logic},
  publisher	= {Springer},
  series	= {LNCS},
  volume	= 2283,
  year		= 2002}

@inproceedings{Pusch-TACAS99,
        author = {Cornelia Pusch},
        title = {Proving the Soundness of a {J}ava Bytecode Verifier Specification in {Isabelle/HOL}},
        booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99)},
        series = {LNCS},
        volume = {1579},
        year = {1999},
        publisher = {Springer-Verlag},
        editor = {W. Rance Cleaveland},
        pages = {p. 89--103},
        CRClassification = {D.3.1, F.3.2},
        CRGenTerms = {Languages, Security, Verification},
}

@misc{b:serveur-graphe,
author= {Arnaud {Le Hors}},
title={Graph: A Directed Graph Displaying Server,
       {GIPE} 2 {E}SPRIT project, 4th Review Report, Workpackage 4},
year=1992
}

@misc{b:serveur-graphe2,
author= {Jean-Michel L{\'e}on},
title={{Displaying graphs with Centaur,
        Bull Research France}},
month={Janvier},
year=1993
}


@misc{diva,
  author="John Reekie and Michael Shilman",
  title={Diva: Dynamic, Interactive Visualization},
  note = {available at URL http://www-cad.eecs.berkeley.edu/diva/about/papers/thanksgiving.html},
  year = 1998,
}

@techreport{ptolemyII,
  author="John Davis II, Mudit Goel, Christopher Hylands, Bart Kienhuis, Edward A. Lee, , Jie Liu, Xiaojun Liu, Lukito Muliadi, Steve Neuendorffer, John Reekie, Neil Smyth, Jeff Tsay and Yuhong Xiong ",
  title = "Overview of the Ptolemy Project",
  institution = {University of California at Berkeley},
  number={ERL Technical Report UCB/ERL No. M99/37},
  month = jul,
  year = 1999
}

@inprocedings{edge,
  author="Frances J. Newberry",
  title = "An Interface Description Language for Graph Editors",
  year = 1988,
  booktitle = "IEEE Workshop on Visual Languages",
  pages = "144--149",
  publisher = "IEEE Computer Society Press"
}

@string{spe={Software---Practice and Experience}}


%%%%%%%%%%%%%%%%%%%%%%%%%
%%%  Graphviz and dotty
%%%%%%%%%%%%%%%%%%%%%%%%%

@TechReport{North:1992:NUG,
  author =       "Stephen C. North",
  title =        "{{\sc NEATO}} User's Guide",
  type =         "Technical Report",
  number =       "59113-921014-14TM",
  institution =  "AT\&T Bell Laboratories",
  address =      "Murray Hill, NJ, USA",
  day =          "14",
  month =        oct,
  year =         "1992",
  bibdate =      "Sat May 23 08:02:17 1998",
  acknowledgement = ack-nhfb,
}

@TechReport{dottyManual,
  author =       "Eleftherios Koutsofios",
  title =        "Editing graphs with {\em dotty}",
  type =         "Technical Report",
  institution =  "AT\&T Bell Laboratories",
  address =      "Murray Hill, NJ, USA",
  day =          "5",
  month =        jul,
  year =         "1994",
  bibdate =      "Sat May 23 08:02:17 1998",
  note =         "This report, and the program, is included in the {\tt
                 graphviz} package, available for non-commercial use at
                 http://www.research.att.com/\-sw/tools/graphviz/",
  acknowledgement = ack-nhfb,
}


@TechReport{Koutsofios:1996:DGD,
  author =       "Eleftherios Koutsofios",
  title =        "Drawing graphs with {{\em dot}}",
  type =         "Technical Report",
  institution =  "AT\&T Bell Laboratories",
  address =      "Murray Hill, NJ, USA",
  day =          "20",
  month =        nov,
  year =         "1996",
  bibdate =      "Sat May 23 08:02:17 1998",
  note =         "This report, and the program, is included in the {\tt
                 graphviz} package, available for non-commercial use at
                 \path=http://www.research.att.com/sw/tools/graphviz/=.",
  acknowledgement = ack-nhfb,
}

@Misc{graphviz,
  author =       "John Ellson and Emden Gansner and Eleftherios
                 Koutsofios and Stephen North",
  title =        "GraphViz",
  howpublished = "Available on the internet at URL
                 http://www.research.att.com/\-sw/tools/graphviz",
  url =          "http://www.research.att.com/sw/tools/graphviz",
}


@Article{GansnerNorthSPE2000,
title={An open graph visualization system and its applications to software engineering},
author={Emden R. Gansner, Stephen C. North},
journal=spe,
pages={1203--1233},
month=apr,
year=2000,
volume=30,
number=4,

}


%%%%%%%%%%%%%%%%%%%%%%% 
%%%   Davinci
%%%%%%%%%%%%%%%%%%%%%%%
@PhdThesis{Fro97,
         author =       "Michael Fröhlich",
         title =      "Incremental Graphlayout in the Visualization
		  System daVinci (in german language)",
         school =       "Department of Computer Science; University of Bremen",
         year =         "1997",
         month =        nov,
         keywords =     "Graph",
	ftp ={ftp://ftp.Uni-Bremen.DE/pub/Uni-Bremen/Departments/CS/Chairs/Krieg-Brueckner/froehlich/dis.ps.gz}
		  
       }
		  
@Misc{daVinci98,
        author = { Michael Fröhlich and Mattias Werner},
        TITLE={{daVinci V2.1 Online Documentation}},
        note= {accessible  at http://www.informatik.uni-bremen.de/\-\~{}davinci/\-doc\_V2.1},
        year={1998},
month={July}

}

@inproceedings{Tar75,
   title = "On the {E}fficiency of a {G}ood but not {L}inear {S}et 
                  {M}erging {A}lgorithm",
  author = "R. Tarjan",
  booktitle = "Journal of the ACM",
  volume = 22,
  pages = "215--225",
  year = 1975
}



@InProceedings{Froehlich:1994:DIG,
  author =       "M. Fr{\"{o}}hlich and M. Werner",
  title =        "Demonstration of the Interactive Graph-Visualization
                 System daVinci",
  editor =       "R. Tamassia and I. G. Tollis",
  volume =       "894",
  series =       "Lecture Notes in Computer Science",
  pages =        "266--269",
  booktitle =    "Graph Drawing",
  year =         "1994",
  organization = "DIMACS",
  publisher =    "Springer-Verlag",
  month =        oct,
  note =         "ISBN 3-540-58950-3",
}

@techreport{FrohlichMa1994a,
 author      ={ Michael Fröhlich and Mattias Werner},
 title       ="The Graph Visualization System daVinci - A User 
               Interface for Applications",
 number      ="5/94",
 institution ="Department of Computer Science; University of Bremen",
 month       ="September",
 year        ="1994",
 scope       ="appl",
 documentURL ="ftp://ftp.Uni-Bremen.DE/pub/graphics/daVinci/papers/techrep0594.ps.gz",
 keywords    ="implemented in ASpecT"
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%% Graplet seem to be still alive.......to be updated .(OCT 2000)
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
       @InCollection{gd96,
         author =       "Michael Himsolt",
         title =        "The Graphlet System",
         booktitle =    "Graph Drawing 96",
         publisher =    "Springer-Verlag  LNCS 1190 ",
         year =         "1996",
         editor =       "Stephen North",
         pages =        "233-240",
       }	  
		  gd96

@techreport{GML,
        author = {Michael Himsolt},
        TITLE={GML: A portable Graph File Format},
        institution= { Universität Passau},
        type = {Technical Report},
        year={1997}

}
@techreport{GraphletManual,
        author = {Michael Himsolt},
        TITLE={Graphlet Manuals: GML, GraphScript, C++ Interface},
        institution= { Universität Passau},
        type = {Technical Report},
        year={1997}

}


%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%algorith
%%%%%%%%%%%%%%%%%%%%%%%%
@Article{STT81,
title={Methods for Visual Understanding of Hierarchical System Structures},
author={Kozo Sugiyama and Shojiro Tagawa and Mitsuhiko Toda},
journal={IEEE Transactions on Systems, Man, and Cybernetics},
pages={109 - 125},
month= {July/August},
year=1981,
volume={SMC-11},
number=2
}


%%%%%%a regarder si je le trouve.......

@misc{ livadas-new,
    author = "P. Livadas and S. Croll",
    title = "A new algorithm for the calculation of transitive dependences",
    text = "Livadas, P. E., and Croll, S. A new algorithm for the calculation of transitive
      dependences. Journal of Software Maintenance ((accepted))."
}

@InProceedings{MenissierReals95,
author = "Val{\'e}rie M{\'e}nissier-Morain",
title = "Conception et algorithmique d'une repr{\'e}sentation
d'arithm{\'e}tique r{\'e}elle en pr{\'e}cision arbitraire",
booktitle = "Proceedings of the first conference on real numbers
and computers",
year = 1995}

@inproceedings{BartheRuysBarendregt95,
 author = {Gilles Barthe and Mark Ruys and Henk Barendregt},
 title = {A Two-Level Approach Towards Lean Proof-Checking},
 booktitle = {TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs},
 year = {1996},
 isbn = {3-540-61780-9},
 pages = {16--35},
 publisher = {Springer-Verlag},
 address = {London, UK},
 }

@article{MuellerNvOS99,
author=
{Olaf M\"uller and Tobias Nipkow and Oheimb, David von and Oskar Slotosch},
title={{HOLCF = HOL + LCF}},
journal={Journal of Functional Programming},volume=9,pages={191--223},
year=1999}

 @InProceedings{flop-barthe-forest-pichardie-rusu-06,
   Author = { Barthe, G. and Forest, J. and Pichardie, D. and Rusu, V.},
   Title = {Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant},
   BookTitle = {Functional and LOgic Programming Systems (FLOPS'06)},
   Address = {Fuji Susono, Japan},
   Month = {April},
   Year = {2006}
}



@article{Nipkow98,
   title = "Winskel is (almost) Right:Towards a Mechanized Semantics Textbook",
   author = "Tobias Nipkow",
   journal = "Formal Aspects of Computing",
   year = 1998,
   pages = "171--186",
   volume = "10"

}

@inproceedings{CoquandInfinite93,
 author = "Thierry Coquand",
 title = "Infinite objects in {T}ype {T}heory",
 booktitle = "Types for Proofs and Programs",
 editor = "Henk Barendregt and Tobias Nipkow",
 pages = "62--78",
 year = 1993,
 volume = 806,
 publisher = "Springer Verlag",
 series = "LNCS"
}

@inproceedings{Gimenez94,
  author = "Eduardo Gim{\'e}nez",
  title = "Codifying guarded definitions with recursive schemes",
  booktitle = "Types for proofs and Programs",
  editor = "Peter Dybjer and Bengt Nordstr{\"o}m and Jan Smith",
  publisher = "Springer Verlag",
  series = "LNCS",
  pages = "39--59",
  year = "1994",
  volume = "996"
}

@inproceedings{Gimenez95,
title = "An Application of Co-Inductive Types in {C}oq: Verification of the Alternating Bit Protocol",
author = "Eduardo Gim{\'e}nez",
booktitle = {\sl  Proceedings of the 1995 Workshop on Types for Proofs and Programs},
series= {Lecture Notes in Computer Science},
volume= {1158},
pages= {135-152},
year = 1995,
publisher= {Springer-Verlag},
}


%%%%%%%%%%%%%%%%%%%%%%%
%%%     Provers :
%%%%%%%%%%%%%%%%%%%%%%
@Manual{coq6,
  title = 	 {The Coq Proof Assistant User's Guide. Version 6.3.1},
  author = {Bruno Barras and Samuel Boutin and Cristina Cornes and
                 Judicael Courant and   Yann Coscoy and David Delahaye and 
                 Daniel de Rauglaudre,Jean-Christophe Filliatre and
                 Eduardo Gimenez and Hugo Herbelin and Gerard Huet and
                 Cesar Munoz and Chetan Murthy and Catherine Parent and
                 Christine Paulin-Mohring and Amokrane Saibi and
                 Benjamin Werner},
  organization = {INRIA},
  month = 	 {December},
  year = 	 {1999}
}

@misc{ mehlhorn96checking,
    author = "K. Mehlhorn and S. Naher and M. Seel and R. Seidel and T. Schilz and S.
      Schirra and C. Uhring",
    title = "Checking geometric programs or verification of geometric structures",
    text = "K. Mehlhorn, S. Naher, M. Seel, R. Seidel, T. Schilz, S. Schirra, and C.
      Uhring. Checking geometric programs or verification of geometric structures.
      In Proc 12th GEOMETRY, pages 159--165, 1996.",
    year = "1996"
}

@Book{HOL93a,
 author =       "Michael J.C. Gordon and Thomas.F. Melham",
 title =        "Introduction to {HOL}: a theorem proving environment
                        for higher order logic",
 publisher =    "Cambridge University Press",
 year =         "1993",
 key =          "HOL",
}

@inproceedings{hensel+98,
title= "Reasoning about Classes in Object-Oriented Languages: Logical Models and Tools",
author= "Ulrich Hensel and Marieke Huisman and Bart Jacobs and Hendrik Tews",
booktitle ="Proceedings of European Symposium on Programming (ESOP '98)",
month = Mar,
year = 1998,
series =  "LNCS",
volume = 1381,
pages= "105--121",
publisher = "Springer-Verlag"
}

@article{Owre95:prolegomena,
       AUTHOR = {Sam Owre and John Rushby and Natarajan Shankar
   and Friedrich von Henke},
       TITLE = {Formal Verification for Fault-Tolerant Architectures:
   Prolegomena to the Design of {PVS}},
       JOURNAL = {{IEEE} Transactions on Software Engineering},
       VOLUME = {21},
       NUMBER = {2},
       YEAR = {1995},
       PAGES = {107--125},
       MONTH = {feb},
       URL = {http://www.csl.sri.com/papers/tse95/}
   }

@article{unspecified,
       AUTHOR = {Natarajan Shankar},
       TITLE = {{PVS:} Combining Specification, Proof Checking, and
   Model Checking},
       YEAR = {1996},
       URL = {http://www.csl.sri.com/papers/fmcad-tutorial/},
       BOOKTITLE = {{FMCAD96}}
   }


@manual{PVS:prover,
        TITLE = {The {PVS} Proof Checker: A Reference Manual},
        AUTHOR = {Natarajan Shankar and Sam Owre and John M. Rushby},
        MONTH = feb,
        YEAR = 1993,
        ORGANIZATION = {Computer Science Laboratory, SRI International},
        ADDRESS = {Menlo Park, CA},
        NOTE = {A new edition for PVS Version 2 is expected in 1998}
}
 
@book{NUPRL,
  author = "Robert Constable and S. F. Allen and H. M. Bromley and
                  W. R. Cleaveland and J. F. Cremer and R. W. Harber and
                  D. J. Howe and T. B. Knoblock and N. P. Mendler and
                  P. Panangaden and J. T. Sasaki and S. F. Smith",
  title = "Implementing mathematics with the {Nuprl} proof development
                  system",
  year = 1986,
  publisher = "Prentice-{H}all"
}            
 

@incollection{Reif92,
  AUTHOR = {Wolfgang  Reif},
  TITLE = {The {KIV} System: Systematic Construction of Verified Software},
  YEAR = 1992,
  BOOKTITLE = {Automated Deduction: CADE-11 - Proc.\ of the 11th International Conference on Automated Deduction},
  EDITOR = {D. Kapur},
  PUBLISHER = {Springer},
  ADDRESS = {Berlin, Heidelberg},
  PAGES = {753-757},
  KEYWORDS = {}}

@InCollection{Reif95korso,
        author = {Wolfgang  Reif},
        title = {{The {KIV}-approach to Software Verification}},
        booktitle = {{KORSO: Methods, Languages, and Tools for the
                Construction of Correct Software -- Final Report}},
        year = {1995},
        editor = {M. Broy and S. J\"ahnichen},
        publisher = {Springer LNCS 1009}
}


@inproceedings{Coscoy96,
author = "Yann Coscoy",
title = "A natural language explanation for formal proofs",
editor="Christian R{\'e}tor{\'e}",
booktitle="Logical {A}spects of {C}omputational {L}inguistics",
publisher = "Springer-Verlag",
series = "LNCS/LNAI",
volume = 1328,
year = 1996
}
%%%%%%%%%%%% omega http://www.ags.uni-sb.de/projects/deduktion/
@INPROCEEDINGS{Omega94,
   author    = {Xiaorong Huang and Manfred Kerber and Michael Kohlhase and Erica Melis and Dan Nesmith and J{\"o}rn Richts and J{\"o}rg Siekmann},
   TITLE     = {{$\Omega$-MKRP}: A proof development environment},
   EDITOR    = {Alan Bundy},
   BOOKTITLE = {Automated Deduction --- CADE-12},
   SERIES    = {Proceedings of the 12th International Conference on Automated Deduction},
   PAGES     = {788--792},
   ADDRESS   = {Nancy, France},
   YEAR      = {1994},
   ORGANIZATION = {},
   PUBLISHER = {Springer-Verlag, Berlin, Germany},
   NOTE      = {LNAI 814},
   ABSTRACT = {$\Omega$-MKRP is an interactive proof development
 environment, the requirements of which were derived from our
 experiences in proving theorems of a typical mathematical
 textbook with the first-order theorem prover MKRP.
 $\Omega$-MKRP uses an input language which is based on sorted
 higher-order logic.  The user can use a database of
 mathematical knowledge (definitions, theorems and tactics) and
 is supported by automated theorem provers, proofs of which
 can be transformed into the natural deduction calculus.
 Finally a proof can be presented in natural English.
}}

InProceedings{BenzmuellerEtAl:otama97,
  author =       {Christoph  Benzm{\"u}ller and Lassaad Cheikhrouhou and Detlef Fehrer and Armin Fiedler and Xiaorong   Huang and  Manfred Kerber and Michael Kohlhase and Karsten Konrad and Erica Melis and Andreas Meier and Wolf Schaarschmidt and J{\"o} Siekmann and Volker Sorge},
  title =        {{$\Omega$ Mega}: Towards a mathematical assistant},
  crossref =  {CADE97},
  year =         1997,
  abstract = {{$\Omega$ Mega} is a mixed-initiative system with the ultimate 
purpose of supporting theorem proving in main-stream mathematics and 
mathematics education. The current system consists of a proof planner and an 
integrated collection of tools for formulating problems, proving subproblems, 
and proof presentation.}
}



@misc{ergo,
    author = "Holger Becht Anthony",
    title = "Ergo 4.1 Reference Manual"
}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%  graph and tree visualization in proof assistant
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

@InProceedings{TPHOLs94:SchubertBiggs,
   author = {Tom Schubert and John Biggs},
   title = {A Tree-Based, Graphical Interface for Large Proof Development},
   booktitle = "Supplementary Proceedings of the 1994 HOL",
   location =  "Malta",
   Editor="Tom Melham and Juanito Camilleri",
   note = "available at URL http://www.dcs.gla.ac.uk/~hug94/sproc.html",
   year = 1994
}
	  


@InProceedings{LOUI98-UITP,
  author =       "Jörg Siekman and  Stephan Hess and Christoph Benzmüller and Lassaad  Cheikhrouhou and  Detlef Fehrer and Armin Fiedler and Helmut Horacek and Michael Kohlhase and  Karsten Konrad and Andreas Meier and Erica Melis and Volker Sorge",
  title =        "A Distributed Graphical User Interface for the Interactive Proof System ",
  year =         1998,
  booktitle =    {Proceedings of the International Workshop "User Interfaces for Theorem Provers 1998 (UITP'98)"}, 
  series = {},
  address = {Eindhoven, Netherlands},
  abstract = {Most interactive proof development environments are
  insufficient to handle the complexity of the information to be
  conveyed to the user and to support his orientation in large-scale
  proofs.  In this paper we present a distributed client-server
  extension of the OMEGA proof development system, focusing on the LOUI
  (Lovely OMEGA User Interface) client. This graphical user interface
  provides advanced communication facilities through an adaptable proof
  tree visualization and through various selective proof object display
  methods.  Some of LOUI's main features are the graphical display of
  co-references in proof graphs, a selective term browser, and support
  for dynamically adding knowledge to partial proofs -- all based upon
  and implemented in a client-server architecture.}
}

@Article{LOUI99,
  author =       {J{\"o}rg Siekmann and Stephan M. Hess and Christoph Benzm{\"u}ller and Lassaad
  Cheikhrouhou and  Armin Fiedler and Helmut Horacek and Michael Kohlhase and Karsten Konrad and
  Andreas Meier and Erica Melis and Martin Pollet and Volker Sorge},
  title =        {{$\cal LOUI$: $\cal L$ovely {$\Omega$} $\cal U$ser $\cal I$nterface}},
  journal =      {Formal Aspects of Computing},
  pages =        {326--342},
  volume =       11,
  number =       3,
  year =         1999
} 

@Misc{dependtohtml,
  author = 	 {Loic Pottier and Olivier Pons},
  title = 	 {dependtohtml: Creating hypertext graphical representation of directed graphs},
  year={1998},
   note = {Available on the internet at URL http://www.inria.fr\-/croap\-/personnel\-/Loic.Pottier\-/Dependtohtml\-/README.html}

  }

		  
 @MastersThesis{valentin,
  author = 	 {Pierre  Valentin},
  title = 	 {Legolang:   Une  interface  graphique  pour  le systeme  de  preuve  lego},
  school = 	 {Universite  de  Nice},
  type ={Rapport de DEA},
  year = 	 {1993}

}


@phdthesis{pons-th,
author={O. Pons},
title="Conception et réalisation d'outils d'aide au développement de
                  grosses théories dans les systèmes de preuves
                  interactifs",
school={Conservatoire National des Arts et Métiers},
year=1999}            





@Misc{Reetz,
  key = 	 {},
  author = 	 {Ralf Reetz},
  title = 	 {Improving the usability of higher order logic theorem prover by graph visualisation},
 }


@InProceedings{Nickson95,
  author =       "Ray Nickson",
  title =        "A New Face for Ergo: Adding a User Interface to a
                 Programmable Theorem Prover",
  booktitle =    "Proceedings of OZCHI'95, the CHISIG Annual Conference
                 on Human-Computer Interaction",
  series =       "Full Papers",
  pages =        "204--209",
  year =         "1995",
  copyright =    "(c) Copyright 1997 Ergonomics Society of Australia
                 CHISIG",
  keywords =     "Proof tools, User interfaces, Prototyping, Emacs",
  mrnumber =     "C.OZCHI.95.204",
  abstract =     "We describe some of the technology we used to build a
                 user interface for a programmable theorem prover. By
                 separating the user interface from the application
                 itself, it is possible to experiment with new interface
                 features very easily, without compromising the
                 soundness of the proof tool.",
}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%Using of dependcy graph in software enineering.........
%%%%%%%%% Old...
%%%%%%%%%%%%%%%%%%%%%%%%%%%%


@Article{LinosADHLT94,
title={Visualizing Program Dependencies: An Experimental Study},
author={Panagiotis K. Linos and Philippe Aubet and Laurent Dumas and
Yann Helleboid and Patricia Lejeune and Philippe Tulula},
journal=spe,
pages={387--403},
month=apr,
year=1994,
volume=24,
number=4,
source={http://theory.lcs.mit.edu/~dmjones/hbp/bibs/ley/spe/spe.bib}
}



@InProceedings{   horwitz:92,
  author        = {Susan B. Horwitz and Thomas Reps},
  title         = {The Use of Program Dependence Graphs in Software
                  Engineering},
  booktitle     = icse14,
  pages         = {392--411},
  month         = may,
  year          = {1992},
  abstract      = {This paper describes a language-independent program
                  representation-the program dependence graph-and discusses
                  how program dependence graphs, together with operations
                  such as program slicing, can provide the basis for powerful
                  programming tools that address important software
                  engineering problems, such as understanding what an
                  existing program does and how it works, understanding the
                  differences between several versions of a program, and
                  creating new programs by combining pieces of old programs.
                  The paper primarily surveys work in this area that has been
                  carried out at the University of Wisconsin.},
  http          = {http://www.cs.wisc.edu/wpis/papers/icse92.ps},
  class         = {Reverse_Engineering,
                  Intermediate_Representations_of_Source_Code, Using_graphs},
}


@InProceedings{   livadas:92,
  author        = {Panos E. Livadas and Prabal K. Roy},
  title         = {Program Dependence Analysis},
  pages         = {356-365},
  booktitle     = icsm92,
  year          = {1992},
  publisher     = ieeecsp,
  month         = nov,
  abstract      = {It is generally recognized that one of the reasons that
                  software maintenance is so costly is that each modification
                  to a program must take into account the numerous complex
                  interrelationships in the existing software; an
                  understanding of program dependences is fundamental to
                  efficient software change. Such dependences can be of the
                  following types, data flow, calling, and functional
                  dependences. Furthermore, as the software community
                  gradually begins to move toward a more object-oriented
                  perspective on software development, it will become
                  increasingly important to be able to 'objectify' existing
                  software systems. Successful maintenance requires precise
                  knowledge of the data items in a system, the ways these
                  items are created and modified, and their relationships
                  between one another.
                  
                  In this paper the authors address these two issues. First,
                  they will discuss three methods of identifying objects the
                  first two of which were suggested by Liu and Wilde; the
                  third method is one that is proposed in this paper and is
                  based on the determination of the receiver of a procedure.
                  We believe that the latter method is one that is more
                  natural and precise than the former two. Second, algorithms
                  that perform precise interprocedural flow-sensitive
                  dependency analysis, as well as algorithms that identify
                  'objects', are introduced. Furthermore, the internal
                  program representation that we emply, the parse-tree-based
                  system dependence graph (SDG), is briefly discussed.
                  Finally, a unique tool that we have developed is presented
                  that accepts a subset of ANSI C (or Pascal) as input and
                  which implements all algorithms discussed in this paper.},
  class         = {Reverse_Engineering,
                  Intermediate_Representations_of_Source_Code, Using_graphs,
                  Static_Analysis, Static_Data_Flow_Analysis,
                  Reverse_Engineering, Re-Use}
}


@InProceedings{   loyall:93,
  author        = {Joseph P. Loyall and Susan A. Mathisen},
  title         = {Using Dependence Analysis to Support the Software
                  Maintenance Process},
  pages         = {282-291},
  booktitle     = icsm93,
  year          = {1993},
  publisher     = ieeecsp,
  month         = sep,
  abstract      = {Dependence analysis is useful for software maintenance
                  because it indicates the possible effects of a software
                  modification on the rest of a program. This helps the
                  software maintainer evaluate the appropirateness of a
                  software modification, drive regression testing, and
                  determine the vulnerabiltiy of critical sections of code.
                  This paper presents a definition of interprocedural
                  dependence analysis and its implementation in a prototype
                  tool that supports software maintenance.},
  class         = {Alteration, Change_Impact}
}


@book{Thompson96,
  title = "Haskell, the craft of functional programming",
  author = "Simon Thompson",
  year = 1996,
  publisher = "Addison-Wesley",
  isbn = "0-201-40357-9"
}

@book{ChaillouxManouryPagano,
  author = "Emmanuel Chailloux and Pascal Manoury and Bruno Pagano",
  title = "D{\'e}veleoppement d'applications avec Objective Caml",
  publisher = "O'Reilly and associates",
  year = 2000
}

@book{WeisLeroy99,
  author = "Pierre Weis and Xavier Leroy",
  title = "Le Langage Caml",
  publisher = "Dunod",
  year = 1999
}

@misc{ han97supporting,
    author = "J. Han",
    title = "Supporting Impact Analysis and Change Propagation in Software Engineering
      Environments",
    text = "J. Han. Supporting Impact Analysis and Change Propagation in Software Engineering
      Environments, Proceedings. In Proc. of the 8th Intl. Workshop on Software
      Technology and Engineering Practice (STEP'97), London, England, pp. 172-182,
      July 1997.",
    year = "1997"
}


	  
@Article{Moser90,
title={Data Dependency Graphs for {Ada} Programs},
author={Louise E. Moser},
journal=ieets1,
pages={499--509},
month=may,
year=1990,
volume=16,
number=5,
source={http://theory.lcs.mit.edu/~dmjones/hbp/bibs/ley/tse/ieeetse.bib}
}

	  


@InProceedings{Erwig1997,
title={Functional Programming with Graphs},
author={Martin Erwig},
pages={52--65},
crossref={ICFP2},
source={http://theory.lcs.mit.edu/~dmjones/hbp/icfp/icfp.bib}
}

%%%

@Article{SM91,
title={Visualization of Structural Information: Automatic Drawing of Compound Digraphs},
author={Kozo Sugiyama and Kazuo Misue},
journal={IEEE Transactions on Systems, Man, and Cybernetics},
pages={876 - 892},
month= {July/August},
year=1991,
volume={SMC-21},
number=4
}


@InProceedings{   loyall:93,
  author        = {Joseph P. Loyall and Susan A. Mathisen},
  title         = {Using Dependence Analysis to Support the Software
                  Maintenance Process},
  pages         = {282-291},
  booktitle     = icsm93,
  year          = {1993},
  publisher     = ieeecsp,
  month         = sep,
  abstract      = {Dependence analysis is useful for software maintenance
                  because it indicates the possible effects of a software
                  modification on the rest of a program. This helps the
                  software maintainer evaluate the appropirateness of a
                  software modification, drive regression testing, and
                  determine the vulnerabiltiy of critical sections of code.
                  This paper presents a definition of interprocedural
                  dependence analysis and its implementation in a prototype
                  tool that supports software maintenance.},
  class         = {Alteration, Change_Impact}
}

%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%slicing 
%%%%%%%%%%%%%%%%%%%%%%%
@InCollection{Tip94a,
  author =       "Frank Tip",
  title =        "A Survey of Program Slicing Techniques.",
  booktitle =    "301",
  pages =        "58",
  publisher =    "Centrum voor Wiskunde en Informatica (CWI)",
  address =      "ISSN 0169-118X",
  month =        jul # " 31",
  year =         "1994",
  url =          "ftp://ftp.cwi.nl/pub/CWIreports/AP/CS-R9438.ps.Z",
  note =         "AP (Department of Software Technology)",
  note =         "CS-R9438",
  note =         "Wed, 13 Aug 1997 10:40:56 GMT",
}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% clustering 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@InProceedings{ref187,
  author =       "D. Doval and S. Mancoridis and B. S. Mitchell",
  title =        "Automatic Clustering of Software Systems using a
                 Genetic Algorithm",
  booktitle =    "{IEEE} Proceedings of the 1999 Int. Conf. on Software
                 Tools and Engineering Practice ({STEP}'99)",
  year =         "1999",
  citekey =      "ref187",
}


@InProceedings{ref2002,
  author =       "S. Mancoridis and B. S. Mitchell and C. Rorres and Y.
                 Chen and E. R. Gansner",
  title =        "Using Automatic Clustering to Produce High-Level
                 System Organizations of Source Code",
  booktitle =    "{IEEE} Proceedings of the 1998 Int. Workshop on
                 Program Understanding ({IWPC}'98)",
  year =         "1998",
  citekey =      "ref2002",
}

@inproceedings{Pons00,
title = "Ing{\'e}ni{\'e}rie de preuve",
author = "Olivier Pons",
booktitle = {\sl Journ{\'e}es Francophones pour les Langages Applicatifs},
month = jan,
yead = 2000,
}

@inproceedings{MagaudBertot01,
title = "Changement de repr{\'e}sentation des
structures de donn{\'e}es en Coq: le cas des entiers naturels", 
author = "Nicolas Magaud and Yves Bertot",
booktitle = {\sl Journ{\'e}es Francophones pour les Langages Applicatifs},
month = jan,
year = 2001,
}

@inproceedings{Bertot02,
title = "Des descriptions fonctionnelles aux implémentations impératives de programmes",
booktitle ={\sl Journ{\'e}es francophones pour les langages applicatifs, JFLA'02},
month = jan,
year = 2002,
note = {en Fran{\c{c}}ais}
}


@inproceedings{BalaaBertot02,
title = "Fonctions r{\'e}cursives g{\'e}n{\'e}rales par it{\'e}ration
         en th{\'e}orie des types",
author = "Antonia Balaa and Yves Bertot",
booktitle = {\sl Journ{\'e}es Francophones pour les Langages Applicatifs},
month = jan,
year = 2002,
}

@ARTICLE{Filliatre00a,
  AUTHOR = {J.-C. Filli\^atre},
  TITLE = {{Verification of Non-Functional Programs 
                   using Interpretations in Type Theory}},
  JOURNAL = {Journal of Functional Programming},
  YEAR = 2001,
  NOTE = {English translation of~\cite{Filliatre99}. To appear.},
  URL = {http://www.lri.fr/~filliatr/ftp/publis/jphd.ps.gz},
  ABSTRACT = {We study the problem of certifying programs combining imperative and
  functional features within the general framework of type theory.
  
  Type theory constitutes a powerful specification language, which is
  naturally suited for the proof of purely functional programs. To
  deal with imperative programs, we propose a logical interpretation
  of an annotated program as a partial proof of its specification. The
  construction of the corresponding partial proof term is based on a
  static analysis of the effects of the program, and on the use of
  monads. The usual notion of monads is refined in order to account
  for the notion of effect. The missing subterms in the partial proof
  term are seen as proof obligations, whose actual proofs are left to
  the user. We show that the validity of those proof obligations
  implies the total correctness of the program.
  We also establish a result of partial completeness.
  
  This work has been implemented in the Coq proof assistant.
  It appears as a tactic taking an annotated program as argument and
  generating a set of proof obligations. Several nontrivial
  algorithms have been certified using this tactic.}
}

@PHDTHESIS{Filliatre99,
  AUTHOR = {J.-C. Filli\^atre},
  TITLE = {{Preuve de programmes imp\'eratifs en th\'eorie des types}},
  TYPE = {Th{\`e}se de Doctorat},
  SCHOOL = {Universit\'e Paris-Sud},
  YEAR = 1999,
  MONTH = {July},
  URL = {http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz},
  ABSTRACT = {Nous étudions le problème de la certification de programmes mêlant
  traits impératifs et fonctionnels dans le cadre de la théorie des
  types.

  La théorie des types constitue un puissant langage de spécification,
  naturellement adapté à la preuve de programmes purement
  fonctionnels.  Pour y certifier également des programmes impératifs,
  nous commençons par exprimer leur sémantique de manière purement
  fonctionnelle. Cette traduction repose sur une analyse statique des
  effets de bord des programmes, et sur l'utilisation de la notion de
  monade, notion que nous raffinons en l'associant à la notion d'effet
  de manière générale.  Nous montrons que cette traduction est
  sémantiquement correcte.

  Puis, à partir d'un programme annoté, nous construisons une preuve
  de sa spécification, traduite de manière fonctionnelle. Cette preuve
  est bâtie sur la traduction fonctionnelle précédemment
  introduite. Elle est presque toujours incomplète, les parties
  manquantes étant autant d'obligations de preuve qui seront laissées
  à la charge de l'utilisateur.  Nous montrons que la validité de ces
  obligations entraîne la correction totale du programme.

  Nous avons implanté notre travail dans l'assistant de preuve
  Coq, avec lequel il est dès à présent distribué. Cette
  implantation se présente sous la forme d'une tactique prenant en
  argument un programme annoté et engendrant les obligations de
  preuve.  Plusieurs algorithmes non triviaux ont été certifiés à
  l'aide de cet outil (Find, Quicksort, Heapsort, algorithme de
  Knuth-Morris-Pratt).}
}

@INPROCEEDINGS{FilliatreMagaud99,
  AUTHOR = {J.-C. Filli\^atre and N. Magaud},
  TITLE = {{Certification of sorting algorithms in the system Coq}},
  BOOKTITLE = {Theorem Proving in Higher Order Logics: 
                  Emerging Trends},
  YEAR = 1999,
  ABSTRACT = {We present the formal proofs of total correctness of three sorting
  algorithms in the system Coq, namely \textit{insertion sort},
  \textit{quicksort} and \textit{heapsort}. The implementations are
  imperative programs working in-place on a given array. Those
  developments demonstrate the usefulness of inductive types and higher-order
  logic in the process of software certification. They also
  show that the proof of rather complex algorithms may be done in a
  small amount of time --- only a few days for each development ---
  and without great difficulty.},
  URL = {http://www.lri.fr/~filliatr/ftp/publis/Filliatre-Magaud.ps.gz}
}

@inproceedings{Gregoire-Leroy-02,
        author =        "Benjamin Gr{\'e}goire and Xavier Leroy",
        title =         "A compiled implementation of strong reduction",
        booktitle =     "International Conference on Functional Programming 2002",
        pages =         "235--246",
        publisher =     "ACM Press",
        year =          2002,
        url =           "http://pauillac.inria.fr/~xleroy/publi/strong-reduction.pdf"
}

@Preamble{"\newcommand{\noopsort}[1]{}"}

@String{north_holland={North Holland}}
@String{springer={Springer-Verlag}}
@String{jsc  = "Journal of Symbolic Computation"}
@String{AP   = "Academic Press"}
@String{camb = "Cambridge University Press"} 
@String{elsevier = "Elsevier Science Publishers"}
@String{entcs = "Electronic Notes in Theoretical Computer Science"}


@PhdThesis{bates.01,
  author = 	 {Bruce P. Bates},
  title = 	 {Self-{M}atching and Interleaving in Some Integer Sequences and the Gauss Map},
  school = 	 {University of Wollogong},
  year = 	 {2001}
}


@Misc{bogomolny,
  author = 	 {Alexander Bogomolny},
  title = 	 {Stern-{B}rocot {T}ree},
  howpublished = {\url{http://www.cut-the-knot.com/blue/Stern.html}},
}


@Article{brocot.1861,
  author = 	 {Achille Brocot},
  title = 	 {Calcul des rouages par approximation, nouvelle m\'ethode.},
  journal = 	 {Revue chronom\'etrique. Journal des horlogers, scientifique et pratique},
  year = 	 {1861},
  volume = 	 {3},
  pages = 	 {186-194},
}


@techreport{diGianantonioGolden96,
  title = "A Golden Ration Notation for the Real Numbers",
  author = "Pietro Di Gianantonio",
  institution = "CWI, Amsterdam",
  number = "CS-R9602",
  issn = "0189-118X",
  year = 1996
}

@InProceedings{diGianantonioMiculan,
  author = "Pietro Di Gianantonio and Marino Miculan",
  title = "A Unifying Approach to Recursive and Co-recursive Definitions",
  booktitle = "Types for Proofs and Programs",
  year= 2003,
  volume = 2646,
  series = "LNCS",
  publisher = {Springer Verlag},
  pages = "148--161",
  editor = "Herman Geuvers and Freek Wiedijk"
}

@InProceedings{diGianantonioMiculan04,
  author = "Pietro Di Gianantonio and Marino Miculan",
  title = "Unifying Recursive and Co-recursive Definitions in Sheaf Categories",
  booktitle = "Foundations of Software Science and Computation Structures (FOSSACS'04)",
  year= 2004,
  volume = 2987,
  series = "LNCS",
  publisher = {Springer Verlag},
  editor = "Igora Walukiewicz"
}

@InProceedings{ciaffaglione.00,
  author = 	 {Alberto Ciaffaglione and Pietro Di Gianantonio},
  title = 	 {A coinductive approach to real numbers},
  booktitle = 	 {Types 1999 Workshop, L\"okeberg, Sweden}, 
  year = 	 {2000},
  series = 	 {LNCS},
  number = 	 {1956},
  editor = 	 {Th.~Coquand and P.~Dybjer and B.~Nordstr\"om and J.~Smith},
  pages = 	 {114-130},
  publisher =    springer,
}

@Manual{coq73,
  title = 	 {The Coq Proof Assistant Reference Manual, Version 7.3},
  author = 	 {Bruno Barras et al.},
  organization = {INRIA},
  address = 	 {\url{http://coq.inria.fr/doc/main.html}},
  month = 	 {oct},
  year = 	 {2002},
}

@INPROCEEDINGS{LTAC,
  AUTHOR = {Delahaye, David},
  TITLE = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}},
  BOOKTITLE = {Proceedings of Logic for Programming and Automated Reasoning
               (LPAR), Reunion Island (France)},
  PUBLISHER = {Springer-Verlag},
  SERIES = {LNCS/LNAI},
  VOLUME = 1955,
  PAGES = {85--95},
  MONTH = {November},
  YEAR = 2000,
  URL = {http://cedric.cnam.fr/~delahaye/publications/LPAR2000-ltac.ps.gz}
}

@InProceedings{del.may.2001,
  author = 	 {David ~Delahaye and Micaela ~Mayero},
  title = 	 {Field: une proc\'edure de d\'ecision pour les nombres 
                  r\'eels en Coq},
  booktitle = 	 {Proceedings of JFLA'2001},
  year = 	 {2001},
  publisher =    {INRIA},
}

@PHDTHESIS{mayero-thesis,
  AUTHOR = {Mayero, Micaela},
  TITLE = {Formalisation et automatisation de preuves en analyses r\'eelle 
           et num\'erique},
  SCHOOL = {Universit\'e Paris VI},
  MONTH = {d\'ecembre},
  YEAR = {2001},
  FTP = {ftp://ftp.inria.fr/INRIA/LogiCal/Micaela.Mayero/papers/these-mayero.ps.gz}
}

@InProceedings{edalat.98,
    author = {Abbas Edalat and Peter John Potts},
    title = {A new representation for exact real numbers},
    booktitle = entcs,
    volume = {6},
    publisher = elsevier,
    editor = {Stephen Brookes and Michael Mislove},
    year = {1998}
}


@Book{gathen.99,
  author = 	 {Gathen, Joachim von zur and J\"urgen Gerhard},
  title =        {Modern Computer Algebra},
  publisher = 	 camb,
  year = 	 {1999},
  address = 	 {Cambridge},
}



@InProceedings{geuvers.00c,
  author = 	 {Herman Geuvers and Freek Wiedijk and Jan Zwanenburg},
  title = 	 {Equational Reasoning via Partial Reflection},
  booktitle = 	 {Theorem Proving in Higher Order Logics},
  year = 	 {2000},
  editor = 	 {Mark Aagaard and John Harrison},
  number = 	 {1869},
  series = 	 {LNCS},
  address = 	 {Berlin},
  organization = {TPHOLS 2000},
  publisher =    springer,
}


@Article{geuvers.02,
  author = 	 {Herman ~Geuvers and Randy ~Pollack and Freek ~Wiedijk and 
                  Jan ~Zwanenburg},
  journal = 	 jsc,
  title = 	 {A Constructive Algebraic Hierarchy in Coq},
  note = 	 {Special Issue on the Integration of Automated Reasoning and Computer Algebra Systems,},
  pages = 	 {271-286},
  year = 	 {2002},
  volume = 	 {34},
  number = 	 {4},
  month = 	 {october},
  publisher =    elsevier,
}


@Misc{gosper.72,
  author = 	 {Ralph W. Gosper},
  title = 	 {{HAKMEM}, {I}tem 101 {B}},
  howpublished = {\url{http://www.inwap.com/pdp10/hbaker/hakmem/cf.html#item101b}},
  month = 	 {feb.},
  year = 	 {1972},
  note =         {MIT AI Laboratory Memo No.239}
}

@Book{graham.94,
  author = 	 {Ronald E. Graham and Donald E. Knuth and Oren Patashnik},
  title = 	 {Concrete Mathematics},
  publisher = 	 {Addison-Wesley},
  year = 	 {1994},
  address = 	 {Reading, Massachusetts},
  edition = 	 {Second},
}

@Book{harrison.98,
  author = 	 {John Harrison},
  title = 	 {Theorem Proving with the Real Numbers},
  publisher = 	 springer,
  year = 	 {1998},
  series = 	 {Distinguished dissertations},
  address = 	 {London},
}



@Article{hayes.00,
  author = 	 {Brian Hayes},
  title = 	 {On the Teeth of Wheels},
  journal = 	 {American Scientist},
  year = 	 {2000},
  volume = 	 {88},
  number = 	 {4},
  pages = 	 {296--300},
  month = 	 {july-august},
}

@InProceedings{heckmann.99,
    author = {Reinhold Heckmann},
    title = {How Many Argument Digits are Needed to Produce n Result Digits?},
    booktitle = entcs,
    volume = {24},
    publisher = elsevier,
    editor = {Abbas Edalat, David Matula and Philipp S\"underhauf},
    year = {1999}
}

@inproceedings{DBLP:conf/ac/EdalatH00,
  author    = {Abbas Edalat and
               Reinhold Heckmann},
  title     = {Computing with Real Numbers.},
  booktitle = {APPSEM},
  year      = {2000},
  pages     = {193-267},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2395/23950193.htm},
  crossref  = {DBLP:conf/ac/2000appsem},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@proceedings{DBLP:conf/ac/2000appsem,
  editor    = {Gilles Barthe and
               Peter Dybjer and
               Luis Pinto and
               Jo{\~a}o Saraiva},
  title     = {Applied Semantics, International Summer School, APPSEM 2000,
               Caminha, Portugal, September 9-15, 2000, Advanced Lectures},
  booktitle = {APPSEM},
  publisher = {Springer},
  series    = {Lecture Notes in Computer Science},
  volume    = {2395},
  year      = {2002},
  isbn      = {3-540-44044-5},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}


@Book{knuth.98,
  author = 	 {Donald Ervin Knuth},
  title = 	 {The Art of Computer Programming},
  publisher = 	 {Addison-Wesley},
  year = 	 {1998},
  volume = 	 {2},
  edition = 	 {3},
}


@Article{kornerup.88,
  author = 	 {Peter Kornerup and David Matula},
  title = 	 {An On-Line Arithmetic Unit for Bit-Pipelined Rational Arithmetic},
  journal = 	 {Journal of Parallel and Distributed Computing},
  year = 	 {1988},
  volume = 	 {5},
  pages = 	 {310-330},
}


@Article{kornerup.95,
  author = 	 {Peter Kornerup and David Matula},
  title = 	 {{LCF}: A Lexicographic Binary Representation of the Rationals},
  journal = 	 {Journal of Universal Computer Science},
  year = 	 {1995},
  volume = 	 {1},
  number = 	 {7},
  pages = 	 {484--503},
  month = 	 {july},
}

@Article{liardel.98,
  author = 	 {Pierre Liardel and Pierre Stambul },
  title = 	 {Algebraic Computations with Continued Fractions},
  journal = 	 {Journal of Number Theory},
  year = 	 {1998},
  volume = 	 {73},
  pages = 	 {92-121},
}

@PhdThesis{mencer.00,
  author = 	 {Oskar Mencer},
  title = 	 {Rational Arithmetic Units In Computer Systems },
  school = 	 {Stanford University},
  year = 	 {2000},
  month = 	 {feb},
}

@PhdThesis{menissier.94,
    author = {Val\'erie M\'enissier-Morain},
    title = {Arithm\'etique exacte, conception, algorithmique et
    performances d'une impl\'ementation informatique en
    pr\'ecision arbitraire},
    school = {Universit\'e Paris 7},
    type = {Th\`ese},
    year = {1994},
    month = {dec},
}

@PhdThesis{NiquiThesis,
 author = "Milad Niqui",
 title = "Formalising Exact Arithmetic, Representations, Algorithms, and
          Proofs",
 School = {University of Nijmegen},
 year = 2004,
 month = sep,
 note = "ISBN 90-9018333-7"
}

@Phdthesis{Boldo04,
  author = "Sylvie Boldo",
  title = "Preuves formelles en arithm{\'e}tiques {\`a}virgule flottante",
  school = {{\'E}cole Normale Sup'erieure de Lyon},
  year = {2004},
  month = nov
}

@inproceedings{NiquiBertot,
 author = "Milad Niqui and Yves Bertot",
 title = "QArith: Coq Formalization of Lazy Rational Arithmetic",
 booktitle = "Types for proofs and programs",
 number = 3085,
 year = 2004,
 series = "Lecture Notes in Computer Science",
 publisher = "Springer-Verlag"
}

@article{ViewLeft,
  title = "The view from the left",
  author = "Conor McBride and James McKinna",
  journal = "Journal of Functional Programming",
  volume = 14,
  number = 1,
  year = 2004
}

@InProceedings{milad.02,
  author = 	 {Herman Geuvers and Milad Niqui},
  title = 	 {Constructive Real Numbers in {C}oq: Axioms and {C}ategoricity},
  booktitle = 	 {Types for Proofs and Programs},
  publisher =    springer,
  pages = 	 {79-95},
  year = 	 {2002},
  editor = 	 {Paul Callaghan and Zhaohui Luo and James McKinna and Robert Pollack},
  volume = 	 {2277},
  series = 	 {LNCS},
  address = 	 {Durham, UK},
  note = 	 {Proceedings of TYPES2000 workshop},
}


@Misc{milad.02b,
  author = 	 {Milad Niqui},
  howpublished = {\url{http://www.cs.kun.nl/~milad/programs/coq/Stern_Brocot.tar.gz}},
  month = 	 {dec},
  year = 	 {2002},
  note = 	 {Files under Coq 7.3},
}



@Unpublished{milad.03,
  author = 	 {Milad Niqui},
  title = 	 {Exact {A}rithmetic on {S}tern-{B}rocot {T}ree},
  note = 	 {\emph{submitted}},
  month = 	 {jan},
  year = 	 {2003},
}


@Article{nielsen.95,
  author = 	 {Asger Munk Nielsen and Peter Kornerup},
  title = 	 {MSB-First Digit Serial Arithmetic},
  journal = 	 {Journal of Universal Computer Science},
  year = 	 {1995},
  volume = 	 {1},
  number = 	 {7},
  pages = 	 {527--547},
}



@book{NielsonNielson92,
  title = "Semantics with Applications: A Formal Introduction",
  author = "Hanne Riis Nielson and Flemming Nielson",
  year = "1992",
  publisher = "Wiley"
}
@PhdThesis{potts.98,
  author = 	 {Peter J. Potts},
  title = 	 {Exact Real Arithmetic using M\"obius Transformations},
  school = 	 {Uiversity of London, Imperial College},
  year = 	 {1998},
  month = 	 {jul}
}


@Article{stern.1858,
  author = 	 {Moritz Abraham Stern},
  title = 	 {Ueber eine zahlentheoretische {F}unktion},
  journal = 	 {Journal f\"ur die {R}eine und angewandte {M}athematik},
  year = 	 {1858},
  volume = 	 {55},
  pages = 	 {193--220},
}

@Article{raney.73,
  author = 	 {George N. Raney},
  title = 	 {On Continued Fractions and Finite Automata},
  journal = 	 {Mathematische Annalen},
  year = 	 {1973},
  volume = 	 {206},
  pages = 	 {265--283},
}



@Article{vuillemin.90,
  author = 	 {Jean E. Vuillemin},
  title = 	 {Exact Real Computer Arithmetic with Continued Fractions},
  journal = 	 {IEEE Transactions on Computers},
  year = 	 {1990},
  volume = 	 {39},
  number = 	 {8},
  pages = 	 {1087-1105},
  month = 	 {aug},
}

@book{BertotCasteran04,
  title = "Interactive theorem proving and program development,
Coq'art: the calculus of inductive constructions",
  author = "Yves Bertot and Pierre Cast{\'e}ran",
  publisher = "Springer-Verlag",
  year= 2004,
  Series = "Texts in Theoretical Computer Science: an EATCS series",
  ISBN = "3-540-20854-2"
}

@INPROCEEDINGS{harrison-hol99,
        crossref        = "hol99",
        author          = "John Harrison",
        title           = "A Machine-Checked Theory of Floating Point
                           Arithmetic",
        pages           = "113--130"}

@PROCEEDINGS{hol99,
        editor          = "Yves Bertot and Gilles Dowek and Andr{\'e}
                           Hirschowitz and Christine Paulin and
                           Laurent Th{\'e}ry",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           12th International Conference, TPHOLs'99",
        series          = "Lecture Notes in Computer Science",
        volume          = 1690,
        address         = "Nice, France",
        date            = "September 1999",
        year            = 1999,
        publisher       = "Springer-Verlag"}

@inproceedings{bertot05a,
  author = "Yves Bertot",
  title = "Filters on CoInductive Streams, an Application to Eratosthenes'
           sieve",
  editor = "Pawe{\l} Urzyczyn",
  booktitle = "Typed Lambda Calculi and Applications, TLCA 2005",
  location = "Nara, Japan",
  pages = "102--115",
  publisher = "Springer-Verlag",
  year =2005
}

@inproceedings{DBLP:conf/cca/Lambov05,
  author    = {Branimir Lambov},
  title     = {RealLib: an Efficient Implementation of Exact Real Arithmetic.},
  booktitle = {CCA},
  year      = {2005},
  pages     = {169-175},
  crossref  = {DBLP:conf/cca/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/lfp/BoehmCRO86,
  author    = {Hans-Juergen Boehm and
               Robert Cartwright and
               Mark Riggle and
               Michael J. O'Donnell},
  title     = {Exact Real Arithmetic: A Case Study in Higher Order Programming.},
  booktitle = {LISP and Functional Programming},
  year      = {1986},
  pages     = {162-173},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{DBLP:conf/cca/Muller05,
  author    = {Norbert Th. M{\"u}ller},
  title     = {Implementing Exact Real Numbers Efficiently.},
  booktitle = {CCA},
  year      = {2005},
  pages     = {378},
  crossref  = {DBLP:conf/cca/2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}
@incollection {BauerEscardoSimpson02,
    AUTHOR = {Bauer, A. and Escard{\'o}, M.H. and
              Simpson, A.},
     TITLE = {Comparing functional paradigms for exact real-number
              computation},
 BOOKTITLE = {Automata, languages and programming},
    SERIES = {Lecture Notes in Comput. Sci.},
    VOLUME = {2380},
     PAGES = {489--500},
 PUBLISHER = {Springer},
      YEAR = {2002},
}
@proceedings{DBLP:conf/cca/2005,
  editor    = {Tanja Grubba and
               Peter Hertling and
               Hideki Tsuiki and
               Klaus Weihrauch},
  title     = {CCA 2005 - Second International Conference on Computability
               and Complexity in Analysis, August 25-29, 2005, Kyoto, Japan},
  booktitle = {CCA},
  publisher = {FernUniversit{\"a}t Hagen, Germany},
  series    = {Informatik Berichte},
  volume    = {326-7/2005},
  year      = {2005},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{augustsson98cayenne,
    author = "Lennart Augustsson",
    title = "Cayenne - a Language with Dependent Types",
    booktitle = "International Conference on Functional Programming",
    pages = "239--250",
    year = "1998",
    url = "citeseer.ist.psu.edu/augustsson98cayenne.html" }


@inproceedings{ xi99dependent,
    author = "Howgwei Xi and Frank Pfenning",
    title = "Dependent Types in Practical Programming",
    booktitle = "Conference Record of {POPL} 99: The 26th {ACM} {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages, San Antonio, Texas",
    address = "New York, NY",
    pages = "214--227",
    year = "1999",
    url = "citeseer.ist.psu.edu/xi98dependent.html" }

@inproceedings{huet87,
  author = "G{\'e}rard Huet",
  title="Induction principles formalized in the calculus of constructions",
  booktitle = "TAPSOFT'87",
  publisher = "Springer",
  series = "LNCS",
  year = 1987,
  volume = 249,
  pages = "276--286"
}

@inproceedings{bertot-exactreals,
  author = "Yves Bertot",
  title="Calcul de formules affines et de séries entières en arithmétique exacte avec types co-inductifs",
  booktitle = "Journées francophones des langages applicatifs",
  publisher = "INRIA",
  year = 2006,
  month = "Janvier",
  editor = "Thérèse Hardin et Luc Moreau",
}

@article{1961-avizienis,
  note={URL: {\tt http://cr.yp.to/\allowbreak bib/\allowbreak entries.html\#\allowbreak 1961/\allowbreak avizienis}},
  author={Algirdas A. Avizienis},
  ISSN={0367--9950},
  journal={IRE Transactions on Electronic Computers},
  MR={24:B1263},
  pages={389--400},
  title={{Signed-digit number representations for fast parallel arithmetic}},
  volume={10},
  year={1961}
}

@InProceedings{paulin-tlca,
  author	= {Christine Paulin-Mohring},
  title		= {Inductive Definitions in the System {Coq}: Rules and
		 Properties},
  crossref	= {tlca93},
  pages		= {328-345}
}

@Proceedings{tlca93,
  title		= {Typed Lambda Calculi and Applications},
  booktitle	= {Typed Lambda Calculi and Applications},
  editor	= {M. Bezem and J.F. Groote},
  year		= 1993,
  publisher	= {Springer},
  series	= {LNCS 664}
}