Attention: Maintenance on monday 19.04.2021 from 07:00 - 13:00 (Gitlab and Mattermost are offline!)

Commit 92e8dcaa authored by Michael Kohlhase's avatar Michael Kohlhase

more

parent 2857786e
......@@ -10,3 +10,4 @@ auto
*.run.xml
*.synctex.gz
*.toc
*.xml
%Systems and applications
@inproceedings{comparing,
AUTHOR = {F. Wiedijk},
TITLE = "{Comparing mathematical provers}",
BOOKTITLE = "{Proceedings of Mathematical Knowledge Management}",
YEAR = {2003},
EDITOR = {A. Asperti and B. Buchberger and J. Davenport},
PAGES = {188-202},
PUBLISHER = {Springer},
}
@inproceedings{pvs,
AUTHOR = {S. Owre and J. Rushby and N. Shankar},
TITLE = "{PVS: A Prototype Verification System}",
BOOKTITLE = "{11th International Conference on Automated Deduction (CADE)}",
YEAR = {1992},
EDITOR = {D. Kapur},
PAGES = {748--752},
PUBLISHER = {Springer},
}
@InProceedings{pvs_shostak_decon,
author = "H. Rue{\ss} and N. Shankar",
title = "Deconstructing {S}hostak",
editor = "J. Halpern",
booktitle = "Logic in Computer Science",
year = "2001",
publisher = "IEEE Computer Society",
pages = "19--28",
}
@misc{nasapvs,
author = "NASA Langley",
title = "{NASA PVS Library}",
note = "\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html}",
year = 2014,
}
@inproceedings{specware,
title = "{Specware: Formal Support for Composing Software}",
author = "Y. Srinivas and R. J{\"u}llig",
booktitle = "Mathematics of Program Construction",
editor = "B. M{\"o}ller",
year = 1995,
publisher = "Springer",
}
@TECHREPORT{pvssemantics,
author = "S. Owre and N. Shankar",
title = "The formal semantics of {PVS}",
institution = "SRI International",
year = "1997",
number = "SRI-CSL-97-2",
}
@book{nuprl,
author = "R. Constable and S. Allen and H. Bromley and W. Cleaveland and J. Cremer and R. Harper and D. Howe and T. Knoblock and N. Mendler and P. Panangaden and J. Sasaki and S. Smith",
title = "{Implementing Mathematics with the Nuprl Development System}",
publisher = "Prentice-Hall",
year = 1986,
}
@incollection{nuprl_classes,
title = "{Nuprl's Class Theory and Its Applications}",
author = "R. Constable and J. Hickey",
booktitle = "{Foundations of Secure Computation}",
editor = "F. Bauer and R. Steinbruggen",
publisher = "{IOS Press}",
pages = "91--115",
year = "2000",
}
@Inproceedings{delphin,
author = "A. Poswolsky and C. Sch{\"u}rmann",
title = "{System Description: Delphin - A Functional Programming Language for Deductive Systems}",
booktitle = "{International Workshop on Logical Frameworks and Metalanguages: Theory and Practice}",
year = "2008",
editor = "A. Abel and C. Urban",
pages = "135--141",
publisher = "ENTCS",
}
@phdthesis{agdaphd,
author = "U. Norell",
title = "{Towards a practical programming language based on dependent type theory}",
school = "{Chalmers University of Technology and G{\"o}teborg University}",
year = "2007",
}
@misc{agda,
author = "U. Norell",
title = "{The Agda WiKi}",
note = {\url{http://wiki.portal.chalmers.se/agda}},
year = "2005",
}
@InCollection{hol,
author = "M. Gordon",
editor = "G. Birtwistle and P. Subrahmanyam",
year = "1988",
title = "{HOL: A Proof Generating System for Higher-Order Logic}",
booktitle = "{VLSI Specification, Verification and Synthesis}",
pages = "73--128",
publisher = "{Kluwer-Academic Publishers}",
}
@InCollection{holsemantics,
author = "M. Gordon and A. Pitts",
title = "{The HOL Logic}",
booktitle = "{Introduction to HOL, Part III}",
editor = "M. Gordon and T. Melham",
publisher = "Cambridge University Press",
year = "1993",
pages = "191--232",
}
@Book{holbook,
author = "M. Gordon and T. Melham",
title = "{Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic}",
publisher = "Cambridge University Press",
year = "1993",
}
@misc{hol4,
key = "HOL4",
author = "{HOL4 development team}",
note = "\url{http://hol.sourceforge.net/}",
}
@misc{proofpower,
author = "R. Arthan",
title = "{ProofPower}",
note = "\url{http://www.lemma-one.com/ProofPower/}",
}
@inproceedings{hollight,
author = "J. Harrison",
title ="{HOL Light: A Tutorial Introduction}",
pages = "265--269",
booktitle = "{Proceedings of the First International Conference on Formal Methods in Computer-Aided Design}",
year = "1996",
publisher = "Springer",
}
@InProceedings{hollight_hints,
title = "{Automated Reasoning Service for HOL Light}",
author = "C. Kaliszyk and J. Urban",
booktitle = "Intelligent Computer Mathematics",
publisher = "Springer",
year = "2013",
editor = "J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger",
pages = "120--135",
}
@INPROCEEDINGS{hollight_realclosedfield,
title = "A Proof-Producing Decision Procedure for Real Arithmetic",
author = "S. McLaughlin and J. Harrison",
booktitle = "Automated Deduction",
editor = "R. Nieuwenhuis",
publisher = "Springer",
year = 2005,
pages = "295--314"
}
@Article{isabelle1,
author = "L. Paulson",
title = "{The Foundation of a Generic Theorem Prover}",
journal = "{Journal of Automated Reasoning}",
pages = "363--397",
volume = "5",
number = "3",
year = "1989",
}
@InProceedings{isabelle2,
author = "L. Paulson",
title = "{Isabelle: The Next 700 Theorem Provers}",
year = "1990",
pages = "361--386",
editor = "P. Odifreddi",
publisher = "Academic Press",
booktitle = "Logic and Computer Science",
}
@misc{isabellemanual,
author = "M. Wenzel",
title = "{The Isabelle/Isar Reference Manual}",
note = "\url{http://isabelle.in.tum.de/documentation.html}, Dec 3, 2009",
year = "2009",
}
@Book{isabelle,
author = "L. Paulson",
title = "{Isabelle: A Generic Theorem Prover}",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "828",
year = "1994",
}
@Book{isabellehol,
author= {T. Nipkow and L. Paulson and M. Wenzel},
title= "{Isabelle/HOL --- A Proof Assistant for Higher-Order Logic}",
publisher= {Springer},
year= "2002"
}
@misc{isabelle_zf,
author = "L. Paulson and M. Coen",
title = "{Zermelo-Fraenkel Set Theory}",
note = "{Isabelle distribution, ZF/ZF.thy}",
year = 1993,
}
@InProceedings{isabelle_documentoriented,
title = "Isabelle as a Document-Oriented Proof Assistant",
author = "M. Wenzel",
booktitle = "Intelligent Computer Mathematics",
publisher = "Springer",
year = "2011",
editor = "J. Davenport and W. Farmer and J. Urban and F. Rabe",
pages = "244--259",
}
@InProceedings{isabelle_jedit,
title = "{Isabelle/jEdit - {A} Prover {IDE} within the {PIDE} Framework}",
author = "M. Wenzel",
booktitle = "Intelligent Computer Mathematics",
year = "2012",
editor = "J. Jeuring and J. Campbell and J. Carette and G. Dos Reis and P. Sojka and M. Wenzel and V. Sorge",
pages = "468--471",
}
@InProceedings{isabelle_async,
title = "{Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit}",
author = "M. Wenzel",
booktitle = "{User Interfaces for Theorem Provers}",
editor = "D. Aspinall and C. {Sacerdoti Coen}",
year = "2010",
publisher = "ENTCS",
pages = "101--114",
}
@InProceedings{isar,
title = "{Isar - A Generic Interpretative Approach to Readable Formal Proof Documents}",
author = "M. Wenzel",
booktitle = "Theorem Proving in Higher Order Logics",
publisher = "Springer",
year = "1999",
editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Th{\'e}ry",
pages = "167--184",
}
@misc{isabellehol2,
author= {T. Nipkow and L. Paulson and M. Wenzel},
title= "{Isabelle's Logics: HOL}",
year= "2004",
note= {\url{http://isabelle.in.tum.de/dist/Isabelle2004/doc/logics-HOL.pdf}}
}
@InProceedings{isabelle_locales,
title = "{Locales -- a Sectioning Concept for Isabelle}",
author = "F. Kamm{\"u}ller and M. Wenzel and L. Paulson",
editor = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Thery",
year = "1999",
booktitle = "{Theorem Proving in Higher Order Logics}",
publisher = "Springer",
pages = "149--166"
}
@InProceedings{isabelle_classes,
title = "{Constructive Type Classes in Isabelle}",
author = "F. Haftmann and M. Wenzel",
publisher = "Springer",
year = "2006",
booktitle = "TYPES conference",
editor = "T. Altenkirch and C. McBride",
pages = "160--174",
}
@misc{isabelle_library,
title = "Isabelle Library",
key = "Isabelle",
year = 2008,
note = "\url{http://isabelle.in.tum.de/dist/library/index.html}",
}
@InProceedings{isabellehol_codegen,
title = "{Code Generation via Higher-Order Rewrite Systems}",
author = "F. Haftmann and T. Nipkow",
booktitle = "Functional and Logic Programming",
publisher = "Springer",
year = "2010",
editor = "M. Blume and N. Kobayashi and G. Vidal",
pages = "103--117",
}
@TechReport{isabelle_nuprl,
title = "{Formalization of Isabelle Meta Logic in NuPRL}",
author = "P. Naumov",
year = "1999",
institution = "Cornell",
}
@InProceedings{proof_general,
title = "{Proof General: {A} Generic Tool for Proof Development}",
author = "D. Aspinall",
booktitle = "Tools and Algorithms for Construction and Analysis of Systems",
publisher = "Springer",
year = "2000",
editor = "S. Graf and M. Schwartzbach",
pages = "38--42",
}
@InProceedings{lambdaprolog,
author = "D. Miller and G. Nadathur",
title = "Higher-order logic programming",
booktitle = "Proceedings of the Third International Conference on Logic Programming",
year = "1986",
editor = "E. Shapiro",
publisher = "Springer",
pages = "448--462",
}
@Book{acl2,
author = "M. Kaufmann and P. Manolios and J Moore",
title = "{Computer-Aided Reasoning: An Approach}",
publisher = "Kluwer Academic Publishers",
year = "2000",
}
@InProceedings{acl2sedan,
title = "{ACL2s: The ACL2 Sedan}",
author = "P. Dillinger and P. Manolios and D. Vroon and J. Strother Moore",
booktitle = "Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)",
editor = "S. Autexier and C. Benzm{\"u}ller",
pages = "3--18",
year = "2007",
}
@InProceedings{chiron_biform,
title = "{Biform Theories in Chiron}",
author = "W. Farmer",
booktitle = "Towards Mechanized Mathematical Assistants",
publisher = "Springer",
year = "2007",
editor = "M. Kauers and M. Kerber and R. Miner and W. Windsteiger",
pages = "66--79",
series = "Lecture Notes in Computer Science",
volume = "4573",
}
@Article{tps,
title = "{TPS: A Theorem-Proving System for Classical Type Theory}",
author = "P. Andrews and M. Bishop and S. Issar and D. Nesmith and F. Pfenning and H. Xi",
journal = "{Journal of Automated Reasoning}",
pages = "321--353",
year = "1996",
volume = "16",
number = "3",
}
@Article{imps,
author = "W. Farmer and J. Guttman and F. Thayer",
title = "{IMPS: An Interactive Mathematical Proof System}",
journal = "{Journal of Automated Reasoning}",
pages = "213--248",
volume = "11",
number = "2",
year = "1993",
}
@InProceedings{lutins,
author = "{J. Guttman}",
title = "An Interface Logic for Verification Environments",
editor = "M. Archer and J. Joyce and K. Levitt and P. Windley",
booktitle = "{International Workshop on Higher Order Logic Theorem Proving and its Applications}",
publisher = "IEEE Computer Society Press",
year = "1991",
}
@InProceedings{alf,
author = "L. Magnusson and B. Nordstr{\"o}m",
title = "{The ALF proof editor and its proof engine}",
booktitle = "{Types for Proofs and Programs}",
editor = "H. Barendregt and T. Nipkow",
year = "1994",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
volume = "806",
pages = "213--237",
}
@Book{coqbook,
author= {Y. Bertot and P. Cast{\'e}ran},
title= {Coq'Art: The Calculus of Inductive Constructions},
publisher= {Springer},
year= "2004",
}
@techreport{coq,
author = "{Coq Development Team}",
title = "{The Coq Proof Assistant: Reference Manual}",
institution = "INRIA",
year = 2015
}
@misc{coq_library,
title = "Coq Library",
key = "Coq",
year = 2008,
note = "\url{http://coq.inria.fr/library-eng.html}",
}
@incollection{coq_cct,
author = "G. Huet and A. Sa{\"\i}bi",
title = "Constructive category theory",
editor = "G. Plotkin and C. Stirling and M. Tofte",
booktitle = "{Proof, Language and Interaction: Essays in Honour of Robin Milner}",
year = "1998",
publisher = "MIT Press"
}
@techreport{coq_ssreflect,
title = "{A Small Scale Reflection Extension for the Coq system}",
author = "G. Gonthier and A. Mahboubi",
institution = "{INRIA}",
number = "{RR-6455}",
year = {2008},
}
@InProceedings{gonthier_packaging,
title = "Packaging Mathematical Structures",
author = "F. Garillot and G. Gonthier and A. Mahboubi and L. Rideau",
booktitle = "Theorem Proving in Higher Order Logics",
publisher = "Springer",
year = "2009",
editor = "S. Berghofer and T. Nipkow and C. Urban and M. Wenzel",
pages = "327--342",
}
@InProceedings{dedukti,
author = "M. Boespflug and Q. Carbonneaux and O. Hermant",
title = "The {$\lambda\Pi$}-calculus modulo as a universal proof language",
editor = "D. Pichardie and T. Weber",
booktitle = "Proceedings of PxTP2012: Proof Exchange for Theorem Proving",
pages = "28--43",
year = "2012",
}
@misc{holide,
author = "A. Assaf and G. Burel",
title = "Holide",
note = "\url{https://www.rocq.inria.fr/deducteam/Holide/index.html}",
year = 2013,
}
@inproceedings{coqine,
author = "M. Boespflug and G. Burel",
title = "{CoqInE: Translating the Calculus of Inductive Constructions into the lambda Pi-calculus Modulo}",
booktitle = "Proof Exchange for Theorem Proving",
editor = "D. Pichardie and T. Weber",
year = 2012,
}
@InProceedings{lambdaPimodulo,
title = "Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo",
author = "D. Cousineau and G. Dowek",
booktitle = "Typed Lambda Calculi and Applications",
publisher = "Springer",
year = "2007",
editor = "S. Ronchi Della Rocca",
pages = "102--117",
}
@misc{focalize,
author = "T. Hardin and others",
title = "The FoCaLiZe Essential",
note = "\url{http://focalize.inria.fr/}",
year = 2012
}
@Book{bmethod,
author = "J. Abrial",
title = "{The B-Book: Assigning Programs to Meanings}",
publisher = "Cambridge University Press",
year = "1996",
}
@InProceedings{etb,
title = "{Tool Integration with the Evidential Tool Bus}",
author = "S. Cruanes and G. Hamon and S. Owre and N. Shankar",
booktitle = "Verification, Model Checking, and Abstract Interpretation",
publisher = "Springer",
year = "2013",
editor = "R. Giacobazzi and J. Berdine and I. Mastroeni",
pages = "275--294",
}
@inproceedings{why3,
author = {F. Bobot and J. Filli{\^a}tre and C. March{\'e} and A. Paskevich},
title = "{Why3: Shepherd Your Herd of Provers}",
booktitle = "{Boogie 2011: First International Workshop on Intermediate Verification Languages}",
year = 2011,
pages = {53--64},
}
@Book{caslmanual,
author = "{CoFI (The Common Framework Initiative)}",
title = "{CASL Reference Manual}",
year = "2004",
publisher = "Springer",
series = "LNCS",
volume = "2960",
}
@incollection{obj,
author = "J. Goguen and Timothy Winkler and J. Meseguer and K. Futatsugi and J. Jouannaud",
title = "{Introducing OBJ}",
booktitle = "Applications of Algebraic Specification using {OBJ}",
publisher = "Cambridge",
editor = "J. Goguen and D. Coleman and R. Gallimore",
year = "1993",
}
@Article{clear,
title = "The Semantics of {Clear}, a Specification Language",
author = "Joseph A. Goguen and Rod M. Burstall",
journal = "Journal of the ACM",
publisher = "Springer",
volume = "39",
number = "1",
pages = "95--146",
year = "1980",
}
@InProceedings{aspinallaslplus,
author = "D. Aspinall",
title = "{Types, Subtypes, and ASL+}",
editor = "E. Astesiano and G. Reggio and A. Tarlecki",
booktitle = "{Recent Trends in Data Type Specification}",
publisher = "Springer",
year = "1994",
pages = "116--131",
}
@InProceedings{asl,
title = "{A Kernel Language for Algebraic Specification and Implementation}",
author = "D. Sannella and M. Wirsing",
booktitle = "{Fundamentals of Computation Theory}",
publisher = "Springer",
year = "1983",
editor = "M. Karpinski",
pages = "413--427",
}
@Article{extendedml,
title = "{The definition of extended ML: A gentle introduction}",
author = "S. Kahrs and D. Sannella and A. Tarlecki",
pages = "445--484",
journal = "Theoretical Computer Science",
year = "1997",
volume = "173",
number = "2",
}
@Article{aslplus,
author = "D. Sannella and S. Sokolowski and A. Tarlecki",
title = "{Toward Formal Development of Programs from Algebraic Specifications: Parameterisation Revisited}",
journal = "{Acta Informatica}",
volume = "29",
number = "8",
year = "1992",
pages = "689--736",
}
@inproceedings{maude,
author = "M. Clavel and S. Eker and P. Lincoln and J. Meseguer",
title = "Principles of {Maude}",
booktitle = "Proceedings of the First International Workshop on Rewriting Logic",
volume = "4",
editor = "J. Meseguer",
pages = "65--89",
year = "1996",
}
@inproceedings{maude_rewriting,
author = "R. Bruni and J. Meseguer",
title = "Generalized rewrite theories",
booktitle = "Proceedings of ICALP '03.",
publisher = "Springer",
year = "2003",
}
@INPROCEEDINGS{omega,
author = {C. Benzm{\"u}ller and L. Cheikhrouhou and D. Fehrer and A. Fiedler and X. Huang and M. Kerber and M. Kohlhase and K. Konrad and E. Melis and A. Meier and W. Schaarschmidt and J. Siekmann and V. Sorge},
title = "{$\Omega$MEGA: Towards a mathematical assistant}",
booktitle = "{Proceedings of the 14th Conference on Automated Deduction}",
editor = {W. McCune},
publisher = {Springer},
year = {1997},
pages = {252--255},
}
@InProceedings{mathweb,
author = "A. Franke and M. Kohlhase",
title = "{System Description: MATHWEB, an Agent-Based Communication Layer for Distributed Automated Theorem Proving}",
editor = "H. Ganzinger",
booktitle = "Automated Deduction",
pages = "217--221",
publisher = "Springer",
year = "1999",
}
@InProceedings{matita,
title = "{Crafting a Proof Assistant}",
author = "A. Asperti and C. Sacerdoti Coen and E. Tassi and S. Zacchiroli",
publisher = "Springer",
year = "2006",
booktitle = "TYPES",
editor = "T. Altenkirch and C. McBride",
pages = "18--32",
}
@Article{matita_refiner,
title = "{A Bi-Directional Refinement Algorithm for the Calculus of (Co)Inductive Constructions}",
author = "A. Asperti and W. Ricciotti and C. Sacerdoti Coen and E. Tassi",
journal = "Logical Methods in Computer Science",
year = "2012",
number = "1",
volume = "8",
}
@InProceedings{matita_hints,
title = "Hints in Unification",
author = "A. Asperti and W. Ricciotti and C. Sacerdoti Coen and E. Tassi",
booktitle = "Theorem Proving in Higher Order Logics",
publisher = "Springer",
year = "2009",
editor = "S. Berghofer and T. Nipkow and C. Urban and M. Wenzel",
pages = "84--98",
}
@Article{pientka_reconstruction,
title = "{An insider's look at {LF} type reconstruction: everything you (n)ever wanted to know}",
author = "B. Pientka",
journal = "J. Funct. Program",
year = "2013",
number = "1",
volume = "23",
pages = "1--37",
}
@InProceedings{luther_reconstruction,
title = "{More On Implicit Syntax}",
author = "M. Luther",
booktitle = "Automated Reasoning",