Publications

This page contains a list of my publications, split into journal publications, referereed conferences and workshops, unrefereed workshops, technical reports, theses and the rest.

The copies of papers provided here may be preview copies where copyright applies to the originals, but the content can be taken as authoratitive.

Journal Papers

• Holger Täubig, Udo Frese, Christoph Hertzberg, Christoph Lüth, Stefan Mohr, Elena Vorobev, Dennis Walter: Guaranteeing Functional Safety: Design for Provability and Computer-Aided Verification
  Autonomous Robots 32(3):303-- 331, April 2012. © Springer Verlag.
  [PDF (free pre-print)] [PDF (SpringerLink)] [BibTeX]
• David Aspinall, Ewen Denney, Christoph Lüth: Tactics for Hierarchical Proof
  Mathematics in Computer Science, 3:309-- 330. March 2010.
  [PDF] [BiBTeX]
• David Aspinall, Christoph Lüth (eds): Special Issue on User Interfaces in Theorem Proving
  Journal for Automated Reasoning, 39:2, 107-- 108. August 2007.
  [PDF (Preface)] [BibTeX]
• Christoph Lüth, Bernd Krieg-Brückner: Sicherheit in der Künstlichen Intelligenz.
  Künstliche Intelligenz, 1:51-- 52, 2007.
  [PDF (extern)] [PDF (lokal)] [BibTeX]
• Maksym Bortin, Einar Broch Johnsen, Christoph Lüth: Structured Formal Development in Isabelle.
  Nordic Journal of Computing, 13: 1-- 20, 2006.
  [PDF] [PostScript] [BibTeX]
• Einar Broch Johnsen, Christoph Lüth: Abstracting Refinements for Transformation.
  Nordic Journal of Computing, 10: 316-- 336, 2004.
  [PDF] [PostScript] [BibTeX]
• Neil Ghani, Christoph Lüth: Rewriting via Coinserters.
  Nordic Journal of Computing, 10:290-- 312, 2004.
  [PDF] [PostScript] [BibTeX] [Sources]
• Christoph Lüth:
  Haskell in Space. An interactive game as a functional programming exercise.
  Eductional Pearl, Journal of Functional Programming, 13(6): 1077- 1085, November 2003.
  [PDF] [PostScript] [BibTeX] [Sources]
• Neil Ghani, Christoph Lüth, Federico deMarchi: Monads of Coalgebras: Rational Terms and Term Graphs.
  Mathematical Structures in Computer Science, 15(3):433- 451, 2005.
  [PDF] [PostScript] [BibTeX]
• Federico deMarchi, Neil Ghani, Christoph Lüth: Solving Algebraic Equations using Coalgebra.
  Theoretical Informatics and Applications, 37:301-- 314, 2003.
  [PDF] [PostScript] [BibTeX]
• Neil Ghani, Christoph Lüth, Federico de Marchi, John Power:
  Dualizing Initial Algebras.
  Mathematical Structures in Computer Science, 13(2):349- 370, 2003.
  [PDF] [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.
  [PDF] [PostScript] [BibTeX]

Refereed Conferences and Workshops

• David Aspinall, Ewen Denney, Christoph Lüth: Querying Proofs.
  Accepted at LPAR 18, The 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning .
  To appear in Lecture Notes in Computer Science, © Springer Verlag.
  [PDF] [BibTeX]
• Serge Autexier, Christoph Lüth: Adding Change Impact Analysis to the Formal Verification of C Programs
  iFM 2010: Integrated Formal Methods - 8th International Conference.
  Springer LNCS 6396, © Springer Verlag.
  [PDF] [BibTeX]
• Dennis Walter, Holger Täubig, Christoph Lüth: Experiences in Applying Verification in Robotics.
  SafeComp2010 - 29th International Conference on Computer Safety, Reliability and Security.
  Springer LNCS 6351, © Springer Verlag.
  [PDF] [BibTeX]
• 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]
• Christoph Lüth: User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?
  Ninth International Workshop on Automated Verification of Critical Systems AVOCS'09 (Invited Talk).
  [PDF] [BibTeX]
• Christoph Lüth, Dennis Walter: Certifiable specification and verification of C programs.
  FM 2009 --- 16th International Symposium on Formal Methods.
  Springer LNCS 5850, © Springer Verlag.
  [PDF] [BibTeX]
• David Aspinall, Serge Autexier, Christoph Lüth, Marc Wagner: Towards Merging PlatΩ and PGIP.
  8th International Workshop on User Interfaces for Theorem Provers (UITP 2008), Electronic Notes in Theoretical Computer Science, Vol. 226, 3 January 2009.
  [DOI] [BibTeX]
• David Aspinall, Ewen Denney, Christoph Lüth:
  A Tactic Language for Hiproofs.
  Mathematical Knowledge Management MKM 2008, Conferences on Intelligent Computer Mathematics (CICM), Birmingham, July 2008.
  Springer LNAI 5144, © Springer Verlag
  [PDF] [BibTeX]
• Christoph Lüth, Udo Frese, Holger Täubig, Dennis Walter, Daniel Hausmann: SAMS --- Sicherungskomponente für Autonome Mobile Serviceroboter.
  ROBOTIK 2008: Leistungsstand- Anwendungen- Visionen- Trends. VDI-Bericht 2012, VDI Verlag, Düsseldorf.
  [PDF] [BiBTeX]
• Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig and Dennis Walter: The Importance of Being Formal
  International Workshop on the Certification of Safety-Critical Software Controlled Systems SafeCert'08 at ETAPS'08.
  Electronic Notes in Theoretical Computer Science, Vol. 238 (2009), p. 57-- 70.
  [PDF] [BibTeX]
• Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig, Dennis Walter: Zertifizierung einer Sicherungskomponente mittels durchgängig formaler Modellierung
  Workshop SoftZert'08, Feb. 2008, Munich. Lecture Notes in Informatics P-122, S. 335-- 338. Gesellschaft für Informatik (GI).
  [PDF] [BibTeX]
• David Aspinall, Christoph Lüth, Daniel Winterstein: A Framework for Interactive Proof.
  Mathematical Knowledge Management MKM 2007, Linz, July 2007.
  Springer LNAI 4573, © Springer Verlag
  [PostScript] [PDF] [BibTeX]
• David Aspinall, Christoph Lüth, Daniel Winterstein and Ahsan Fayyaz: Proof General in Eclipse.
  Eclipse Technology eXchange ETX'06. Portland OR, USA, Oct. 2006.
  ACM Press (Digital library link)
  [PDF] [BibTeX]
• David Aspinall, Christoph Lüth, Burkhart Wolff: Assisted Proof Document Authoring.
  Mathematical Knowledge Management MKM 2005, Bremen, August 2005.
  Springer LNAI 3863, © Springer Verlag
  [PostScript] [PDF] [BibTeX]
• Micheal Abbot, Neil Ghani, Christoph Lüth: Abstract Modularity.
  Rewriting Techniques and Applications RTA'05, Nara, Japan, April 2005.
  Springer LNCS 3467, © Springer Verlag
  [PostScript] [PDF] [BibTeX]
• Christoph Lüth, Markus Roggenbach, Lutz Schröoder: CCC - The CASL Consistency Checker.
  Recent Trends in Algebraic Development Techniques, 16th International Workshop (WADT 2004), Barcelona, April 2004.
  Springer LNCS 3423, © Springer Verlag
  [PostScript] [PDF] [BibTeX]
• Lutz Schröder, Till Mossakowski, Christoph Lüth: Type class polymorphism in an institutional framework.
  Recent Trends in Algebraic Development Techniques, 16th International Workshop (WADT 2004), Barcelona, April 2004.
  Springer LNCS 3423 , © Springer Verlag
  [PostScript] [PDF] [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
  [PostScript] [PDF] [BibTeX] [Sources]
• 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
  [PDF] [ScienceDirect] [BibTeX]
• Bernd Krieg-Brückner, Dieter Hutter, Arne Lindow, Christoph Lüth, Achim Mahnke, Erica Melis, Philipp Meier, Arnd Poetzsch-Heffter, Markus Roggenbach, George Russell, Jan-Georg Smaus and Martin Wirsing: MultiMedia Instruction in Safe and Secure Systems.
  Invited technical paper. Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002, Frauenchiemsee, Germany, September 24-27.
  Springer LNCS 2755, © Springer Verlag
  [PDF] [BibTeX]
• Christoph Lüth, Neil Ghani:
  Composing Monads Using Coproducts.
  Seventh ACM SIGPLAN International Conference on Functional Programmin ICFP'02. Pittsburgh, Pa, USA, October 2002. ACM Press.
  [PostScript] [PDF] [BibTeX] [Sources]
• Neil Ghani, Christoph Lüth and Federico de Marchi: Coalgebraic Approaches to Algebraic Terms.
  Workshop on Fixed Points in Computer Science FICS'02. Copenhagen, Denmark, July 2002.
  BRICS Notes Series NS-02-2
  [PostScript] [BibTeX]
• Christoph Lüth, Neil Ghani:
  Monads and Modularity.
  4th International Workshop on Frontiers of Combining Systems FroCoS 2002. Santa Margherita Ligure, Italy, April 2002.
  Springer LNAI 2309, © Springer Verlag
  [PostScript] [PDF] [BibTeX]
• Neil Ghani, Christoph Lüth and Federico de Marchi: Coalgebraic Monads.
  5th International Workshop on Coalgebraic Methods in Computer Science, Grenoble, April 2002.
  Eletronic Notes in Theoretical Computer Science Vol. 65.1.
  [PostScript] [BibTeX]
• Neil Ghani, Christoph Lüth, Federico de Marchi, J. Power: Algebras, Coalgebras, Monads and Comonads.
  4th International Workshop on Coalgebraic Methods in Computer Science , Genoa, April 2001.
  Eletronic Notes in Theoretical Computer Science, Vol 44.1.
  [PostScript] [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
  [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, Haykal Tej, Kolyang, Bernd Krieg-Brückner: TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving.
  European Joint Conference on Theory and Practice of Software ETAPS'99. Amsterdam, The Netherlands, March 1999.
  Springer LNCS 1577, © Springer Verlag
  [PostScript] [BibTeX]
• Christoph Lüth, Einar W. Karlsen, Kolyang, Stefan Westmeier, Burkhart Wolff: HOL-Z in the UniForM-Workbench -- a Case Study in Tool Integration for Z.
  11. International Conference of Z Users ZUM'98. Berlin, Germany, September 1997.
  Springer LNCS 1493, © Springer Verlag
  [PostScript] [BibTeX]
• Christoph Lüth, Einar W. Karlsen, Kolyang, Stefan Westmeier, Burkhart Wolff: Tool Integration in the UniForM Workbench.
  Tool Support for System Specification, Development, and Verification. International Workshop, Malente, Germany, June 1998.
  Advances in Computing Science, Springer Verlag, Wien New York.
  [PostScript] [BibTeX]
• Kolyang, Christoph Lüth, T. Meyer, Burkhart Wolff:
  TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving.
  TAPSOFT'97: Theory and Practice of Software Development. 7th International Joint Conference CAAP/FASE. Lille, France, April 1997.
  [PostScript] [BibTeX]
• Kolyang, Christoph Lüth, Thomas Meyer, Burkhart Wolff:
  Generic Interfaces for Formal Development Support Tools.
  Proc. International Workshop for Tool Support in Verification and Validation, Bremen, May 1996. BISS Monograph 1, Bremen, 1998.
  [Extended Abstract] [PostScript (submitted version)] [BibTeX]
• Christoph Lüth, Neil Ghani: Monads and Modular Term Rewriting.
  Category Theory and Computer Science, 7th Internal Conference CTCS'97, Santa Margherita Ligure, Italy, September 1997. Springer LNCS 1290.
  [PostScript] [PDF] [BibTeX]
• Kolyang, Christoph Lüth, Thomas Meyer, Burkhart Wolff:
  Generating Graphical User Interfaces in a Functional Setting.
  User Interfaces for Theorem Provers 1996 , University of York, England, 19.7.96.
  [PostScript] [BibTeX]
• Christoph Lüth: Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem.
  Rewriting Techniques and Applications, 7th International Conference RTA-96, New Brunswick, USA, July 1996. Springer LNCS 1103.
  [PostScript] [PDF] [BibTeX]

Workshops, Technical Reports and Theses

• Christoph Lüth: Schlussbericht des Projektes SAMS.
  Research Report DFKI-RR-10-01, Deutsches Forschungszentrum für Künstliche Intelligenz.
  [PDF] [BibTeX]
• Christoph Lüth: Formal Software Development: From Foundations to Tools
  Habilitation Thesis, University of Bremen, 2005.
  [Overview] [Full thesis]
• Christoph Lüth:
  Modular Modelling with Monads.
  Methods of Category Theory in Software Engineering. Dresden, November 2005.
  Technischer Bericht TUD-FI05-12, Fakultät Informatik, Technische Universität Dresden.
  [PostScript] [PDF]
• Christoph Lüth:
  Haskell in Space - an Interactive Game as a Functional Programming Exercise.
  Functional and Declarative Programming in Education. Pittsburgh, Pa, USA, October 2002.
  Technischer Bericht 0210, Institut für Informatik und Praktische Mathematik,Christian-Albrechts-Universität zu Kiel.
  An extended version appeared as an Eductional Pearl in the Journal of Functional Programming.
  [PostScript] [PDF] [BibTeX]
• Neil Ghani, Christoph Lüth, Stefan Kahrs: Rewriting the Conditions in Conditional Rewriting.
  Technical Report 2000/20, Dept. of Mathematics and Computer Science, University of Leicester.
  [PostScript] [BibTeX]
• Christoph Lüth: Categorical Term Rewriting: Monads and Modularity.
  PhD Thesis, University of Edinburgh, 1998.
  [PostScript] [BibTeX]
• Christoph Lüth: Transformational Program Development in the UniForM Workbench.
  Selected Papers from the 8th Nordic Workshop on Programming Theory. Research Report 248, Dept. of Informatics, University of Oslo.
  [PostScript] [BibTeX]
• Kolyang, Christoph Lüth, Thomas Meyer, Burkhart Wolff:
  Generic Transformation Systems for Formal Methods.
  System description for a tool demonstration at FME'97.
  [PostScript]
• Christoph Lüth, Stefan Westmeier, Burkhart Wolff: sml_tk: Functional Programming for Graphical User Interfaces.
  Technical Report 8/96, FB 3, University of Bremen. Bremen, 1996.
  [HTML] [PostScript, Part 1 and Part 2] [BibTeX]

Unpublished

• Christoph Lüth, Neil Ghani: An Introduction to Categorical Rewriting (1999)
  [PostScript]
• Christoph Lüth, Haykal Tej, Burkhart Wolff: Generic Transformational Program Development (1998)
  [PostScript]