Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: T4695348.out Sprache: Latech

Original von: Coq^©

@String{jfp   = "Journal of Functional Programming"}
@String{lncs  = "Lecture Notes in Computer Science"}
@String{lnai  = "Lecture Notes in Artificial Intelligence"}
@String{SV    = "{Springer-Verlag}"}

@InCollection{Asp00,
  Title        = {Proof General: A Generic Tool for Proof Development},
  Author       = {Aspinall, David},
  Booktitle    = {Tools and Algorithms for the Construction and
               Analysis of Systems, {TACAS} 2000},
  Publisher    = {Springer Berlin Heidelberg},
  Year         = {2000},
  Editor       = {Graf, Susanne and Schwartzbach, Michael},
  Pages        = {38--43},
  Series       = {Lecture Notes in Computer Science},
  Volume       = {1785},
  Doi          = {10.1007/3-540-46419-0_3},
  ISBN         = {978-3-540-67282-1},
}

@Book{Bar81,
  author      = {H.P. Barendregt},
  publisher   = {North-Holland},
  title       = {The Lambda Calculus its Syntax and Semantics},
  year        = {1981}
}

@InProceedings{Bou97,
  title       = {Using reflection to build efficient and certified decision procedure
s},
  author      = {S. Boutin},
  booktitle   = {TACS'97},
  editor      = {Martin Abadi and Takahashi Ito},
  publisher   = SV,
  series      = lncs,
  volume      = 1281,
  year        = {1997}
}

@Article{Bru72,
  author      = {N.J. de Bruijn},
  journal     = {Indag. Math.},
  title       = {{Lambda-Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with Application to the Church-Rosser Theorem}},
  volume      = {34},
  year        = {1972}
}

@inproceedings{CH85,
  title={Constructions: a higher order proof system for mechanizing mathematics},
  author={Coquand, Thierry and Huet, Gérard},
  booktitle={European Conference on Computer Algebra},
  pages={151--184},
  year={1985},
  issn         = {1611-3349},
  doi          = {10.1007/3-540-15983-5_13},
  url          = {http://dx.doi.org/10.1007/3-540-15983-5_13},
  isbn         = 9783540396840,
  publisher    = {Springer Berlin Heidelberg}
}

@techreport{CH88
  TITLE = {{The calculus of constructions}},
  AUTHOR = {Coquand, T. and Huet, G{\'e}rard},
  URL = {https://hal.inria.fr/inria-00076024},
  NUMBER = {RR-0530},
  INSTITUTION = {{INRIA}},
  YEAR = {1986},
  MONTH = May,
  PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf},
  HAL_ID = {inria-00076024},
  HAL_VERSION = {v1},
}

@techreport{CH87,
  TITLE = {{Concepts mathematiques et informatiques formalises dans le calcul des constructions}},
  AUTHOR = {Coquand, T. and Huet, G{\'e}rard},
  URL = {https://hal.inria.fr/inria-00076039},
  NUMBER = {RR-0515},
  INSTITUTION = {{INRIA}},
  YEAR = {1986},
  MONTH = Apr,
  PDF = {https://hal.inria.fr/inria-00076039/file/RR-0515.pdf},
  HAL_ID = {inria-00076039},
  HAL_VERSION = {v1},
}

@techreport{C90,
  TITLE = {{Metamathematical investigations of a calculus of constructions}},
  AUTHOR = {Coquand, T.},
  URL = {https://hal.inria.fr/inria-00075471},
  NUMBER = {RR-1088},
  INSTITUTION = {{INRIA}},
  YEAR = {1989},
  MONTH = Sep,
  PDF = {https://hal.inria.fr/inria-00075471/file/RR-1088.pdf},
  HAL_ID = {inria-00075471},
  HAL_VERSION = {v1},
}

@PhDThesis{Coq85,
  author      = {Th. Coquand},
  month       = jan,
  school      = {Universit\'e Paris~7},
  title       = {Une Th\'eorie des Constructions},
  year        = {1985}
}

@InProceedings{Coq86,
  author      = {Th. Coquand},
  address     = {Cambridge, MA},
  booktitle   = {Symposium on Logic in Computer Science},
  publisher   = {IEEE Computer Society Press},
  title       = {{An Analysis of Girard's Paradox}},
  year        = {1986}
}

@InProceedings{Coq92,
  author      = {Th. Coquand},
  title       = {{Pattern Matching with Dependent Types}},
  year        = {1992},
  booktitle   = {Proceedings of the 1992 Workshop on Types for Proofs and Programs}
}

@InProceedings{DBLP:conf/types/CornesT95,
  author    = {Cristina Cornes and
               Delphine Terrasse},
  title     = {Automating Inversion of Inductive Predicates in Coq},
  booktitle = {TYPES},
  year      = {1995},
  pages     = {85-104},
  crossref  = {DBLP:conf/types/1995},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@inproceedings{CP90,
  title={Inductively defined types},
  author={Coquand, Thierry and Paulin, Christine},
  booktitle={COLOG-88},
  pages={50--66},
  year={1990},
  issn         = {1611-3349},
  doi          = {10.1007/3-540-52335-9_47},
  url          = {http://dx.doi.org/10.1007/3-540-52335-9_47},
  isbn         = 9783540469636,
  publisher    = {Springer Berlin Heidelberg}
}

@Book{Cur58,
  author      = {Haskell B. Curry and Robert Feys and William Craig},
  title       = {Combinatory Logic},
  volume      = 1,
  publisher   = "North-Holland",
  year        = 1958,
  note        = {{\S{9E}}},
}

@Article{CSlessadhoc,
author = {Gonthier, Georges and Ziliani, Beta and Nanevski, Aleksandar and Dreyer, Derek},
title = {How to Make Ad Hoc Proof Automation Less Ad Hoc},
journal = {SIGPLAN Not.},
issue_date = {September 2011},
volume = {46},
number = {9},
month = sep,
year = {2011},
issn = {0362-1340},
pages = {163--175},
numpages = {13},
url = {http://doi.acm.org/10.1145/2034574.2034798},
doi = {10.1145/2034574.2034798},
acmid = {2034798},
publisher = {ACM},
address = {New York, NY, USA},
keywords = {canonical structures, coq, custom proof automation, hoare type theory, interactive theorem proving, tactics, type classes},
}

@InProceedings{CSwcu,
    hal_id = {hal-00816703},
    url = {http://hal.inria.fr/hal-00816703},
    title = {{Canonical Structures for the working Coq user}},
    author = {Mahboubi, Assia and Tassi, Enrico},
    booktitle = {{ITP 2013, 4th Conference on Interactive Theorem Proving}},
    publisher = {Springer},
    pages = {19-34},
    address = {Rennes, France},
    volume = {7998},
    editor = {Sandrine Blazy and Christine Paulin and David Pichardie },
    series = {LNCS },
    doi = {10.1007/978-3-642-39634-2_5},
    year = {2013},
}

@InProceedings{Del00,
  author      = {Delahaye, D.},
  title       = {A {T}actic {L}anguage for the {S}ystem {{\sf Coq}}},
  booktitle   = {Proceedings of Logic for Programming and Automated Reasoning
               (LPAR), Reunion Island},
  publisher   = SV,
  series      =  LNCS,
  volume      = {1955},
  pages       = {85--95},
  month       = {November},
  year        = {2000},
  url         = {http://www.lirmm.fr/%7Edelahaye/papers/ltac%20(LPAR%2700).pdf}
}

@Article{Dyc92,
  author      = {Roy Dyckhoff},
  journal     = {The Journal of Symbolic Logic},
  month       = sep,
  number      = {3},
  title       = {Contraction-free sequent calculi for intuitionistic logic},
  volume      = {57},
  year        = {1992}
}

@Book{Fourier,
  author      = {Jean-Baptiste-Joseph Fourier},
  publisher   = {Gauthier-Villars},
  title       = {Fourier's method to solve linear
                 inequations/equations systems.},
  year        = {1890}
}

@InProceedings{Gim94,
  author      = {E. Gim\'enez},
  booktitle   = {Types'94 : Types for Proofs and Programs},
  note        = {Extended version in LIP research report 95-07, ENS Lyon},
  publisher   = SV,
  series      = LNCS,
  title       = {Codifying guarded definitions with recursive schemes},
  volume      = {996},
  year        = {1994}
}

@TechReport{Gim98,
  author      = {E. Gim\'enez},
  title       = {A Tutorial on Recursive Types in Coq},
  institution = {INRIA},
  year        = 1998,
  month       = mar
}

@Unpublished{GimCas05,
  author      = {E. Gim\'enez and P. Cast\'eran},
  title       = {A Tutorial on [Co-]Inductive Types in Coq},
  institution = {INRIA},
  year        = 2005,
  month       = jan,
  note        = {available at \url{http://coq.inria.fr/doc}}
}

@InProceedings{Gimenez95b,
  author      = {E. Gim\'enez},
  booktitle   = {Workshop on Types for Proofs and Programs},
  series      = LNCS,
  number      = {1158},
  pages       = {135-152},
  title       = {An application of co-Inductive types in Coq:
                 verification of the Alternating Bit Protocol},
  editorS     = {S. Berardi and M. Coppo},
  publisher   = SV,
  year        = {1995}
}

@Book{Gir89,
  author      = {J.-Y. Girard and Y. Lafont and P. Taylor},
  publisher   = {Cambridge University Press},
  series      = {Cambridge Tracts in Theoretical Computer Science 7},
  title       = {Proofs and Types},
  year        = {1989}
}

@InCollection{How80,
  author      = {W.A. Howard},
  booktitle   = {to H.B. Curry : Essays on Combinatory Logic, Lambda Calculus and Formalism.},
  editor      = {J.P. Seldin and J.R. Hindley},
  note        = {Unpublished 1969 Manuscript},
  publisher   = {Academic Press},
  title       = {The Formulae-as-Types Notion of Constructions},
  year        = {1980}
}

@inproceedings{H88,
  title={Induction principles formalized in the Calculus of Constructions},
  author={Huet, G{\'e}rard},
  booktitle={Programming of Future Generation Computers. Elsevier Science},
  year={1988},
  issn         = {1611-3349},
  doi          = {10.1007/3-540-17660-8_62},
  url          = {http://dx.doi.org/10.1007/3-540-17660-8_62},
  isbn         = 9783540477464,
  publisher    = {Springer Berlin Heidelberg}
}

@InProceedings{H89,
  author      = {G. Huet},
  booktitle   = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney},
  editor      = {R. Narasimhan},
  publisher   = {World Scientific Publishing},
  title       = {{The Constructive Engine}},
  year        = {1989}
}

@Article{LeeWerner11,
  author    = {Gyesik Lee and
               Benjamin Werner},
  title     = {Proof-irrelevant model of {CC} with predicative induction
               and judgmental equality},
  journal   = {Logical Methods in Computer Science},
  volume    = {7},
  number    = {4},
  year      = {2011},
  ee        = {http://dx.doi.org/10.2168/LMCS-7(4:5)2011},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@TechReport{Leroy90,
  author      = {X. Leroy},
  title       = {The {ZINC} experiment: an economical implementation of the {ML} language},
  institution = {INRIA},
  number      = {117},
  year        = {1990}
}

@InProceedings{Let02,
  author      = {P. Letouzey},
  title       = {A New Extraction for Coq},
  booktitle   = {TYPES},
  year        = 2002,
  crossref    = {DBLP:conf/types/2002},
  url         = {http://www.irif.fr/~letouzey/download/extraction2002.pdf}
}

@InProceedings{Luttik97specificationof,
  author = {Sebastiaan P. Luttik and Eelco Visser},
  booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
  publisher = SV,
  title = {Specification of Rewriting Strategies},
  year = {1997}
}

@InProceedings{DBLP:conf/types/McBride00,
  author    = {Conor McBride},
  title     = {Elimination with a Motive},
  booktitle = {TYPES},
  year      = {2000},
  pages     = {197-216},
  ee        = {http://link.springer.de/link/service/series/0558/bibs/2277/22770197.htm},
  crossref  = {DBLP:conf/types/2000},
  bibsource = {DBLP, http://dblp.uni-trier.de}
}

@InProceedings{Moh93,
  author      = {C. Paulin-Mohring},
  booktitle   = {Proceedings of the conference Typed Lambda Calculi and Applications},
  editor      = {M. Bezem and J.-F. Groote},
  note        = {Also LIP research report 92-49, ENS Lyon},
  number      = {664},
  publisher   = SV,
  series      = {LNCS},
  title       = {{Inductive Definitions in the System Coq - Rules and Properties}},
  year        = {1993}
}

@MastersThesis{Mun94,
  author      = {C. Muñoz},
  month       = sep,
  school      = {DEA d'Informatique Fondamentale, Universit\'e Paris 7},
  title       = {D\'emonstration automatique dans la logique propositionnelle intuitionniste},
  year        = {1994}
}

@Article{Myers,
  author    = {Eugene Myers},
  title     = {An {O(ND)} difference algorithm and its variations},
  journal   = {Algorithmica},
  volume    = {1},
  number    = {2},
  year      = {1986},
  bibsource = {https://link.springer.com/article/10.1007\%2FBF01840446},
  url       = {http://www.xmailserver.org/diff2.pdf}
}

@inproceedings{P86,
  title={Algorithm development in the calculus of constructions},
  author={Mohring, Christine},
  booktitle={LICS},
  pages={84--91},
  year={1986}
}

@inproceedings{P89,
  title={Extracting $\Omega$'s programs from proofs in the calculus of constructions},
  author={Paulin-Mohring, Christine},
  booktitle={Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages},
  pages={89--104},
  year={1989},
  doi          = {10.1145/75277.75285},
  url          = {http://dx.doi.org/10.1145/75277.75285},
  isbn         = 0897912942,
  organization = {ACM Press}
}

@inproceedings{P93,
  title={Inductive definitions in the system coq rules and properties},
  author={Paulin-Mohring, Christine},
  booktitle={International Conference on Typed Lambda Calculi and Applications},
  pages={328--345},
  year={1993},
  doi          = {10.1007/bfb0037116},
  url          = {http://dx.doi.org/10.1007/bfb0037116},
  isbn         = 3540565175,
  organization = {Springer-Verlag}
}

@inproceedings{PP90,
  title={Inductively defined types in the Calculus of Constructions},
  author={Pfenning, Frank and Paulin-Mohring, Christine},
  booktitle={International Conference on Mathematical Foundations of Programming Semantics},
  pages={209--228},
  year={1989},
  doi          = {10.1007/bfb0040259},
  url          = {http://dx.doi.org/10.1007/bfb0040259},
  isbn         = 0387973753,
  organization = {Springer-Verlag}
}

@InProceedings{Parent95b,
  author      = {C. Parent},
  booktitle   = {{Mathematics of Program Construction'95}},
  publisher   = SV,
  series      = {LNCS},
  title       = {{Synthesizing proofs from programs in
the Calculus of Inductive Constructions}},
  volume      = {947},
  year        = {1995}
}

@InProceedings{Pit16,
  Title        = {Company-Coq: Taking Proof General one step closer to a real IDE},
  Author       = {Pit-Claudel, Clément and Courtieu, Pierre},
  Booktitle    = {CoqPL'16: The Second International Workshop on Coq for PL},
  Year         = {2016},
  Month        = jan,
  Doi          = {10.5281/zenodo.44331},
}

@Book{RC95,
  author      = {di~Cosmo, R.},
  title       = {Isomorphisms of Types: from $\lambda$-calculus to information
                 retrieval and language design},
  series      = {Progress in Theoretical Computer Science},
  publisher   = {Birkhauser},
  year        = {1995},
  note        = {ISBN-0-8176-3763-X}
}

@Article{Rushby98,
  title       = {Subtypes for Specifications: Predicate Subtyping in
                {PVS}},
  author      = {John Rushby and Sam Owre and N. Shankar},
  journal     = {IEEE Transactions on Software Engineering},
  pages       = {709--720},
  volume      = 24,
  number      = 9,
  month       = sep,
  year        = 1998
}

@InProceedings{sozeau06,
  author = {Matthieu Sozeau},
  title = {Subset Coercions in {C}oq},
  year = {2007},
  booktitle = {TYPES'06},
  pages = {237-252},
  volume = {4502},
  publisher = "Springer",
  series =    {LNCS}
}

@InProceedings{sozeau08,
        Author = {Matthieu Sozeau and Nicolas Oury},
        booktitle = {TPHOLs'08},
        Pdf = {http://www.lri.fr/~sozeau/research/publications/drafts/classes.pdf},
        Title = {{F}irst-{C}lass {T}ype {C}lasses},
        Year = {2008},
}

@InProceedings{sugar,
    author = {Alessandro Giovini and Teo Mora and Gianfranco Niesi and Lorenzo Robbiano and Carlo Traverso},
    title = {"One sugar cube, please" or Selection strategies in the Buchberger algorithm},
    booktitle = { Proceedings of the ISSAC'91, ACM Press},
    year = {1991},
    pages = {5--4},
    publisher = {}
}

@Article{TheOmegaPaper,
    author = "W. Pugh",
    title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis",
    journal = "Communication of the ACM",
    pages = "102--114",
    year = "1992",
}

@PhDThesis{Wer94,
  author      = {B. Werner},
  school      = {Universit\'e Paris 7},
  title       = {Une th\'eorie des constructions inductives},
  type        = {Th\`ese de Doctorat},
  year        = {1994}
}

@InProceedings{CompiledStrongReduction,
  author    = {Benjamin Gr{\'{e}}goire and
               Xavier Leroy},
  editor    = {Mitchell Wand and
               Simon L. Peyton Jones},
  title     = {A compiled implementation of strong reduction},
  booktitle = {Proceedings of the Seventh {ACM} {SIGPLAN} International Conference
               on Functional Programming {(ICFP} '02), Pittsburgh, Pennsylvania,
               USA, October 4-6, 2002.},
  pages     = {235--246},
  publisher = {{ACM}},
  year      = {2002},
  url       = {http://doi.acm.org/10.1145/581478.581501},
  doi       = {10.1145/581478.581501},
  timestamp = {Tue, 11 Jun 2013 13:49:16 +0200},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/icfp/GregoireL02},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

@InProceedings{FullReduction,
  author    = {Mathieu Boespflug and
               Maxime D{\'{e}}n{\`{e}}s and
               Benjamin Gr{\'{e}}goire},
  editor    = {Jean{-}Pierre Jouannaud and
               Zhong Shao},
  title     = {Full Reduction at Full Throttle},
  booktitle = {Certified Programs and Proofs - First International Conference, {CPP}
               2011, Kenting, Taiwan, December 7-9, 2011. Proceedings},
  series    = {Lecture Notes in Computer Science},
  volume    = {7086},
  pages     = {362--377},
  publisher = {Springer},
  year      = {2011},
  url       = {http://dx.doi.org/10.1007/978-3-642-25379-9_26},
  doi       = {10.1007/978-3-642-25379-9_26},
  timestamp = {Thu, 17 Nov 2011 13:33:48 +0100},
  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/cpp/BoespflugDG11},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.