Bibliography
This is a list of papers published during the project, or describing relevant previous work (before 2002).-
Maksym Bortin: An Approach to the Extension of a Theorem Prover by Advanced Structuring Mechanisms.
Dissertation, Universität Bremen. Logos-Verlag, Berlin. 2010.
[Order] [Google Books] - Maksym Bortin, Christoph Lüth:
Structured Formal Development with Quotient Types in Isabelle/HOL.
AISC2010 - 10th International Conference on Artifial Intelligence and Symbolic Computation.
Springer LNCS 6167, © Springer Verlag.
[PDF] [BibTeX]
Structured Formal Development in Isabelle. -
Maksym Bortin, Einar Broch Johnsen, Christoph Lüth:
Structured Formal Development in Isabelle.
Nordic Journal of Computing, 13: 1-- 20, 2006.
[Abstract] [PDF] [PostScript] [BibTeX] -
Einar Broch Johnsen, Christoph Lüth:
Theorem Reuse by Proof Term Transformation.
International Conference on Theorem Proving in Higher-Order Logics TPHOLs 2004.
Springer LNCS 3223, © Springer Verlag
[Abstract] [PostScript] [PDF] [BibTeX] -
Einar Broch Johnsen, Christoph Lüth:
Abstracting Refinements for Transformation.
Nordic Journal of Computing, 10: 316-- 336, 2004.
[Abstract] [PDF] [PostScript] [BibTeX] -
David Aspinall, Christoph Lüth, Daniel Winterstein:
A Framework for Interactive Proof.
Unpublished.
[PDF] [PostScript] -
David Aspinall, Christoph Lüth:
Proof General meets IsaWin --- Combining Text-Based And Graphical User Interfaces.
International Workshop on User Interfaces for Theorem Provers (UITP'03), Rome, Italy, Sept. 2003.
Electronic Notes in Theoretical Computer Science, Vol 103:C
[Abstract] [PDF] [ScienceDirect] [BibTeX] - Christoph Lüth, Burkhart Wolff:
TAS --- A Generic Window Inference System.
13th International Conference on Theorem Proving and Higher Order Logics. Portland, Oregon, August 2000.
Springer LNCS 1869, © Springer Verlag
[Abstract] [PostScript] [PDF] [BibTeX]
- Christoph Lüth, Burkhart Wolff:
More About TAS and IsaWin --- Tools for Formal Program Development.
European Joint Conferences on Theory and Practice of Software ETAPS 2000. Berlin, Germany, March 2000.
Springer LNCS 1783, © Springer Verlag
[PostScript] [BibTeX] - Christoph Lüth, Burkhart Wolff:
Functional Design and Implementation of Graphical User Interfaces for Theorem Provers.
Journal of Functional Programming, 9(2): 167- 189, March 1999.
[Abstract] [PDF] [PostScript] [BibTeX]
Nordic Journal of Computing, 13: 1-- 20, 2006.
[Abstract] [PDF] [PostScript] [BibTeX]