Type Classes and Overloading in Higher-Order Logic. - Markus Wenzel 001 (TPHOLs, 1997)

Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic. - Wolfgang Naraschewski; Markus Wenzel 001 (TPHOLs, 1998)

Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering. - Stefan Berghofer; Markus Wenzel 001 (TPHOLs, 1999)

Locales - A Sectioning Concept for Isabelle. - Florian Kammüller; Markus Wenzel 001; Lawrence C. Paulson (TPHOLs, 1999)

Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. - Markus Wenzel 001 (TPHOLs, 1999)

Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar). - Gertrud Bauer; Markus Wenzel 001 (TYPES, 1999)

Calculational Reasoning Revisited (An Isabelle/Isar Experience). - Gertrud Bauer; Markus Wenzel 001 (TPHOLs, 2001)

Isabelle/HOL - A Proof Assistant for Higher-Order Logic - Tobias Nipkow; Lawrence C. Paulson; Markus Wenzel 001 (Springer, 2002)

A Comparison of Mizar and Isar. - Markus Wenzel 001; Freek Wiedijk (J. Autom. Reason., 2002)

Isabelle, Isar - a versatile environment for human readable formal proof documents. - Markus Wenzel 001 (2002)

Structured Induction Proofs in Isabelle/Isar. - Makarius Wenzel (MKM, 2006)

Isabelle/Isar. - Markus Wenzel 001; Lawrence C. Paulson (The Seventeen Provers of the World, 2006)

Constructive Type Classes in Isabelle. - Florian Haftmann; Makarius Wenzel (TYPES, 2006)

Context Aware Calculation and Deduction. - Amine Chaieb; Makarius Wenzel (Calculemus/MKM, 2007)

Building Formal Method Tools in the Isabelle/Isar Framework. - Makarius Wenzel; Burkhart Wolff (TPHOLs, 2007)

Logic-Free Reasoning in Isabelle/Isar. - Stefan Berghofer; Makarius Wenzel (AISC/MKM/Calculemus, 2008)

The Isabelle Framework. - Makarius Wenzel; Lawrence C. Paulson; Tobias Nipkow (TPHOLs, 2008)

Local Theory Specifications in Isabelle/Isar. - Florian Haftmann; Makarius Wenzel (TYPES, 2008)

State Spaces - The Locale Way. - Norbert Schirmer; Makarius Wenzel (SSV, 2009)

Efficient parallel programming in Poly/ML and Isabelle/ML. - David C. J. Matthews; Makarius Wenzel (DAMP, 2010)

Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. - Makarius Wenzel (UITP, 2010)

Preface. - Jacques Carette; Makarius Wenzel; Freek Wiedijk (J. Autom. Reason., 2010)

Isabelle as Document-Oriented Proof Assistant. - Makarius Wenzel (Calculemus/MKM, 2011)

Isabelle/PIDE as Platform for Educational Tools - Makarius Wenzel; Burkhart Wolff (ThEdu, 2011)

Isabelle/jEdit - A Prover IDE within the PIDE Framework. - Makarius Wenzel (AISC/MKM/Calculemus, 2012)

READ-EVAL-PRINT in Parallel and Asynchronous Proof-checking. - Makarius Wenzel (UITP, 2012)

The Circus Testing Theory Revisited in Isabelle/HOL. - Abderrahmane Feliachi; Marie-Claude Gaudel; Makarius Wenzel; Burkhart Wolff (ICFEM, 2013)

Shared-Memory Multiprocessing for Interactive Theorem Proving. - Makarius Wenzel (ITP, 2013)

A Qualitative Comparison of the Suitability of Four Theorem Provers for Basic Auction Theory. - Christoph Lange 002; Marco B. Caminati; Manfred Kerber; Till Mossakowski; Colin Rowat; Makarius Wenzel; Wolfgang Windsteiger (MKM/Calculemus/DML, 2013)

Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. - Bruno Barras; Lourdes Del Carmen González-Huesca; Hugo Herbelin; Yann Régis-Gianas; Enrico Tassi; Makarius Wenzel; Burkhart Wolff (MKM/Calculemus/DML, 2013)

PIDE as front-end technology for Coq - Makarius Wenzel (CoRR, 2013)

An Isabelle Proof Method Language. - Daniel Matichuk; Makarius Wenzel; Toby C. Murray (ITP, 2014)

Asynchronous User Interaction and Tool Integration in Isabelle/PIDE. - Makarius Wenzel (ITP, 2014)

Transitive closure according to Roy-Floyd-Warshall. - Makarius Wenzel (Arch. Formal Proofs, 2014)

System description: Isabelle/jEdit in 2014. - Makarius Wenzel (UITP, 2014)

Eisbach: A Proof Method Language for Isabelle. - Daniel Matichuk; Toby C. Murray; Makarius Wenzel (J. Autom. Reason., 2016)

Isabelle/jEdit as IDE for Domain-specific Formal Languages and Informal Text Documents. - Makarius Wenzel (F-IDE@FLoC, 2018)

Virtualization of HOL4 in Isabelle. - Fabian Immler; Jonas Rädle; Makarius Wenzel (ITP, 2019)

Relational Data Across Mathematical Libraries. - Andrea Condoluci; Michael Kohlhase; Dennis Müller 001; Florian Rabe 001; Claudio Sacerdoti Coen; Makarius Wenzel (CICM, 2019)

Interaction with Formal Mathematical Documents in Isabelle/PIDE. - Makarius Wenzel (CICM, 2019)

Isabelle technology for the Archive of Formal Proofs with application to MMT. - Makarius Wenzel (CICM Workshops, 2019)

Making Isabelle Content Accessible in Knowledge Representation Formats. - Michael Kohlhase; Florian Rabe 001; Makarius Wenzel (TYPES, 2019)

Isabelle technology for the Archive of Formal Proofs. - Makarius Wenzel (CoRR, 2019)

From LCF to Isabelle/HOL. - Lawrence C. Paulson; Tobias Nipkow; Makarius Wenzel (Formal Aspects Comput., 2019)

The Isabelle/Naproche Natural Language Proof Assistant. - Adrian De Lon; Peter Koepke; Anton Lorenzen; Adrian Marti; Marcel Schütz; Makarius Wenzel (CADE, 2021)

CICM'21 Systems Entries. - Martin Líska; Dávid Lupták; Vít Novotný; Michal Ruzicka; Boris Shminke; Petr Sojka; Michal Stefánik; Makarius Wenzel (CICM, 2021)

Designing an Inclusive and Accessible Mathematical Learning Environment Based on a Theorem Prover. - Bernhard Stöger; Klaus Miesenberger; Walther Neuper; Makarius Wenzel; Thomas Neumayr (ICCHP-AAATE (1), 2022)

Seventeen Provers Under the Hammer. - Martin Desharnais; Petar Vukmirovic; Jasmin Blanchette; Makarius Wenzel (ITP, 2022)

Towards an Accessible Mathematics Working Environment Based on Isabelle/VSCode. - Klaus Miesenberger; Walther Neuper; Bernhard Stöger; Makarius Wenzel (ThEdu@FLoC, 2022)

Distributed Parallel Build for the Isabelle Archive of Formal Proofs. - Fabian Huch; Makarius Wenzel (ITP, 2024)