@article(Asperti-et-al:2007,
 author       = "Andrea Asperti and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli",
 year         = "2007",
 title        = "User Interaction with the {Matita} Proof Assistant",
 journal      = "Journal of Automated Reasoning",
 volume       = "39",
 number       = "2",
 doi          = "10.1007/s10817-007-9070-5",
)
@inproceedings(Aspinall:2000,
 author       = "David Aspinall",
 year         = "2000",
 title        = "{Proof General}: A Generic Tool for Proof Development",
 editor       = "Susanne Graf and Michael Schwartzbach",
 booktitle    = "European Joint Conferences on Theory and Practice of Software (ETAPS)",
 series       = "LNCS",
 volume       = "1785",
 publisher    = "Springer",
 doi          = "10.1007/3-540-46419-0\_3",
)
@inproceedings(Aspinall-et-al:2007,
 author       = "David Aspinall and Christoph L\"uth and Daniel Winterstein",
 year         = "2007",
 title        = "A Framework for Interactive Proof",
 editor       = "M. Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger",
 booktitle    = "Towards Mechanized Mathematical Assistants (CALCULEMUS and MKM 2007)",
 series       = "LNAI",
 volume       = "4573",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-73086-6\_15",
)
@article(Bertot-Thery:1998,
 author       = "Yves Bertot and Laurent Th\'ery",
 year         = "1998",
 title        = "A generic approach to building user interfaces for theorem provers",
 journal      = "Journal of Symbolic Computation",
 volume       = "25",
 number       = "7",
 doi          = "10.1006/jsco.1997.0171",
)
@inproceedings(Chaieb-Wenzel:2007,
 author       = "Amine Chaieb and Makarius Wenzel",
 year         = "2007",
 title        = "Context aware Calculation and Deduction --- Ring Equalities via {Gr\"obner Bases} in {Isabelle}",
 editor       = "Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger",
 booktitle    = "Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)",
 series       = "LNAI",
 volume       = "4573",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-73086-6\_3",
)
@article(PROSPER:2003,
 author       = "Louise A. Dennis and Graham Collins and Michael Norrish and Richard J. Boulton and Konrad Slind and Thomas F. Melham",
 year         = "2003",
 title        = "The {PROSPER} toolkit",
 journal      = "International Journal on Software Tools for Technology Transfer (STTT)",
 volume       = "4",
 number       = "2",
 pages        = "189--210",
 doi          = "10.1007/s100090200076",
)
@book(Gordon-Milner-Wadsworth:1979,
 author       = "M. J. C. Gordon and R. Milner and C. P. Wadsworth",
 year         = "1979",
 title        = "Edinburgh {LCF}: A Mechanized Logic of Computation",
 series       = "LNCS",
 volume       = "78",
 publisher    = "Springer",
 doi          = "10.1007/3-540-09724-4",
)
@inproceedings(Haftmann-Wenzel:2006:classes,
 author       = "Florian Haftmann and Makarius Wenzel",
 year         = "2007",
 title        = "Constructive Type Classes in {Isabelle}",
 editor       = "T. Altenkirch and C. McBride",
 booktitle    = "Types for Proofs and Programs, TYPES 2006",
 series       = "LNCS",
 volume       = "4502",
 publisher    = "Springer",
 doi          = "10.1007/978-3-540-74464-1\_11",
)
@inproceedings(Haftmann-Wenzel:2009,
 author       = "Florian Haftmann and Makarius Wenzel",
 year         = "2009",
 title        = "Local theory specifications in {Isabelle/Isar}",
 editor       = "Stefano Berardi and Ferruccio Damiani and Ugo de Liguoro",
 booktitle    = "Types for Proofs and Programs, TYPES 2008",
 series       = "LNCS",
 volume       = "5497",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-03359-9\_11",
)
@inproceedings(Haller-Odersky:2006,
 author       = "P. Haller and M. Odersky",
 year         = "2006",
 title        = "Event-Based Programming without Inversion of Control",
 booktitle    = "Joint Modular Languages Conference",
 series       = "Springer LNCS",
 doi          = "10.1007/11860990\_2",
)
@article(hendriks-adn10,
 author       = "Maxim Hendriks and Cezary Kaliszyk and Femke van Raamsdonk and Freek Wiedijk",
 year         = "2010",
 title        = "Teaching logic using a state-of-the-art proof assistant",
 journal      = "Acta Didactica Napocensia",
 volume       = "3",
 number       = "2",
 pages        = "35--48",
)
@inproceedings(Kaliszyk:2006,
 author       = "Cezary Kaliszyk",
 year         = "2007",
 title        = "Web interfaces for proof assistants",
 editor       = "S. Autexier and C. Benzm\"uller",
 booktitle    = "User Interfaces for Theorem Provers (UITP 2006)",
 series       = "ENTCS",
 volume       = "174(2)",
 publisher    = "Elsevier",
 doi          = "10.1016/j.entcs.2006.09.021",
)
@inproceedings(Matthews-Wenzel:2010,
 author       = "David C. J. Matthews and Makarius Wenzel",
 year         = "2010",
 title        = "Efficient Parallel Programming in {Poly/ML} and {Isabelle/ML}",
 booktitle    = "ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010), co-located with POPL",
 publisher    = "ACM Press",
 doi          = "10.1145/1708046.1708058",
)
@techreport(Scala:2004,
 author       = "M. Odersky",
 year         = "2004",
 title        = "An Overview of the {Scala} Programming Language",
 type         = "Technical Report",
 number       = "IC/2004/64",
 institution  = "EPF Lausanne",
)
@article(Oppen:1980,
 author       = "D. C. Oppen",
 year         = "1980",
 title        = "Pretty Printing",
 journal      = "ACM Transactions on Programming Languages and Systems",
 volume       = "2",
 number       = "4",
 doi          = "10.1145/357114.357115",
)
@incollection(paulson700,
 author       = "Lawrence C. Paulson",
 year         = "1990",
 title        = "{Isabelle}: The Next 700 Theorem Provers",
 editor       = "P. Odifreddi",
 booktitle    = "Logic and Computer Science",
 publisher    = "Academic Press",
 pages        = "361--386",
 url          = "http://arxiv.org/abs/cs.LO/9301106",
)
@inproceedings(Pham-Bertot:2010,
 author       = "Tuan Minh Pham and Yves Bertot",
 year         = "2010",
 title        = "A combination of a dynamic geometry software with a proof assistant for interactive formal proofs",
 editor       = "C. Sacerdoti Coen and D. Aspinall",
 booktitle    = "User Interfaces for Theorem Provers (UITP 2010)",
 series       = "ENTCS",
 note         = "FLOC 2010 Satellite Workshop",
)
@inproceedings(mathwiki:2010,
 author       = "J. Urban and J. Alama and P. Rudnicki and H. Geuvers",
 year         = "2010",
 title        = "A {Wiki} for {Mizar}: Motivation, Considerations, and Initial Prototype",
 booktitle    = "Conference on Intelligent Computer Mathematics (CICM 2010)",
 series       = "LNCS",
 volume       = "6167",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-14128-7\_38",
)
@inproceedings(Wagner-et-al:2006,
 author       = "Marc Wagner and S. Autexier and C. Benzm\"uller",
 year         = "2007",
 title        = "{PLAT\relax $\Omega \relax \GenericError { }{LaTeX Error: Bad math environment delimiter}{See the LaTeX manual or LaTeX Companion for explanation.}{Your command was ignored.\MessageBreak Type I <command> <return> to replace it with another command,\MessageBreak or <return> to continue without it.}}: A Mediator between Text-Editors and Proof Assistance Systems",
 editor       = "S. Autexier and C. Benzm\"uller",
 booktitle    = "User Interfaces for Theorem Provers (UITP 2006)",
 series       = "ENTCS",
 volume       = "174(2)",
 publisher    = "Elsevier",
)
@inproceedings(Wenzel:2011:CICM,
 author       = "M. Wenzel",
 year         = "2011",
 title        = "Isabelle as Document-oriented Proof Assistant",
 booktitle    = "Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011)",
 series       = "LNAI",
 volume       = "6824",
 publisher    = "Springer",
 doi          = "10.1007/978-3-642-22673-1\_17",
 note         = "\url {http://www4.in.tum.de/~wenzelm/papers/isabelle-doc.pdf}",
)
@inproceedings(Wenzel-Paulson-Nipkow:2008,
 author       = "M. Wenzel and L.C. Paulson and T. Nipkow",
 year         = "2008",
 title        = "The {Isabelle} Framework",
 booktitle    = "Theorem Proving in Higher Order Logics (TPHOLs 2008)",
 series       = "LNCS",
 publisher    = "Springer",
 url          = "http://www4.in.tum.de/~wenzelm/papers/isabelle-overview.pdf",
 note         = "Invited paper",
)
@manual(isabelle-implementation,
 author       = "Makarius Wenzel",
 title        = "The {Isabelle/Isar} Implementation",
 note         = "\url {http://isabelle.in.tum.de/doc/implementation.pdf}",
)
@manual(isabelle-isar-ref,
 author       = "Makarius Wenzel",
 title        = "The {Isabelle/Isar} Reference Manual",
 note         = "\url {http://isabelle.in.tum.de/doc/isar-ref.pdf}",
)
@inproceedings(Wenzel:2009,
 author       = "Makarius Wenzel",
 year         = "2009",
 title        = "Parallel Proof Checking in {Isabelle/Isar}",
 editor       = "G. Dos Reis and L. Th\'ery",
 booktitle    = "ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)",
 publisher    = "ACM Digital library",
)
@inproceedings(Wenzel:2010,
 author       = "Makarius Wenzel",
 year         = "2010",
 title        = "Asynchronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}",
 editor       = "C. Sacerdoti Coen and D. Aspinall",
 booktitle    = "User Interfaces for Theorem Provers (UITP 2010)",
 series       = "ENTCS",
 note         = "FLOC 2010 Satellite Workshop",
)
@inproceedings(Wenzel-Chaieb:2007b,
 author       = "Makarius Wenzel and Amine Chaieb",
 year         = "2007",
 title        = "{SML} with antiquotations embedded into {Isabelle/Isar}",
 editor       = "Jacques Carette and Freek Wiedijk",
 booktitle    = "Workshop on Programming Languages for Mechanized Mathematics (PLMMS 2007). Hagenberg, Austria",
)
@inproceedings(Wenzel:1999,
 author       = "Markus Wenzel",
 year         = "1999",
 title        = "{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents",
 editor       = "Y. Bertot and G. Dowek and A. Hirschowitz and C. Paulin and L. Thery",
 booktitle    = "Theorem Proving in Higher Order Logics (TPHOLs 1999)",
 series       = "LNCS",
 volume       = "1690",
 publisher    = "Springer",
 doi          = "10.1007/3-540-48256-3\_12",
)
@book(Wiedijk:2006,
 editor       = "Freek Wiedijk",
 year         = "2006",
 title        = "The Seventeen Provers of the World",
 series       = "LNAI",
 volume       = "3600",
 publisher    = "Springer",
)