Current Work

• Makarius Wenzel. READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking. Submitted. May 2012.
• Makarius Wenzel. Shared-Memory Multiprocessing for Interactive Theorem Proving. Unpublished, February 2011.

Publications

• Makarius Wenzel. Isabelle/jEdit — a Prover IDE within the PIDE framework. In J. Jeuring et-al, editors, Conference on Intelligent Computer Mathematics (CICM 2012). Springer LNAI 7362, 2012.
• Makarius Wenzel and Burkhart Wolff. Isabelle/PIDE as Platform for Educational Tools. Workshop on Computer Theorem Proving Components for Educational Software (THedu 2011). EPTCS volume 79, 2012.
• Makarius Wenzel. Isabelle as Document-oriented Proof Assistant. In J. H. Davenport, W. M. Farmer, F. Rabe, J. Urban, editors, Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011). Springer LNAI 6824, 2011.
• Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors, User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
• David C. J. Matthews and Makarius Wenzel. Efficient Parallel Programming in Poly/ML and Isabelle/ML. Proceedings of the ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010), co-located with POPL, Madrid, Spain, January 2010. To appear.
• Makarius Wenzel. Parallel Proof Checking in Isabelle/Isar. In G. Dos Reis and L. Théry, editors. The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS). Munich, August 2009. ACM Digital library.
• Norbert Schirmer and Makarius Wenzel. State Spaces --- The Locale Way, In Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, 4th International Workshop on Systems Software Verification (SSV 2009). ENTCS 2009.
• Florian Haftmann and Makarius Wenzel. Local theory specifications in Isabelle/Isar, In S. Berardi, F. Damiani and U. de Liguoro, editors, Types for Proofs and Programs, TYPES 2008. LNCS 5497, © Springer, 2009.
• Makarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle Framework. In O. Ait-Mohamed, editor, Theorem Proving in Higher Order Logics, TPHOLs 2008, invited paper, LNCS 5170, © Springer, 2008.
• Stefan Berghofer and Makarius Wenzel. Logic-free reasoning in Isabelle/Isar, Conference on Mathematical Knowledge Management, MKM 2008, LNAI, © Springer, 2008.
• Makarius Wenzel and Burkhart Wolff. Building Formal Method Tools in the Isabelle/Isar Framework. In K. Schneider and J. Brandth, editors, Theorem Proving in Higher Order Logics, TPHOLs 2007, LNCS 4732, © Springer, 2007.
• Makarius Wenzel and Amine Chaieb. SML with antiquotations embedded into Isabelle/Isar. In J. Carette and F. Wiedijk, editors, Programming Languages for Mechanized Mathematics Workshop (CALCULEMUS 2007). RISC-Linz Report 07-10, Hagenberg, Austria, June 2007.
• Amine Chaieb and Makarius Wenzel. Context aware Calculation and Deduction --- Ring Equalities via Gröbner Bases in Isabelle. In M. Kauers, M. Kerber, R. Miner, and W. Windsteiger, editors, Towards Mechanized Mathematical Assistants (CALCULEMUS 2007 and MKM 2007). LNAI 4573, © Springer, 2007.
• Makarius Wenzel. Isabelle/Isar --- a generic framework for human-readable proof documents. In R. Matuszewski and A. Zalewska, editors, From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec, Studies in Logic, Grammar, and Rhetoric 10(23), University of Białystok, 2007.
• Florian Haftmann and Makarius Wenzel. Constructive Type Classes in Isabelle. In T. Altenkirch and C. McBride, editors, Types for Proofs and Programs, TYPES 2006. LNCS 4502, © Springer, 2007.
• Makarius Wenzel. Structured Induction Proofs in Isabelle/Isar. In J. Borwein and W. Farmer, editors, 5th International Conference on Mathematical Knowledge Management, MKM 2006, LNAI 4108, © Springer, 2006.
• Markus Wenzel and Larry Paulson. Isabelle/Isar. In Freek Wiedijk, editor, The Seventeen Provers of the World. LNCS 3600, Springer, 2006.
• Markus Wenzel and Free Wiedijk. A comparison of the mathematical proof languages Mizar and Isar. In Journal of Automated Reasoning, 29, 2002.
• Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - The Tutorial. LNCS 2283, © Springer, April 2002.
• Gertrud Bauer and Markus Wenzel. Calculational reasoning revisited - an Isabelle/Isar experience. In R. J. Boulton and P. B. Jackson, editors, Theorem Proving in Higher Order Logics, TPHOLs 2001, LNCS 2152, © Springer, 2001.
• Gertrud Bauer and Markus Wenzel. Computer-Assisted Mathematics at Work - The Hahn-Banach Theorem in Isabelle/Isar. In T. Coquand, P. Dybjer, B. Nordström, J. Smith, editors, Types for Proofs and Programs, TYPES'99. Lökeberg, Sweden. © Springer LNCS, 2000.
• Markus Wenzel. Isar - a Generic Interpretative Approach to Readable Formal Proof Documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, TPHOLs'99, LNCS 1690, © Springer, 1999. Slides available.
• Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL - lessons learned in Formal-Logic Engineering. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, TPHOLs'99, LNCS 1690, © Springer, 1999.
• Florian Kammüller and Markus Wenzel and Lawrence C. Paulson. Locales - A Sectioning Concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, TPHOLs'99, LNCS 1690, © Springer, 1999.
• Wolfgang Naraschewski and Markus Wenzel. Object-Oriented Verification based on Record Subtyping in Higher-Order Logic. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, TPHOLs'98, LNCS 1479, Springer, 1998. Extended version available as ps and pdf, slides available as ps.
• Markus Wenzel. Type Classes and Overloading in Higher-Order Logic. In Elsa L. Gunter and Amy Felty, editors, Theorem Proving in Higher Order Logics, TPHOLs'97, LNCS 1275, Springer, 1997.

PhD Thesis

• Markus Wenzel. Isabelle/Isar --- a versatile environment for human-readable formal proof documents, PhD thesis, Institut für Informatik, Technische Universität München, 2002.

Other

• Makarius Wenzel. On prover interaction and integration with Isabelle/Scala, Dagstuhl, October 2009.
• Makarius Wenzel. The languages of Isabelle: Isar, ML, and Scala, Lausanne, September 2009. Video.
• Makarius Wenzel. Interactive Proof Documents -- Theorem Provers for User Interfaces, Edinburgh, November 2008.
• Makarius Wenzel. Asynchronous processing of proof documents -- rethinking interactive theorem proving, Edinburgh, November 2007.
• Florian Kammüller and Markus Wenzel. Locales - A Sectioning Concept for Isabelle, Technical Report No. 449, University of Cambridge, Computer Laboratory, October 1998.
• Markus Wenzel and Wolfgang Naraschewski. Record subtyping based on simply typed languages. Abstract and slides available. Presented on CCL98, Jerusalem, September 1998.
• Markus Wenzel. Isabelle in 18 Slides, Nov-1998.
• Markus Wenzel. Isabelle in 4 Slides, Mar-1998.
• Markus Wenzel. Isabelle in 6 Slides, Dec-1997.
• Markus Wenzel. Isabelle in 7 Slides, Oct-1996.