[1]
Makarius Wenzel. Further scaling of Isabelle technology. In Isabelle Workshop 2018 (Oxford, UK), 2018.
[2]
Makarius Wenzel. Isabelle/PIDE after 10 years of development. In User Interfaces for Theorem Provers (UITP 2018), 2018.
[3]
Makarius Wenzel. Isabelle/jEdit as IDE for domain-specific formal languages and informal text documents. In Paolo Masci, Rosemary Monahan, and Virgile Prevosto, editors, F-IDE Workshop 2018 (Oxford, UK). To appear in EPTCS, 2018.
[4]
Makarius Wenzel. Scaling Isabelle proof document processing. Report for Mu Operator GmbH, Frankfurt am Main, December 2017.
[5]
Makarius Wenzel. The Isar proof language in 2016. In Isabelle Workshop 2016 (Nancy, France), 2016.
[6]
Daniel Matichuk, Toby C. Murray, and Makarius Wenzel. Eisbach: A proof method language for Isabelle. Journal of Automated Reasoning, 56(3), 2016.
[7]
Makarius Wenzel. Interactive theorem proving — from the perspective of Isabelle/Isar. In Bruno Woltzenlogel Paleo and David Delahaye, editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic. College Publications, UK, 2015.
[8]
Makarius Wenzel. Transitive closure according to Roy-Floyd-Warshall. Archive of Formal Proofs, 2014.
[9]
Daniel Matichuk, Makarius Wenzel, and Toby Murray. An Isabelle proof method language. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Vienna, Austria, volume 8558 of Lecture Notes in Computer Science. Springer, 2014.
[10]
Makarius Wenzel. Asynchronous user interaction and tool integration in Isabelle/PIDE. In Gerwin Klein and Ruben Gamboa, editors, Interactive Theorem Proving - 5th International Conference, ITP 2014, Vienna, Austria, volume 8558 of Lecture Notes in Computer Science. Springer, 2014.
[11]
Makarius Wenzel. System description: Isabelle/jEdit in 2014. In Christoph Benzmüller and Bruno Woltzenlogel Paleo, editors, User Interfaces for Theorem Provers (UITP 2014), EPTCS, July 2014.
[12]
Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel, and Burkhart Wolff. The Circus testing theory revisited in Isabelle/HOL. In Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods, ICFEM 2013, Queenstown, New Zealand, October 29 - November 1, 2013, Proceedings, 2013.
[13]
Makarius Wenzel. Shared-memory multiprocessing for interactive theorem proving. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving - 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings, volume 7998 of Lecture Notes in Computer Science. Springer, 2013.
[14]
Christoph Lange, Marco B. Caminati, Manfred Kerber, Till Mossakowski, Colin Rowat, Makarius Wenzel, and Wolfgang Windsteiger. A qualitative comparison of the suitability of four theorem provers for basic auction theory. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, Intelligent Computer Mathematics — MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings, volume 7961 of Lecture Notes in Computer Science, pages 200–215. Springer, 2013.
[15]
Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel, and Burkhart Wolff. Pervasive parallelism in highly-trustable interactive theorem proving systems. In Jacques Carette, David Aspinall, Christoph Lange, Petr Sojka, and Wolfgang Windsteiger, editors, Intelligent Computer Mathematics — MKM, Calculemus, DML, and Systems and Projects 2013, Held as Part of CICM 2013, Bath, UK, July 8-12, 2013. Proceedings, volume 7961 of Lecture Notes in Computer Science. Springer, 2013.
[16]
Makarius Wenzel. PIDE as front-end technology for Coq. 2013.
[17]
Makarius Wenzel. READ-EVAL-PRINT in parallel and asynchronous proof-checking. In Cezary Kaliszyk and Christoph Lüth, editors, User Interfaces for Theorem Provers (UITP 2012), volume 118 of EPTCS, 2013.
[18]
Makarius Wenzel. Isabelle/jEdit — a Prover IDE within the PIDE framework. In J. Jeuring and others, editors, Conference on Intelligent Computer Mathematics (CICM 2012), volume 7362 of LNAI. Springer, 2012.
[19]
Makarius Wenzel. READ-EVAL-PRINT in parallel and asynchronous proof-checking. In Workshop on User Interfaces for Theorem Provers (UITP 2012), July 2012.
[20]
Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, editors. Intelligent Computer Mathematics — 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings, volume 7362 of LNCS. Springer, 2012.
[21]
M. Wenzel. Isabelle as document-oriented proof assistant. In J. H. Davenport, W. M. Farmer, F. Rabe, and J. Urban, editors, Conference on Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011), volume 6824 of LNAI. Springer, 2011.
[22]
Makarius Wenzel and Burkhart Wolff. Isabelle/PIDE as platform for educational tools. In Pedro Quaresma and Ralph-Johan Back, editors, Proceedings First Workshop on CTP Components for Educational Software (THedu'11), volume 79 of EPTCS, 2011.
[23]
Jacques Carette, Makarius Wenzel, and Freek Wiedijk. Special issue on Programming Languages for Mechanized Mathematics Systems. J. Autom. Reasoning, 44(1-2), 2010.
[24]
D. Matthews and M. Wenzel. Efficient parallel programming in Poly/ML and Isabelle/ML. In ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010), 2010.
[25]
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, ENTCS. Elsevier, July 2010.
[26]
Norbert Schirmer and Makarius Wenzel. State spaces — the locale way. In Ralf Huuck, Gerwin Klein, and Bastian Schlich, editors, Systems Software Verification (SSV 2009), ENTCS. Elsevier, 2009.
[27]
Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel, editors. Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings, volume 5674 of Lecture Notes in Computer Science. Springer, 2009.
[28]
M. Wenzel. Parallel proof checking in Isabelle/Isar. In G. Dos Reis and L. Théry, editors, ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). ACM Digital Library, 2009.
[29]
Florian Haftmann and Makarius Wenzel. Local theory specifications in Isabelle/Isar. In Stefano Berardi, Ferruccio Damiani, and Ugo de Liguoro, editors, Types for Proofs and Programs, TYPES 2008, volume 5497 of Lecture Notes in Computer Science. Springer, 2009.
[30]
Stefan Berghofer and Makarius Wenzel. Logic-free reasoning in Isabelle/Isar. In Intelligent Computer Mathematics — Mathematical Knowledge Management (MKM 2008), volume 5144 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2008.
[31]
M. Wenzel, L.C. Paulson, and T. Nipkow. The Isabelle framework. In Theorem Proving in Higher Order Logics (TPHOLs 2008), Lecture Notes in Computer Science. Springer-Verlag, 2008.
[32]
Amine Chaieb and Makarius Wenzel. Context aware calculation and deduction — ring equalities via Gröbner Bases in Isabelle. In Manuel Kauers, Manfred Kerber, Robert Miner, and Wolfgang Windsteiger, editors, Towards Mechanized Mathematical Assistants (CALCULEMUS 2007), volume 4573 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2007.
[33]
Makarius Wenzel and Amine Chaieb. SML with antiquotations embedded into Isabelle/Isar. In Jacques Carette and Freek Wiedijk, editors, Workshop on Programming Languages for Mechanized Mathematics (PLMMS 2007). Hagenberg, Austria, June 2007.
[34]
M. Wenzel and B. Wolff. Building formal method tools in the Isabelle/Isar framework. In K. Schneider and J. Brandt, editors, Theorem Proving in Higher Order Logics (TPHOLs 2007), volume 4732 of Lecture Notes in Computer Science. Springer-Verlag, 2007.
[35]
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, volume 10(23) of Studies in Logic, Grammar, and Rhetoric. University of Białystok, 2007.
[36]
Makarius Wenzel. Structured induction proofs in Isabelle/Isar. In J. Borwein and W. Farmer, editors, Mathematical Knowledge Management (MKM 2006), volume 4108 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2006.
[37]
Florian Haftmann and Makarius Wenzel. Constructive type classes in Isabelle. In T. Altenkirch and C. McBride, editors, Types for Proofs and Programs (TYPES 2006), volume 4502 of Lecture Notes in Computer Science. Springer-Verlag, 2007.
[38]
Markus Wenzel and Lawrence C. Paulson. Isabelle/Isar. In F. Wiedijk, editor, The Seventeen Provers of the World, volume 3600 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2006.
[39]
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL — A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer-Verlag, 2002.
[40]
Markus Wenzel. Isabelle/Isar — a versatile environment for human-readable formal proof documents. PhD thesis, Institut für Informatik, TU München, 2002.
[41]
Freek Wiedijk and Markus Wenzel. A comparison of the mathematical proof languages Mizar and Isar. Journal of Automated Reasoning, 29(3-4), 2002.
[42]
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), volume 2152 of Lecture Notes in Computer Science. Springer-Verlag, 2001.
[43]
Gertrud Bauer and Markus Wenzel. Computer-assisted mathematics at work — the Hahn-Banach Theorem in Isabelle/Isar. In Thierry Coquand, Peter Dybjer, Bengt Nordström, and Jan Smith, editors, Types for Proofs and Programs (TYPES 1999), volume 1956 of Lecture Notes in Computer Science. Springer-Verlag, 2000.
[44]
Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL — lessons learned in Formal-Logic Engineering. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics (TPHOLs 1999), volume 1690 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
[45]
Florian Kammüller, Markus Wenzel, and Lawrence C. Paulson. Locales: A sectioning concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics (TPHOLs 1999), volume 1690 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
[46]
Markus Wenzel. Isar — a generic interpretative approach to readable formal proof documents. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics (TPHOLs 1999), volume 1690 of Lecture Notes in Computer Science. Springer-Verlag, 1999.
[47]
Wolfgang Naraschewski and Markus Wenzel. Object-oriented verification based on record subtyping in Higher-Order Logic. In Jim Grundy and Malcom Newey, editors, Theorem Proving in Higher Order Logics (TPHOLs 1998), volume 1479 of Lecture Notes in Computer Science. Springer-Verlag, 1998.
[48]
M. Wenzel. Type classes and overloading in higher-order logic. In Elsa L. Gunter and Amy Felty, editors, Theorem Proving in Higher Order Logics (TPHOLs 1997), volume 1275 of Lecture Notes in Computer Science. Springer-Verlag, 1997.