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