2008 |
16 | EE | Stefan Berghofer,
Makarius Wenzel:
Logic-Free Reasoning in Isabelle/Isar.
AISC/MKM/Calculemus 2008: 355-369 |
15 | EE | Makarius Wenzel,
Lawrence C. Paulson,
Tobias Nipkow:
The Isabelle Framework.
TPHOLs 2008: 33-38 |
2007 |
14 | EE | Amine Chaieb,
Makarius Wenzel:
Context Aware Calculation and Deduction.
Calculemus/MKM 2007: 27-39 |
13 | EE | Makarius Wenzel,
Burkhart Wolff:
Building Formal Method Tools in the Isabelle/Isar Framework.
TPHOLs 2007: 352-367 |
2006 |
12 | EE | Makarius Wenzel:
Structured Induction Proofs in Isabelle/Isar.
MKM 2006: 17-30 |
11 | EE | Florian Haftmann,
Makarius Wenzel:
Constructive Type Classes in Isabelle.
TYPES 2006: 160-174 |
10 | EE | Markus Wenzel,
Lawrence C. Paulson:
Isabelle/Isar.
The Seventeen Provers of the World 2006: 41-49 |
2002 |
9 | | Tobias Nipkow,
Lawrence C. Paulson,
Markus Wenzel:
Isabelle/HOL - A Proof Assistant for Higher-Order Logic
Springer 2002 |
8 | | Markus Wenzel,
Freek Wiedijk:
A Comparison of Mizar and Isar.
J. Autom. Reasoning 29(3-4): 389-411 (2002) |
2001 |
7 | EE | Gertrud Bauer,
Markus Wenzel:
Calculational Reasoning Revisited (An Isabelle/Isar Experience).
TPHOLs 2001: 75-90 |
1999 |
6 | EE | Florian Kammüller,
Markus Wenzel,
Lawrence C. Paulson:
Locales - A Sectioning Concept for Isabelle.
TPHOLs 1999: 149-166 |
5 | EE | Markus Wenzel:
Isar - A Generic Interpretative Approach to Readable Formal Proof Documents.
TPHOLs 1999: 167-184 |
4 | EE | Stefan Berghofer,
Markus Wenzel:
Inductive Datatypes in HOL - Lessons Learned in Formal-Logic Engineering.
TPHOLs 1999: 19-36 |
3 | EE | Gertrud Bauer,
Markus Wenzel:
Computer-Assisted Mathematics at Work (The Hahn-Banach Theorem in Isabelle/Isar).
TYPES 1999: 61-76 |
1998 |
2 | | Wolfgang Naraschewski,
Markus Wenzel:
Object-Oriented Verification Based on Record Subtyping in Higher-Order Logic.
TPHOLs 1998: 349-366 |
1997 |
1 | | Markus Wenzel:
Type Classes and Overloading in Higher-Order Logic.
TPHOLs 1997: 307-322 |