References

1. 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.
2. 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.
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.
4. 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.
5. 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.
6. 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.
7. 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.
8. 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.
9. 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.
10. P. Haller & M. Odersky (2006): Event-Based Programming without Inversion of Control. In: Joint Modular Languages Conference, Springer LNCS, doi:10.1007/11860990_2.
11. 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.
12. 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.
13. 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.
14. M. Odersky (2004): An Overview of the Scala Programming Language. Technical Report IC/2004/64. EPF Lausanne.
15. D. C. Oppen (1980): Pretty Printing. ACM Transactions on Programming Languages and Systems 2(4), doi:10.1145/357114.357115.
16. 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.
17. 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.
18. 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.
19. 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.
20. 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.
21. M. Wenzel, L.C. Paulson & T. Nipkow (2008): The Isabelle Framework. In: Theorem Proving in Higher Order Logics (TPHOLs 2008), LNCS. Springer. Available at http://www4.in.tum.de/~wenzelm/papers/isabelle-overview.pdf. Invited paper.
22. Makarius Wenzel: The Isabelle/Isar Implementation. http://isabelle.in.tum.de/doc/implementation.pdf.
23. Makarius Wenzel: The Isabelle/Isar Reference Manual. http://isabelle.in.tum.de/doc/isar-ref.pdf.
24. 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.
25. 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.
26. 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.
27. 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.
28. Freek Wiedijk (2006): The Seventeen Provers of the World. LNAI 3600. Springer.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org