Christoph Lüth

• Research
• Brief CV
• Publications
• Lecture archive
• Contact

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.

JournalArticles

• 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: 303-331, 2012.
  AbstractPDF BibTeX

  When autonomous robots begin to share the human living and working spaces, safety becomes paramount. It is legally required that the safety of such systems is ensured, e.g. by certification according to relevant standards such as IEC61508. However, such safety considerations are usually not addressed in academic robotics. In this paper we report on one such successful endeavour, which is concerned with designing, implementing, and certifying a collision avoidance safety function for autonomous vehicles and static obstacles. The safety function calculates a safety zone for the vehicle, depending on its current motion, which is as large as required but as small as feasible, thus ensuring safety against collision with static obstacles. We outline the algorithm which was specifically designed with safety in mind, and present our verification methodology which is based on formal proof and verification using the theorem prover Isabelle. The implementation and our methodology have been certified for use in applications up to SIL3 of IEC61508 by a certification authority (TÜV Süd Rail GmbH, Germany). Throughout, issues we recognised as being important for a successful application of formal methods in robotics are highlighted. Moreover, we argue that formal analysis deepens the understanding of the algorithm, and hence is valuable even outside the safety context.

  @article{5746
  ,   author= {Holger T\"aubig and Udo Frese and Christoph Hertzberg and Christoph L\"uth and Stefan Mohr and Elena Vorobev and Dennis Walter}
  ,   title= {Guaranteeing Functional Safety: Design for Provability and Computer-Aided Verification}
  ,   journal= {Autonomous Robots}
  ,   volume= {32}
  ,   pages= {303-331}
  ,   publisher= {Springer}
  ,   year= {2012}
  ,   keywords= {Collision Detection;  Functional Safety;  Formal Verification;  Certification;  IEC 61508; Braking Model;  Mathematical Proof}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/5746_Taubig2012_AR_author.pdf}
  }
  

• David Aspinall, Ewen Denney, Christoph Lüth. Tactics for Hierarchical Proofs.
  Mathematics in Computer Science, 3: 309-330, 2010.
  AbstractPDF BibTeX

  There is something of a discontinuity at the heart of popular tactical theorem provers. Low-level, fully-checked mechanical proofs are large trees consisting of primitive logical inferences. Meanwhile, high-level human inputs are lexically structured formal texts which include tactics describing search procedures. The proof checking process maps from the high-level to low-level, but after that, explicit connections are usually lost. The lack of connection can make it difficult to understand the proof trees produced by successful tactic proofs, and difficult to debug faulty tactic proofs. We propose the use of hierarchical proofs, also known as hiproofs, to help bridge these levels. Hiproofs superimpose a labelled hierarchical nesting on an ordinary proof tree, abstracting from the underlying logic. The labels and nesting are used to describe the organisation of the proof, typically relating to its construction process. In this paper we introduce a foundational tactic language Hitac which constructs hiproofs in a generic setting. Hitac programs can be evaluated using a big-step or a small-step operational semantics. The big-step semantics captures the intended meaning, whereas the small-step semantics is closer to possible implementations and provides a unified notion of proof state. We prove that the semantics are equivalent and construct valid proofs. We also explain how to detect terms which are stuck in the small-step semantics, and how these suggest interaction points with debugging tools. Finally we show some typical examples of tactics, constructed using tactical combinators, in our language.

  @article{4972
  ,   author= {David Aspinall and Ewen Denney and Christoph L\"uth}
  ,   title= {Tactics for Hierarchical Proofs}
  ,   journal= {Mathematics in Computer Science}
  ,   volume= {3}
  ,   pages= {309-330}
  ,   publisher= {Birkh\"auser}
  ,   year= {2010}
  ,   keywords= {hierachical proof, hiproof, tactical theorem proving}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4972_pgtactic-mcs.pdf}
  }
  

• Christoph Lüth, Bernd Krieg-Brückner. Sicherheit in der Künstlichen Intelligenz.
  KI - Künstliche Intelligenz, German Journal on Artificial Intelligence - Organ des Fachbereiches "Künstliche Intelligenz" der Gesellschaft für Informatik e.V., 1: 51-52, 2007.
  AbstractPDF BibTeX

  Dieses Jahr wurde die Künstliche Intelligenz fünfzig Jahre alt. Aus einem esoterischen Randbereich der Informatik ist eine Kerndisziplin geworden. Techniken der Künstlichen Intelligenz (KI) werden inzwischen in fast allen Gebieten der Informatik eingesetzt. In dem Maße, in dem sich diese Techniken verbreiten, stellt sich verstärkt die Frage nach der Sicherheit. Wenn ich künftig einen Serviceroboter einsetze, wie kann ich sicher sein, dass er mich nicht verletzt? In diesem Artikel stellen wir drei Techniken vor, mit denen das Vertrauen in die Zuverlässigkeit von KI-Systemen erhöht werden kann. Als Beispiele betrachten wir typische KI-Systeme wie Theorembeweiser und Roboter. Für beide ist Sicherheit unerlässlich: ein Theorembeweiser ist nur dann nützlich, wenn wir sicher sein können, dass er nur korrekte Beweise erzeugt (und nicht etwa Widersprüche), und ein mobiler Roboter sollte nicht mit Hindernissen kollidieren.

  @article{3894
  ,   author= {Christoph L\"uth and Bernd Krieg-Br\"uckner}
  ,   title= {Sicherheit in der K\"unstlichen Intelligenz}
  ,   journal= {KI - K\"unstliche Intelligenz, German Journal on Artificial Intelligence - Organ des Fachbereiches "K\"unstliche Intelligenz" der Gesellschaft f\"ur Informatik e.V.}
  ,   volume= {1}
  ,   pages= {51-52}
  ,   publisher= {B\"ottcherIT Verlag}
  ,   year= {2007}
  ,   linksMore= {http://www.informatik.uni-bremen.de/~cxl/papers/ki07.pdf}
  }
  

• Maksym Bortin, Einar Broch Johnsen, Christoph Lüth. Structured Formal Development in Isabelle.
  Nordic Journal of Computing, 13: 1-20, 2006.
  AbstractPDF BibTeX

  General purpose theorem provers provide advanced facilities for proving properties about specifications, and may therefore be a valuable tool in formal program development. However, these provers generally lack many of the useful structuring mechanisms found in functional programming or specification languages. This paper presents a constructive approach to adding theory morphisms and parametrisation to theorem provers, while preserving the proof support and consistency of the prover. The approach is implemented in Isabelle and illustrated by examples of an algorithm design rule and of the modular development of computational effects for imperative language features based on monads.

  @article{3895
  ,   author= {Maksym Bortin and Einar Broch Johnsen and Christoph L\"uth}
  ,   title= {Structured Formal Development in Isabelle}
  ,   journal= {Nordic Journal of Computing}
  ,   volume= {13}
  ,   pages= {1-20}
  ,   year= {2006}
  ,   linksMore= {http://www.informatik.uni-bremen.de/~cxl/papers/njc06.pdf}
  }
  

• Neil Ghani, Christoph Lüth, Federico de Marchi. Monads of Coalgebras: Rational Terms and Term Graphs.
  Mathematical Structures in Computer Science, 15(3): 433-- 451, June 2005.
  AbstractPDF BibTeX

  This paper introduces guarded and strongly guarded monads as a unified model of a variety of different term algebras covering fundamental examples such as initial algebras, final coalgebras, rational terms and term graphs. We develop a general method for obtaining finitary guarded monads which allows us to define and prove properties of the rational and term graph monads. Furthermore, our treatment of rational equations extends the traditional approach to allow right-hand sides of equations to be infinite terms, term graphs or other such coalgebraic structures. As an application, we use these generalised rational equations to sketch part of the correctness of the the term graph implementation of functional programming languages.

  @article{Lueth:MSCS04
  ,   author= {Neil Ghani and Christoph L\"uth and Federico de Marchi}
  ,   title= {Monads of Coalgebras: Rational Terms and Term Graphs}
  ,   journal= {Mathematical Structures in Computer Science}
  ,   volume= {15}
  ,   number= {3}
  ,   pages= {433-- 451}
  ,   month= {June}
  ,   year= {2005}
  ,   doi= {10.1017/S0960129505004743}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/mscs04.pdf}
  }
  

• Neil Ghani, Christoph Lüth. Rewriting via Coinserters.
  Nordic Journal of Computing, 10: 290-- 312, 2004.
  AbstractPDF BibTeX

  This paper introduces a semantics for rewriting that is independent of the data being rewritten and which, nevertheless, models key concepts such as substitution which are central to rewriting algorithms. We demonstrate the naturalness of this construction by showing how it mirrors the usual treatment of algebraic theories as coequalizers of monads. We also demonstrate its naturalness by showing how it captures several canonical forms of rewriting.

  @article{Lueth:RewritingCoinserter
  ,   author= {Neil Ghani and Christoph L\"uth}
  ,   title= {Rewriting via Coinserters}
  ,   journal= {Nordic Journal of Computing}
  ,   volume= {10}
  ,   pages= {290-- 312}
  ,   year= {2004}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/njc04b.pdf}
  }
  

• Einar Broch Johnsen, Christoph Lüth. Abstracting Transformations for Refinement.
  Nordic Journal of Computing, 10: 316-- 336, 2004.
  AbstractPDF BibTeX

  Formal program development by stepwise refinement involves a lot of work discharging proof obligations. Transformational techniques can reduce this work: applying correct transformation rules removes the need for verifying the correctness of each refinement step individually. However, a crucial problem is how to identify appropriate transformation rules. In this paper, a method is proposed to incrementally construct a set of correctness preserving transformation rules for refinement relations in arbitrary specification formalisms. Transformational developments are considered as proofs, which are generalised. This results in a framework where specific example refinements can be systematically generalised to more applicable transformation rules. The method is implemented in the Isabelle theorem prover and demonstrated on an example of data refinement.

  @article{Lueth:AbstractingTransformations
  ,   author= {Einar Broch Johnsen and Christoph L\"uth}
  ,   title= {Abstracting Transformations for Refinement}
  ,   journal= {Nordic Journal of Computing}
  ,   volume= {10}
  ,   pages= {316-- 336}
  ,   year= {2004}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/njc04a.pdf}
  }
  

• Federico de Marchi, Neil Ghani, Christoph Lüth. Coalgebraic Approaches to Algebraic Terms.
  Theoretical Informatics and Applications, 37: 301-- 314, 2003.
  AbstractPDF BibTeX

  Algebraic systems of equations define functions using recursion where parameter passing is permitted. This generalises the notion of a rational system of equations where parameter passing is prohibited. It has been known for some time that algebraic systems in Greibach Normal Form have unique solutions. This paper presents a categorical approach to algebraic systems of equations which generalises the traditional approach in two ways i) we define algebraic equations for locally finitely presentable categories rather than just Set; and ii) we define algebraic equations to allow right-hand sides which need not consist of finite terms. We show these generalised algebraic systems of equations have unique solutions by replacing the traditional metric-theoretic arguments with coalgebraic arguments.

  @article{Lueth:SolvingAlgebraicEquations
  ,   author= {Federico de Marchi and Neil Ghani and Christoph L\"uth}
  ,   title= {Coalgebraic Approaches to Algebraic Terms}
  ,   journal= {Theoretical Informatics and Applications}
  ,   volume= {37}
  ,   pages= {301-- 314}
  ,   year= {2003}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/ita04.pdf}
  }
  

• Christoph Lüth. Haskell in Space.
  Journal of Functional Programming, 13(6): 1077-- 1085, November 2003.
  AbstractPDF BibTeX

  This paper describes a practical exercise set to an introductory functional programming course. The exercise is to implement a small game involving a space ship in an asteroids belt, after the fashion of the classic Asteroids arcade game. The positive experience suggests that interactive graphics programs of this kind make good and entertaining programming exercises for functional programming courses.

  @article{Lueth:HaskellInSpace
  ,   author= {Christoph L\"uth}
  ,   title= {Haskell in Space}
  ,   journal= {Journal of Functional Programming}
  ,   volume= {13}
  ,   number= {6}
  ,   pages= {1077-- 1085}
  ,   month= {November}
  ,   year= {2003}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/jfp03.pdf}
  }
  

• Neil Ghani, Christoph Lüth, Federico de Marchi, John Power. Dualising Initial Algebras.
  Mathematical Structures in Computer Science, 13(2): 349-- 370, 2003.
  AbstractPDF BibTeX

  Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle and that final coalgebras can just as easily form monads as comonads and dually, that initial algebras form both monads and comonads. In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by defining a notion cosignature and coequation and then proving the models of this syntax are precisely the coalgebras of the representing comonad.

  @article{Lueth:MSCS
  ,   author= {Neil Ghani and Christoph L\"uth and Federico de Marchi and John Power}
  ,   title= {Dualising Initial Algebras}
  ,   journal= {Mathematical Structures in Computer Science}
  ,   year= {2003}
  ,   volume= {13}
  ,   number= {2}
  ,   pages= {349-- 370}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/mscs03.pdf}
  }
  

• Christoph Lüth, Burkhardt Wolff. Functional Design and Implementation of Graphical User Interfaces for Theorem Provers.
  Journal of Functional Programming, 9(2): 167-- 189, March 1999.
  AbstractPDF BibTeX

  The design of theorem provers, especially in the LCF-prover family, has strongly profited from functional programming. This paper attempts to develop a metaphor suited to visualize the LCF-style prover design, and a methodology for the implementation of graphical user interfaces for these provers and encapsulations of formal methods. In this problem domain, particular attention has to be paid to the need to construct a variety of objects, keep track of their interdependencies and provide support for their reconstruction as a consequence of changes. We present a prototypical implementation of a generic and open interface system architecture, and show how it can be instantiated to an interface for Isabelle, called IsaWin, as well as to a tailored tool for transformational program development, called TAS.

  @article{LuethWolff
  ,   author= {Christoph L\"uth and Burkhardt Wolff}
  ,   title= {Functional Design and Implementation of Graphical User Interfaces for Theorem Provers}
  ,   journal= {Journal of Functional Programming}
  ,   volume= {9}
  ,   number= {2}
  ,   pages= {167-- 189}
  ,   month= {March}
  ,   year= {1999}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/jfp99.pdf}
  }
  

Refereed Conferences or Workshops

• Christina Cociancig, Christoph Lüth, Rolf Drechsler. Modeling for Explainability: Ethical Decision-Making in Automated Resource Allocation.
  Proceedings of the Upper-Rhine Artificial Intelligence Symposium (UR-AI 2021), 2021.
  AbstractBibTeX

  Decisions delegated to artificial intelligence face an alignment problem: humans expect the algorithm to make fast and well-informed decisions aligning with human morals. In the design and engineering process of algorithms, ethical principles enter the black box explicitly and implicitly as functional or non-functional properties, much to the detriment of explainability and transparency. Previous work has established surrogate modeling to promote explainability and transparency of the decision-making process. We extend on this, model in lower complexity decision trees and as labeled transition systems, which is a method inherent to bisimulation theory, as well as evaluate on synthetic data with a rulebased algorithm. As a case study, we analyze the triage processes in German and Austrian hospitals during the COVID-19 pandemic, based on official guidelines that regulate the allocation of intensive care unit beds. We discovered that the decision processes are similar, however, the systems do not behave in the same manner. The diverging behavior equates to a discrepant ratio of patients treated in intensive care in contrast to the general ward. Our insight leads us to the conclusion that our approach ensures ethical decision-making in healthcare and should be considered due to its explainability and transparency.

  @inproceedings{11853
  ,   author= {Christina Cociancig and Christoph L\"uth and Rolf Drechsler}
  ,   title= {Modeling for Explainability: Ethical Decision-Making in Automated Resource Allocation}
  ,   year= {2021}
  ,   bookTitle= {Proceedings of the Upper-Rhine Artificial Intelligence Symposium (UR-AI 2021)}
  ,   conference= {Upper-Rhine Artificial Intelligence Symposium}
  }
  

• Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler. Performance Aspects of Correctness-oriented Synthesis Flows.
  9th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), 2021.
  AbstractPDF BibTeX

  When designing electronic circuits, available synthesis flows either focus on accelerating the synthesized circuit or correctness. In the quest for ever-faster hardware designs, the correctness of these designs is often neglected. Thus, designers need to trade-off between correctness and performance. The question is how large the trade-off is? This work presents a systematic comparison of two representative synthesis flows, the LegUp HLS framework as a representative for flows focusing on hardware acceleration, and a flow based on the proof assistant Coq focusing on correctness. For evaluation purposes, a 32-bit MIPS processor synthesized using the two flows, and the final HDL implementations are compared regarding their performance. Our evaluation allows a quantitative analysis of the trade-off, showing that correctness-oriented synthesis flows are competitive concerning performance.

  @inproceedings{11380
  ,   author= {Fritjof Bornebusch and Christoph L\"uth and Robert Wille and Rolf Drechsler}
  ,   title= {Performance Aspects of Correctness-oriented Synthesis Flows}
  ,   year= {2021}
  ,   bookTitle= {9th International Conference on Model-Driven Engineering and Software Development (MODELSWARD)}
  ,   conference= {International Conference on Model-Driven Engineering and Software Development}
  ,   keywords= {Hardware Designs,           Proof Assistants,           Functional HDLs,           Hardware Synthesis,           MIPS processor}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/11380_paper.pdf}
  }
  

• Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler. Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications.
  8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), Revised Selected Papers, 2021. Springer.
  AbstractPDF BibTeX

  This work proposes an alternative hardware design approach that allows the detection of arithmetic overflows at the specification level. The established hardware design approach describes infinite integer types at that level while the model describes finite types. This opens a semantic gap between both levels, which means that arithmetic overflows cannot be detected at the specification level. To address this problem the CompCert integer library is utilized that describes finite integer types as dependent types using the proof assistant Coq. Properties that argue about these finite types can be specified and verified at the specification level. This closes the semantic gap the established hardware design approach suffers from.

  @inproceedings{11456
  ,   author= {Fritjof Bornebusch and Christoph L\"uth and Robert Wille and Rolf Drechsler}
  ,   editor= {Slimane Hammoudi and Luís Ferreira Pires and Bran Selić}
  ,   title= {Safety First: About the Detection of Arithmetic Overflows in Hardware Design Specifications}
  ,   publisher= {Springer}
  ,   year= {2021}
  ,   bookTitle= {8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), Revised Selected Papers}
  ,   conference= {International Conference on Model-Driven Engineering and Software Development}
  ,   keywords= {Hardware Designs, Arithmetic Integer Overflows, Proof Assistants, Functional HDLs, Hardware Synthesis}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/11456_paper.pdf}
  }
  

• Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler. Integer Overflow Detection in Hardware Designs at the Specification Level.
  8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), 2020.
  AbstractPDF BibTeX

  In this work, we present a hardware design approach that allows the detection of integer overflows by describing finite integer types at the specification level. In contrast to the established design flow that uses infinite integer types at the specification level. This causes a semantic gap between these infinite types and the finite integer types used at the model level. The proposed design approach uses dependent types in combination with proof assistants. The combination allows the arguing about the behavior of finite integer types that is used to detect integer overflows at the specification level. To achieve this, we utilized the CompCert integer library that describes finite data types as dependent types.

  @inproceedings{10756
  ,   author= {Fritjof Bornebusch and Christoph L\"uth and Robert Wille and Rolf Drechsler}
  ,   title= {Integer Overflow Detection in Hardware Designs at the Specification Level}
  ,   year= {2020}
  ,   bookTitle= {8th International Conference on Model-Driven Engineering and Software Development (MODELSWARD)}
  ,   conference= {International Conference on Model-Driven Engineering and Software Development}
  ,   keywords= {Hardware Designs, Integer Overflows, Proof Assistants, Functional HDLs, Hardware Synthesis}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/10756_integer_overflow_detection_in_hardware_designs_at_the_specification_level.pdf}
  }
  

• Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler. Towards Automatic Hardware Synthesis from Formal Specification to Implementation.
  25th Asia and South Pacific Design Automation Conference (ASP-DAC), 2020.
  AbstractPDF BibTeX

  In this work, we sketch an automated design flow for hardware synthesis based on a formal specification. Verification results are propagated from the FSL level through the proposed flow to generate an ESL model as well as an RTL implementation automatically. In contrast, the established design flow relies on manual implementations at the ESL and RTL level. The proposed design flow combines proof assistants with functional hardware description languages. This combination decreases the implementation effort significantly and the generation of testbenches is no longer needed. We illustrate our design flow by specifying and synthesizing a set of benchmarks that contain sequential and combinational hardware designs. We compare them with implementations required by the established hardware design flow.

  @inproceedings{10702
  ,   author= {Fritjof Bornebusch and Christoph L\"uth and Robert Wille and Rolf Drechsler}
  ,   title= {Towards Automatic Hardware Synthesis from Formal Specification to Implementation}
  ,   year= {2020}
  ,   bookTitle= {25th Asia and South Pacific Design Automation Conference (ASP-DAC)}
  ,   conference= {Asia and South Pacific Design Automation Conference}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/10702_towards_automatic_hardware_synthesis_from_formal_specification_to_implementation.pdf}
  }
  

• Martin Ring, Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler. Verification Runtime Analysis: Get the Most Out of Partial Verification.
  Design, Automation & Test in Europe, 2020. IEEE.
  AbstractBibTeX

  The design of modern systems has reached a complexity which makes it inevitable to apply verification methods in order to guarantee its correct and safe execution. The verification methods frequently produce proof obligations that can not be solved any more due to the huge search space. However, by setting enough variables to fixed values, the search space is obviously reduced and solving engines eventually may be able to complete the verification task. Although this results in a \emph{partial verification}, the results may still be valuable --- in particular as opposed to the alternative of no verification at all. However, so far no systematic investigation has been conducted on which variables to fix in order to reduce verification runtime as much as possible while, at the same time, still getting most coverage. This paper addresses this question by proposing a corresponding verification runtime analysis. Experimental evaluations confirm the potential of this approach.

  @inproceedings{11457
  ,   author= {Martin Ring and Fritjof Bornebusch and Christoph L\"uth and Robert Wille and Rolf Drechsler}
  ,   title= {Verification Runtime Analysis: Get the Most Out of Partial Verification}
  ,   publisher= {IEEE}
  ,   year= {2020}
  ,   bookTitle= {Design, Automation & Test in Europe}
  ,   conference= {Design, Automation & Test in Europe}
  }
  

• Martin Ring, Fritjof Bornebusch, Christoph Lüth, Robert Wille, Rolf Drechsler. Better Late Than Never: Verification of Embedded Systems After Deployment.
  Design, Automation & Test in Europe, 2019.
  AbstractPDF BibTeX

  This paper investigates the benefits of verifying embedded systems after deployment. We argue that the huge state spaces of contemporary embedded and cyber-physical systems are caused by the large variety of operating contexts, which are unknown during development. Once the system is deployed, these contexts become observable, confining several variables. By this, the search space is dramatically reduced, making verification possible even on the limited resources of a deployed system. In this paper, we propose a design and verification flow which exploits this observation. We show how specifications are transferred to the deployed system and verified there. Evaluations on a number of case studies demonstrate the reduction of the search space, and we sketch how the proposed approach can be employed in practice.

  @inproceedings{10130
  ,   author= {Martin Ring and Fritjof Bornebusch and Christoph L\"uth and Robert Wille and Rolf Drechsler}
  ,   title= {Better Late Than Never: Verification of Embedded Systems After Deployment}
  ,   year= {2019}
  ,   bookTitle= {Design, Automation & Test in Europe}
  ,   conference= {Design, Automation & Test in Europe}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/10130_date2019_-_better_late_than_never_verification_of_embedded_systems_after_deployment.pdf}
  }
  

• Martin Ring, Christoph Lüth. Let's Prove It Later --- Verification at Different Points in Time.
  Software Engineering and Formal Methods - 17th International Conference, Proceedings., 2019. Lecture Notes in Computer Science 11724, p. 454-468. Springer.
  AbstractPDF BibTeX

  The vast majority of cyber-physical and embedded systems today is deployed without being fully formally verified during their design. Postponing verification until after deployment is a possible way to cope with this, as the verification process can benefit from instantiating operating parameters which were unknown at design time. But there exist many interesting alternatives between early verification (at design time) and late verification (at runtime). Moreover, this decision also has an impact on the specification style. Using a case study of the safety properties of an access control system, this paper explores the implications of different points in time chosen for verification, and points out the respective benefits and trade-offs. Further, we sketch some general rules to govern the decision when to verify a system.

  @inproceedings{10682
  ,   author= {Martin Ring and Christoph L\"uth}
  ,   editor= {Peter Csaba \"Olveczky and Gwen Sala\"un}
  ,   title= {Let's Prove It Later --- Verification at Different Points in Time}
  ,   volume= {11724}
  ,   pages= {454-468}
  ,   publisher= {Springer}
  ,   year= {2019}
  ,   bookTitle= {Software Engineering and Formal Methods - 17th International Conference, Proceedings.}
  ,   conference= {International Conference on Software Engineering and Formal Methods}
  ,   series= {Lecture Notes in Computer Science}
  ,   isbn= {978-3-030-30446-1}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/10682_main.pdf}
  }
  

• Rolf Drechsler, Christoph Lüth, Goerschwin Fey, Tim Güneysu. Towards Self-Explaining Digital Systems: A Design Methodology for the Next Generation.
  3rd International Verification and Security Workshop (IVSW), 2018.
  AbstractBibTeX

  As digital systems get ever more complex, their behaviour may at times appear unfathomable. Users will only be prepared to accept this if they are convinced that the system does indeed work correctly. Thus, we argue the need for self-explaining systems: systems that are able to explain their behaviour, and the reasons for it. In this paper, we propose first steps towards a design methodology for such systems, and argue that beyond user acceptance, self-explanation also has other applications such as self-verification and reconfiguration. We propose a conceptual framework for self-explaining systems, discuss how to achieve completeness, and consider implementation aspects.

  @inproceedings{9868
  ,   author= {Rolf Drechsler and Christoph L\"uth and Goerschwin Fey and Tim G\"uneysu}
  ,   title= {Towards Self-Explaining Digital Systems: A Design Methodology for the Next Generation}
  ,   year= {2018}
  ,   bookTitle= {3rd International Verification and Security Workshop (IVSW)}
  ,   conference= {International Verification and Security Workshop}
  }
  

• Martin Ring, Christoph Lüth. Interactive Proof Presentations with Cobra.
  Workshop on User Interfaces for Theorem Provers (UITP2016), 2017. Electronic Proceedings in Theoretical Computer Science 239, p. 43-52. Open Publishing Association.
  AbstractPDF BibTeX

  We present Cobra, a modern code and proof presentation framework, leveraging cutting-edge presentation technology together with a state of the art interactive theorem prover to present formalized mathematics as active documents. Cobra provides both an easy way to present proofs and a novel approach to auditorium interaction. The presentation is checked live by the theorem prover, and moreover allows live changes both by the presenter as well as the audience.

  @inproceedings{8590
  ,   author= {Martin Ring and Christoph L\"uth}
  ,   editor= {Serge Autexier and Pedro Queresma}
  ,   title= {Interactive Proof Presentations with Cobra}
  ,   volume= {239}
  ,   pages= {43-52}
  ,   publisher= {Open Publishing Association}
  ,   year= {2017}
  ,   bookTitle= {Workshop on User Interfaces for Theorem Provers (UITP2016)}
  ,   conference= {User Interfaces for Theorem Provers}
  ,   series= {Electronic Proceedings in Theoretical Computer Science}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/8590_main.pdf}
  }
  

• Christoph Lüth, Martin Ring, Rolf Drechsler. Towards a Methodology for Self-Verification.
  6th International Conference on Reliability, Infocom Technologies and Optimization (ICRITO 2017), 2017. IEEE.
  AbstractPDF BibTeX

  The exponential growth of the complexity of electronic systems makes their verification increasingly difficult. To address this problem, incremental refinements of existing approaches are insufficient in the long term; new approaches are needed. In this paper, we explore the new approach of self-verification, where systems will verify themselves during run time. Self-verification will give system engineers more time, more resources, and more information to successfully finish the verification. We sketch an architecture and methodology for self-verification, which maps system properties to the development phase in which they are verified, and illustrate the approach with a first case study.

  @inproceedings{9350
  ,   author= {Christoph L\"uth and Martin Ring and Rolf Drechsler}
  ,   editor= {Sunil Khatri}
  ,   title= {Towards a Methodology for Self-Verification}
  ,   publisher= {IEEE}
  ,   year= {2017}
  ,   bookTitle= {6th International Conference on Reliability, Infocom Technologies and Optimization (ICRITO 2017)}
  ,   conference= {IEEE Conference on  Reliability, Infocom Technologies and Optimization}
  ,   keywords= {self-verification, cyber-physical systems,  verification}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/9350_PID4986755.pdf}
  }
  

• Martin Ring, Jannis Ulrich Stoppe, Christoph Lüth, Rolf Drechsler. Change Impact Analysis for Hardware Designs.
  Forum on Specification & Design Languages FDL 2016, 2016. ECSI - European Electronic Chips and Systems design Initiative.
  AbstractPDF BibTeX

  Design processes are increasingly moving to more abstract description levels; no single formalism can handle the complexities of modern designs. However, keeping designs consistent across different abstraction levels, in particular in the presence of changes, has up to now been an arduous manual task. This paper presents a framework which provides a uniform, interconnected representation of the descriptions across the abstraction levels, starting from natural language requirement specifications over SysML design specifications down to executable SystemC models, allowing to track changes on all levels of abstraction, and ensuring consistency throughout the development process. The framework has been implemented in a tool, ChImpAnC, to show its viability. It assists the developer by highlighting inconsistencies and proof obligations across various descriptions levels in order to simplify

  @inproceedings{8898
  ,   author= {Martin Ring and Jannis Ulrich Stoppe and Christoph L\"uth and Rolf Drechsler}
  ,   title= {Change Impact Analysis for Hardware Designs}
  ,   publisher= {ECSI - European Electronic Chips and Systems design Initiative}
  ,   year= {2016}
  ,   bookTitle= {Forum on Specification & Design Languages FDL 2016}
  ,   conference= {Forum on Specification & Design Languages}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/8898_main-final-IEEE-certified.pdf}
  }
  

• Martin Ring, Christoph Lüth, Rolf Drechsler, Jannis Ulrich Stoppe. Change Management for Hardware Designers.
  3rd Workshop on Design Automation for Understanding Hardware Designs (DUHDe 2016), 2016.
  AbstractPDF BibTeX

  To cope with rising hardware complexity, design processes are increasingly moved to more abstract description languages. Different descriptions impede the design process because they are usually disconnected. Therefore, adding more layers to the design process adds additional overhead to e.g. ensure that changes that are applied on the system level description are either done in accordance with other less or more abstract descriptions or that these changes are propagated accordingly. Managing these changes has so far been a manual task. This paper presents the Change Impact Analysis and Control Tool (ChimpanC), a tool that uses state of the art analysis methods on various abstraction levels to build a single, interconnected model of these descriptions. These are used to track and manage any changes on each level of abstraction and their various refinement steps to ensure consistency throughout the development process. The result is a tool that assists the developer by highlighting inconsistencies and required proof obligations across various descriptions in order to simplify the development process over various abstraction levels.

  @inproceedings{8249
  ,   author= {Martin Ring and Christoph L\"uth and Rolf Drechsler and Jannis Ulrich Stoppe}
  ,   title= {Change Management for Hardware Designers}
  ,   year= {2016}
  ,   bookTitle= {3rd Workshop on Design Automation for Understanding Hardware Designs (DUHDe 2016)}
  ,   conference= {Workshop on Design Automation for Understanding Hardware Designs}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/8249_main-submitted.pdf}
  }
  

• Tim Schwartz, Michael Feld, Dennis Mronga, Gerald Pirkl, Torsten Spieldenner, Malte Wirkus, Ingo Zinnikus, Sirko Straube, Christian Bürckert, Svilen Dimitrov, Joachim Folz, Peter Hevesi, Dieter Hutter, Bernd Kiefer, Hans-Ulrich Krieger, Christoph Lüth. Hybrid Teams of Humans, Robots and Virtual Agents in a Production Setting.
  Proceedings of the 12th International Conference on Intelligent Environments, 2016. IEEE.
  AbstractPDF BibTeX

  This video paper describes the practical outcome of the first milestone of a project aiming at setting up a socalled Hybrid Team that can accomplish a wide variety of different tasks. In general, the aim is to realize and examine the collaboration of augmented humans with autonomous robots, virtual characters and SoftBots (purely software based agents) working together in a Hybrid Team to accomplish common tasks. The accompanying video shows a customized packaging scenario and can be downloaded from http://hysociatea.dfki.de/?p=441.

  @inproceedings{8373
  ,   author= {Tim Schwartz and Michael Feld and Dennis Mronga and Gerald Pirkl and Torsten Spieldenner and Malte Wirkus and Ingo Zinnikus and Sirko Straube and Christian B\"urckert and Svilen Dimitrov and Joachim Folz and Peter Hevesi and Dieter Hutter and Bernd Kiefer and Hans-Ulrich Krieger and Christoph L\"uth}
  ,   title= {Hybrid Teams of Humans, Robots and Virtual Agents in a Production Setting}
  ,   publisher= {IEEE}
  ,   year= {2016}
  ,   bookTitle= {Proceedings of the 12th International Conference on Intelligent Environments}
  ,   conference= {International Conference on Intelligent Environments}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/8373_hysociatea.pdf and https://ieeexplore.ieee.org/document/7723506}
  }
  

• Tim Schwartz, Hans-Ulrich Krieger, Norbert Schmitz, Malte Wirkus, Sirko Straube, Ingo Zinnikus, Christian Bürckert, Joachim Folz, Bernd Kiefer, Peter Hevesi, Christoph Lüth, Gerald Pirkl, Torsten Spieldenner. Hybrid Teams: Flexible Collaboration Between Humans, Robots and Virtual Agents.
  Proceedings of the 14th German Conference on Multiagent System Technologies (Mates 2016), 2016. Lecture Notes in Artificial Intelligence 9872, p. 131-146. Springer.
  AbstractPDF BibTeX

  With the increasing capabilities of agents using Artifcial Intelligence, an opportunity opens up to form teamlike collaboration between humans and artifcial agents. This paper describes the setting-up of a Hybrid Team consisting of humans, robots, virtual characters and softbots. The team is situated in a exible industrial production. Once established, Hybrid Teams can generally accomplish diverse mission scenarios. The work presented here focuses on the architecture and the characteristics of the team members and components. To achieve the overall team goals, several challenges have to be met to find a balance between autonomous behaviours of individual agents and coordinated teamwork. A Hybrid Team can heavily benefit from the heterogeneity of the team members. Humans have the highest overall intelligence, so they are always in the center of the process and take over a leading role if necessary.

  @inproceedings{8634
  ,   author= {Tim Schwartz and Hans-Ulrich Krieger and Norbert Schmitz and Malte Wirkus and Sirko Straube and Ingo Zinnikus and Christian B\"urckert and Joachim Folz and Bernd Kiefer and Peter Hevesi and Christoph L\"uth and Gerald Pirkl and Torsten Spieldenner}
  ,   editor= {Matthias Klusch and Rainer Unland and Onn Shehory and Alexander Pokhar and Sebastian Ahrndt}
  ,   title= {Hybrid Teams: Flexible Collaboration Between Humans, Robots and Virtual Agents}
  ,   volume= {9872}
  ,   pages= {131-146}
  ,   publisher= {Springer}
  ,   year= {2016}
  ,   bookTitle= {Proceedings of the 14th German Conference on Multiagent System Technologies (Mates 2016)}
  ,   conference= {German Conference on Multiagent System Technologies}
  ,   series= {Lecture Notes in Artificial Intelligence}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/8634_20160829_Hybrid_Teams Flexible Collaboration Between Humans Robots and Virtual Agents.pdf and https://link.springer.com/content/pdf/10.1007%2F978-3-319-45889-2_10.pdf}
  }
  

• Rolf Drechsler, Serge Autexier, Christoph Lüth. Model-based Specification and Refinement for Cyber-Physical Systems.
  5th International Conference on Dynamics in Logistics (LDIC 2016), 2016. Lecture Notes in Logistics, p. 3-17. Springer.
  AbstractPDF BibTeX

  Cyber-physical systems are small yet powerful systems which are embedded into their environment, adapting to its changes and at the same controlling it, and often operating autonomously. These systems have reached a level of complexity that opens up new application areas, but at the same time strains the existing design flows in system development. To ameliorate this problem, we propose a novel design flow for cyber-physical systems by adapting model-based specification and refinement methods known from software development. The design flow allows to start with a system specification and its essential properties at a high level of abstraction, and gradually refines it down to an electronic system level. Properties of higher levels can be inherited during refinements to lower levels by relying on local proof obligations only, which results in a design flow capable to keep up with the increasing complexity of cyber-physical systems.

  @inproceedings{8279
  ,   author= {Rolf Drechsler and Serge Autexier and Christoph L\"uth}
  ,   editor= {Michael Freitag and Herbert Kotzab and J\"urgen Pannek (Ed)}
  ,   title= {Model-based Specification and Refinement for Cyber-Physical Systems}
  ,   pages= {3-17}
  ,   publisher= {Springer}
  ,   year= {2016}
  ,   bookTitle= {5th International Conference on Dynamics in Logistics (LDIC 2016)}
  ,   conference= {International Conference on Dynamics in Logistics}
  ,   series= {Lecture Notes in Logistics}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/8279_main.pdf}
  }
  

• Martin Ring, Christoph Lüth. Collaborative Interactive Theorem Proving with Clide.
  Interactive Theorem Proving ITP 2014, 2014. Lecture Notes in Computer Science 8558, p. 467-482. Springer Verlag.
  AbstractPDF BibTeX

  This paper introduces Clide, a collaborative web interface for the Isabelle theorem prover. The interface allows a document-oriented interaction with Isabelle very much like Isabelle's desktop interface. Moreover, it allows users to jointly edit Isabelle proof scripts over the web; editing operations are synchronised to all users who have opened the proof script. The paper describes motivation, user experience, implementation and system architecture of Clide. The implementation is based on the theory of operational transformations; its key concepts have been formalised in Isabelle, its correctness proven and critical parts of the implementation on the server are generated from the formalisation, thus increasing confidence in the system.

  @inproceedings{7385
  ,   author= {Martin Ring and Christoph L\"uth}
  ,   editor= {G. Klein and R. Gamboa}
  ,   title= {Collaborative Interactive Theorem Proving with Clide}
  ,   volume= {8558}
  ,   pages= {467-482}
  ,   publisher= {Springer Verlag}
  ,   year= {2014}
  ,   bookTitle= {Interactive Theorem Proving ITP 2014}
  ,   conference= {International Conference on Interactive Theorem Proving}
  ,   series= {Lecture Notes in Computer Science}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/7385_main-final.pdf and http://www.informatik.uni-bremen.de/~cxl/papers/itp2014-appendix.pdf}
  }
  

• Mathias Soeken, Christoph Lüth, Rolf Drechsler. Entwurf cyber-physikalischer Systeme hoher Qualität und Sicherheit.
  Electronic Design Automation Workshop - Proceedings, 2014. VDE.
  BibTeX

  @inproceedings{7267
  ,   author= {Mathias Soeken and Christoph L\"uth and Rolf Drechsler}
  ,   title= {Entwurf cyber-physikalischer Systeme hoher Qualit\"at und Sicherheit}
  ,   publisher= {VDE}
  ,   year= {2014}
  ,   bookTitle= {Electronic Design Automation Workshop - Proceedings}
  ,   conference= {Electronic Design Automation Workshop}
  }
  

• Martin Ring, Christoph Lüth. Real-time collaborative Scala development with Clide.
  Proceedings of the Fifth Annual Scala Workshop, 2014. p. 63-66. ACM.
  AbstractPDF BibTeX

  We present Clide, a real-time collaborative development environment. Clide offers a new approach to tool integration which complements the way resources are shifted to the cloud today. We achieve this by introducing the novel concept of universal collaboration, which drops the distinction between human and non-human participants (so-called assistants) and enables innovative ways of interaction. Clide has a highly flexible and distributed architecture based on Akka. Despite the complexity of the synchronisation of distributed document states, implementing assistants is pleasantly simple. To demonstrate the versatility and usability of the platform we implement a simple wrapper turning the Scala compiler into a collaborator, offering content assistance to other developers and tools.

  @inproceedings{7514
  ,   author= {Martin Ring and Christoph L\"uth}
  ,   editor= {Heather Miller and Philipp Haller}
  ,   title= {Real-time collaborative Scala development with Clide}
  ,   pages= {63-66}
  ,   publisher= {ACM}
  ,   year= {2014}
  ,   bookTitle= {Proceedings of the Fifth Annual Scala Workshop}
  ,   conference= {Scala Workshop}
  ,   isbn= {978-1-4503-2868-5}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/7514_p63-ring.pdf}
  }
  

• Christoph Lüth, Serge Autexier, Dieter Hutter, Mathias Soeken, Robert Wille, Rolf Drechsler. SPECifIC - A New Design Flow for Cyber-Physical Systems.
  CPS20: CPS 20 years from now - visions and challenges - CyPhERS 2nd Experts Workshop, 2014. p. 4-7.
  AbstractPDF BibTeX

  In this position paper, we propose a new design flow for cyber-physical systems which builds on our previous experiences in both the hardware and software domain. Its defining features are the integration of natural language processing, the formal specification level which allows an abstract description of the system's behaviour, and a comprehensive functional change management throughout. We introduce the design flow and its three levels of abstraction by example, and argue why it is particularly suited for the development of cyber-physical systems.

  @inproceedings{7285
  ,   author= {Christoph L\"uth and Serge Autexier and Dieter Hutter and Mathias Soeken and Robert Wille and Rolf Drechsler}
  ,   title= {SPECifIC - A New Design Flow for Cyber-Physical Systems}
  ,   pages= {4-7}
  ,   year= {2014}
  ,   bookTitle= {CPS20: CPS 20 years from now - visions and challenges - CyPhERS 2nd Experts Workshop}
  ,   conference= {CyPhERS Experts Workshop}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/7285_CPS20_SPECifIC.pdf and http://www.cyphers.eu/cps20}
  }
  

• David Aspinall, Ewen Denney, Christoph Lüth. A Semantic Basis for Proof Queries and Transformations.
  Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, 2013. Lecture Notes in Computer Science 8312, p. 53-70. Springer.
  AbstractPDF BibTeX

  We extend the query language PrQL, which is designed for inspecting machine representations of proofs, to also allow transformations of these proofs. There are several novel aspects. First, PrQL natively supports hiproofs which express proof structure using hierarchically nested labelled trees, which we claim is a natural way of taming the complexity of huge proofs. Query-driven transformations enable manipulation of this structure, in particular, to transform proofs produced by interactive theorem provers into forms that assist their understanding, or that could be consumed by other tools. In this paper we motivate and define basic transformation operations, using a new abstract denotational semantics of hiproofs and queries. This extends our previous semantics for queries based on syntactic tree representations. We define update operations that add and remove sub-proofs, and manipulate the hierarchy to group and ungroup nodes. We show that these basic operations are well-behaved so can form a sound core for a hierarchical transformation language.

  @inproceedings{7110
  ,   author= {David Aspinall and Ewen Denney and Christoph L\"uth}
  ,   editor= {Kevin McMillan and Aart Middeldorp and Andrei Voronkov}
  ,   title= {A Semantic Basis for Proof Queries and Transformations}
  ,   volume= {8312}
  ,   pages= {53-70}
  ,   publisher= {Springer}
  ,   year= {2013}
  ,   bookTitle= {Proceedings of the 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning}
  ,   conference= {International Conference on Logic for Programming, Artificial Intelligence, and Reasoning}
  ,   series= {Lecture Notes in Computer Science}
  ,   keywords= {proof trees, query language, update language, hiproofs, tree transformations		}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/7110_main.pdf}
  }
  

• Christoph Lüth, Martin Ring. A Web Interface for Isabelle: The Next Generation.
  Conferences on Intelligent Computer Mathematics CICM 2013, 2013. Lecture Notes in Artificial Intelligence 7961, p. 326-329. Springer.
  AbstractPDF BibTeX

  We present Clide, a web interface for the interactive theorem prover Isabelle. Clide uses latest web technology and the Isabelle/PIDE framework to implement a web-based interface for asynchronous proof document management that competes with, and in some aspects even surpasses, conventional user interfaces for Isabelle such as Proof General or Isabelle/jEdit.

  @inproceedings{6811
  ,   author= {Christoph L\"uth and Martin Ring}
  ,   editor= {Jacques Carette}
  ,   title= {A Web Interface for Isabelle: The Next Generation}
  ,   volume= {7961}
  ,   pages= {326-329}
  ,   publisher= {Springer}
  ,   year= {2013}
  ,   bookTitle= {Conferences on Intelligent Computer Mathematics CICM 2013}
  ,   conference= {Conferences on Intelligent Computer Mathematics}
  ,   series= {Lecture Notes in Artificial Intelligence}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/6811_main.pdf}
  }
  

• David Aspinall, Ewen Denney, Christoph Lüth. Querying Proofs.
  18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18), 2012. Lecture Notes in Computer Science 7180, p. 92-106. Springer Verlag.
  AbstractPDF BibTeX

  We motivate and introduce a query language PrQL designed for inspecting machine representations of proofs. PrQL natively supports hiproofs which express proof structure using hierarchical nested labelled trees. The core language presented in this paper is locally structured, with queries built using recursion and patterns over proof structure and rule names. We define the syntax and semantics of locally structured queries, demonstrate their power, and sketch some implementation experiments.

  @inproceedings{5817
  ,   author= {David Aspinall and Ewen Denney and Christoph L\"uth}
  ,   title= {Querying Proofs}
  ,   volume= {7180}
  ,   pages= {92-106}
  ,   publisher= {Springer Verlag}
  ,   year= {2012}
  ,   bookTitle= {18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)}
  ,   conference= {International Conference on Logic for Programming, Artificial Intelligence, and Reasoning}
  ,   series= {Lecture Notes in Computer Science}
  ,   keywords= {proofs, query languages, theorem proving}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/5817_lpar2012.pdf}
  }
  

• Serge Autexier, Dominik Dietrich, Dieter Hutter, Christoph Lüth, Christian Maeder. SmartTies - Management of Safety-Critical Developments.
  Proc. 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLa'12), 2012. Lecture Notes in Computer Science 7609, p. 238-252. Springer.
  AbstractPDF BibTeX

  Formal methods have been successfully used to establish assurances for safety-critical systems with mathematical rigor. Based on our experience in developing a methodology and corresponding tools for change management for formal methods, we have generalised this approach to a comprehensive methodology for maintaining heterogeneous collections of both formal and informal documents. Although informal documents, like natural language text, lack a formal interpretation, they still expose a visible structure that reflects different aspects or parts of a development and follows explicit rules formulated in development guidelines. This paper presents our general methodology for maintaining heterogeneous document collections and illustrates its instantiation in the SmartTies tool that supports the development of safety-critical systems. SmartTies utilises the structuring mechanisms prescribed in a certification process to analyze and maintain the documents occurring in safety-critical development processes.

  @inproceedings{6270
  ,   author= {Serge Autexier and Dominik Dietrich and Dieter Hutter and Christoph L\"uth and Christian Maeder}
  ,   editor= {Margaria Tiziana and Bernhard Steffen}
  ,   title= {SmartTies - Management of Safety-Critical Developments}
  ,   volume= {7609}
  ,   pages= {238-252}
  ,   publisher= {Springer}
  ,   year= {2012}
  ,   bookTitle= {Proc. 5th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLa'12)}
  ,   conference= {International Symposium On Leveraging Applications of Formal Methods, Verification and Validation}
  ,   series= {Lecture Notes in Computer Science}
  ,   keywords= {Change Management, Safety-Critical Systems, Formal Methods, Graph Rewriting}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/6270_SmartTies.pdf}
  }
  

• Serge Autexier, Christoph Lüth. Adding Change Impact Analysis to the Formal Verification of C Programs.
  Proceedings 8th International Conference on Integrated Formal Methods (iFM 2010), 2010. Lecture Notes in Computer Science 6396, p. 59-73. Springer.
  AbstractPDF BibTeX

  Handling changes to programs and specifications efficiently is a particular challenge in formal software verification. Change impact analysis is an approach to this challenge where the effects of changes made to a document (such as a program or specification) are described in terms of rules on a semantic representation of the document. This allows to describe and delimit the effects of syntactic changes semantically. This paper presents an application of generic change impact analysis to formal software verification, using the GMOC and SAMS tools. We adapt the GMOC tool for generic change impact analysis to the SAMS verification framework for the formal verification of C programs, and show how a few simple rules are sufficient to capture the essence of change management.

  @inproceedings{4919
  ,   author= {Serge Autexier and Christoph L\"uth}
  ,   editor= {Dominique Méry and Stephan Merz}
  ,   title= {Adding Change Impact Analysis to the Formal Verification of C Programs}
  ,   volume= {6396}
  ,   pages= {59-73}
  ,   publisher= {Springer}
  ,   year= {2010}
  ,   bookTitle= {Proceedings 8th International Conference on Integrated Formal Methods (iFM 2010)}
  ,   conference= {International Conference on Integrated Formal Methods}
  ,   series= {Lecture Notes in Computer Science}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4919_paper.pdf}
  }
  

• Dennis Walter, Holger Täubig, Christoph Lüth. Experiences in Applying Formal Verification in Robotics.
  SafeComp 2010 --- 29th International Conference on Computer Safety, Reliability and Security, Proceedings, 2010. Lecture Notes in Computer Science 6351, p. 347-360. Springer.
  AbstractPDF BibTeX

  In this paper we report on our experiences in applying formal methods, more precisely formal domain modelling and code verification within the theorem prover Isabelle, in the domain of safety-related opto-electronic protective devices. We outline an algorithm that was specifically designed with safety through formal verification in mind. The algorithm has been certified for use in applications up to SIL 3 of IEC 61508 by a certification authority. Our verification methodolody is presented, which has also been accepted for use in safety contexts up to SIL 3, and the necessary normative measures that are covered by its use are discussed. Throughout, issues we recognised as being important for a successful application of formal methods in the domain at hand are highlighted. These pertain to the development process, the abstraction level at which specifications should be formulated, and the interplay between simulation and verification, among others.

  @inproceedings{4973
  ,   author= {Dennis Walter and Holger T\"aubig and Christoph L\"uth}
  ,   title= {Experiences in Applying Formal Verification in Robotics}
  ,   volume= {6351}
  ,   pages= {347-360}
  ,   publisher= {Springer}
  ,   year= {2010}
  ,   bookTitle= {SafeComp 2010 --- 29th International Conference on Computer Safety, Reliability and Security, Proceedings}
  ,   conference= {International Conference on Computer Safety, Reliability and Security}
  ,   series= {Lecture Notes in Computer Science}
  ,   keywords= {formal methods, safety-related systems, verification, specifications, formal models}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4973_safecomp2010.pdf}
  }
  

• Maksym Bortin, Christoph Lüth. Structural Formal Development with Quotient Types in Isabelle/HOL.
  10th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2010), 2010. Lecture Notes in Computer Science 6167, p. 34-48. Springer.
  AbstractPDF BibTeX

  General purpose theorem provers provide sophisticated proof methods, but lack some of the advanced structuring mechanisms found in specification languages. This paper builds on previous work extending the theorem prover Isabelle with such mechanisms. A way to build the quotient type over a given base type and an equivalence relation on it, and a generalised notion of folding over quotiented types is given as a formalised high-level step called a design tactic. The core of this paper are four axiomatic theories capturing the design tactic. The applicability is demonstrated by derivations of implementations for finite multisets and finite sets from lists in Isabelle.

  @inproceedings{4974
  ,   author= {Maksym Bortin and Christoph L\"uth}
  ,   title= {Structural Formal Development with Quotient Types in Isabelle/HOL}
  ,   volume= {6167}
  ,   pages= {34-48}
  ,   publisher= {Springer}
  ,   year= {2010}
  ,   bookTitle= {10th International Conference on Artificial Intelligence and Symbolic Computation (AISC 2010)}
  ,   conference= {International Conference on Artificial Intelligence and Symbolic Computation}
  ,   series= {Lecture Notes in Computer Science}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4974_aisc2010.pdf}
  }
  

• Christoph Lüth, Dennis Walter. Certifiable specification and verification of C programs.
  FM 2009: Formal Methods, 2009. Lecture Notes in Computer Science 5350, p. 419-434. Springer.
  AbstractPDF BibTeX

  A novel approach to the specification and verification of C programs through an annotation language that is a mixture between JML and the language of Isabelle/HOL is proposed. This yields three benefits: specifications are concise and close to the underlying mathematical model; existing Isabelle theories can be reused; and the leap of faith from specification language to encoding in a logic is small. This is of particular relevance for software certification, and verification in application areas such as robotics.

  @inproceedings{4426
  ,   author= {Christoph L\"uth and Dennis Walter}
  ,   title= {Certifiable specification and verification of C programs}
  ,   volume= {5350}
  ,   pages= {419-434}
  ,   publisher= {Springer}
  ,   year= {2009}
  ,   bookTitle= {FM 2009: Formal Methods}
  ,   conference= {International Symposium on Formal Methods}
  ,   series= {Lecture Notes in Computer Science}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4426_final-version.pdf}
  }
  

• Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig, Dennis Walter. The Importance of Being Formal.
  Proceedings of the First Workshop on Certification of Safety-Critical Software Controlled Systems, 2009. 238, p. 57-70. Elsevier B.V..
  AbstractPDF BibTeX

  This paper presents work in the context of the certification of a safety component for autonomous service robots, and investigates the potential advantages offered by formally modelling the domain knowledge, specification and implementation in a theorem prover in higher-order logic. This allows safety properties to be stated in an abstract manner close to textbook mathematics. The automatic proof checking alleviates correctness concerns, and provides a seamless development process from high-level safety requirements down to concrete implementation. Moreover, the formalisation can be checked for correctness automatically, and the certification review process can focus on the correctness of the specification and safety cases.

  @inproceedings{4425
  ,   author= {Udo Frese and Daniel Hausmann and Christoph L\"uth and Holger T\"aubig and Dennis Walter}
  ,   editor= {M. Huhn and H. Hungar}
  ,   title= {The Importance of Being Formal}
  ,   volume= {238}
  ,   pages= {57-70}
  ,   publisher= {Elsevier B.V.}
  ,   year= {2009}
  ,   bookTitle= {Proceedings of the First Workshop on Certification of Safety-Critical Software Controlled Systems}
  ,   conference= {International Workshop on Certification of Safety-Critical Software Controlled Systems}
  ,   keywords= {software certification; formal methods; robotics; safety; Isabelle}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4425_safecert08.pdf}
  }
  

• David Aspinall, Serge Autexier, Christoph Lüth, Marc Wagner. Towards Merging Plato and PGIP.
  Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers, 2009. Electronic Notes in Theoretical Computer Science 226, p. 3-21. Elsevier Science.
  AbstractPDF BibTeX

  The PGIP protocol is a standard, abstract interface protocol to connect theorem provers with user interfaces. Interaction in PGIP is based on ASCII-text input and a single focus point-of-control, which indicates a linear position in the input that has been checked thus far. This fits many interactive theorem provers whose interaction model stems from command-line interpreters. Plato, on the other hand, is a system with a new protocol tailored to transparently integrate theorem provers into text editors like TEXmacs that support semi-structured XML input files and multiple foci of attention. In this paper we extend the PGIP protocol and middleware broker to support the functionalities provided by Plato and beyond. More specifically, we extend PGIP (i) to support multiple foci in provers; (ii) to display semi-structured documents; (iii) to combine prover updates with user edits; (iv) to support context-sensitive service menus, and (v) to allow multiple displays. As well as supporting TEXmacs, the extended PGIP protocol in principle can support other editors such as OpenOffice, Word 2007 and graph viewers; we hope it will also provide guidance for extending provers to handle multiple foci.

  @inproceedings{4451
  ,   author= {David Aspinall and Serge Autexier and Christoph L\"uth and Marc Wagner}
  ,   title= {Towards Merging Plato and PGIP}
  ,   volume= {226}
  ,   pages= {3-21}
  ,   publisher= {Elsevier Science}
  ,   year= {2009}
  ,   bookTitle= {Proceedings of the 8th International Workshop on User Interfaces for Theorem Provers}
  ,   conference= {Workshop on User Interfaces for Theorem Provers}
  ,   series= {Electronic Notes in Theoretical Computer Science}
  ,   keywords= {Plato; Proof General; Mediator; Protocol; PGIP}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4451_paper-final-entcs.pdf}
  }
  

• Christoph Lüth. User Interfaces for Theorem Provers: Necessary Nuisanec or Unexplored Potential?.
  Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09), 2009. Electronic Communications of the EASST 23.
  AbstractPDF BibTeX

  This note considers the design of user interfaces for interactive theorem provers. The basic rules of interface design are reviewed, and their applicability to theorem provers is discussed, leading to considerations about the particular challenges of interface design for theorem provers. A short overview and classification of existing interfaces is given, followed by suggestions of possible future work in the area.

  @inproceedings{9432
  ,   author= {Christoph L\"uth}
  ,   title= {User Interfaces for Theorem Provers: Necessary Nuisanec or Unexplored Potential?}
  ,   volume= {23}
  ,   year= {2009}
  ,   bookTitle= {Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09)}
  ,   conference= {Workshop on Automated Verification of Critical Systems}
  ,   series= {Electronic Communications of the EASST}
  ,   linksMore= {https://journal.ub.tu-berlin.de/eceasst/article/view/322/305 and https://www.dfki.de/fileadmin/user_upload/import/9432_main-final.pdf}
  }
  

• David Aspinall, Ewen Denney, Christoph Lüth. A Tactic Language for Hiproofs.
  7th International Conference on Mathematical Knowledge Management (MKM 2007), 2008. Lecture Notes in Computer Science 5144, p. 339-354. Springer.
  AbstractPDF BibTeX

  We introduce and study a tactic language,Hitac, for constructing hierarchical proofs, known as hiproofs. The idea of hiproofs is to superimpose a labelled hierarchical nesting on an ordinary proof tree. The labels and nesting are used to describe the organisation of the proof, typically relating to its construction process. This can be useful for understanding and navigating the proof. Tactics in our language construct hiproof structure together with an underlying proof tree. We provide both a big-step and a small-step operational semantics for evaluating tactic expressions. The big-step semantics captures the intended meaning, whereas the small-step semantics hints at possible implementations and provides a unified notion of proof state. We prove that these notions are equivalent and construct valid proofs.

  @inproceedings{3843
  ,   author= {David Aspinall and Ewen Denney and Christoph L\"uth}
  ,   editor= {Serge Autexier and J. Campbell and J. Rubio}
  ,   title= {A Tactic Language for Hiproofs}
  ,   volume= {5144}
  ,   pages= {339-354}
  ,   publisher= {Springer}
  ,   year= {2008}
  ,   bookTitle= {7th International Conference on Mathematical Knowledge Management (MKM 2007)}
  ,   conference= {International Conference on Mathematical Knowledge Management}
  ,   series= {Lecture Notes in Computer Science}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/3843_mkm08.pdf}
  }
  

• Christoph Lüth, Udo Frese, Holger Täubig, Dennis Walter, Daniel Hausmann. SAMS: Sicherheitskomponente für Autonome Mobile Serviceroboter.
  Robotik 2008. Leistungsstand - Anwendungen - Visionen - Trends, 2008. VDI-Bericht 2012. VDI-Verlag.
  AbstractPDF BibTeX

  Ziel des Projektes SAMS ist die Entwicklung einer zulassungsfähigen Fahrwegsicherung für Serviceroboter und fahrerlose Transportsysteme (FTS), die mit einem zertifizierten Sicherheitslaserscanner die überwachte Sicherheitszone dynamisch dem Zustand des Fahrzeugs anpasst. Während dies für Forschungsprototypen Stand der Technik ist, konzentriert sich das Projekt SAMS auf eine zulassungsfähige Entwicklung], die durch ein TÜV-Gutachten nachgewiesen werden soll. Kernvorhaben ist dabei die formale mathematische Modellierung und der Korrektheitsbeweis der Implementierung.

  @inproceedings{3856
  ,   author= {Christoph L\"uth and Udo Frese and Holger T\"aubig and Dennis Walter and Daniel Hausmann}
  ,   title= {SAMS: Sicherheitskomponente f\"ur Autonome Mobile Serviceroboter}
  ,   volume= {2012}
  ,   publisher= {VDI-Verlag}
  ,   year= {2008}
  ,   bookTitle= {Robotik 2008. Leistungsstand - Anwendungen - Visionen - Trends}
  ,   conference= {VDI/VDE Fachtagung Robotik}
  ,   series= {VDI-Bericht}
  ,   keywords= {sams}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/3856_robotik2008.pdf}
  }
  

• Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig, Dennis Walter. Zertifizierung einer Sicherungskomponente mittels durchgängig formaler Modellierung.
  Software Engineering 2008 - Workshopband: Fachtagung des GI-Fachbereichs Softwaretechnik, 2008. Lecture Notes in Informatics P-122, p. 335-338. Gesellschaft für Informatik.
  AbstractPDF BibTeX

  Dieses Papier berichtet über Arbeiten im Rahmen des Projektes SAMS, in welchem eine Fahrwegsicherungskomponente für Serviceroboter und fahrerlose Transportsysteme entwickelt und ihre Software nach IEC 61508 zertifiziert wird. Neu ist hierbei der durchgehende Einsatz formaler Modellierung und Beweis als Mittel zur Zertifizierung, das es uns erlaubt, die erforderlichen Sicherheitsbedingungen sehr abstrakt mathematisch zu formulieren, und gleichzeitig den Bezug zur Implementierung bewiesen korrekt herzustellen. Indem wir die Grundlagen der Anwendungsdomäne (Geometrie und die Mechanik bewegter Objekte) in einem Theorembeweiser formalisieren, können wir die Sicherheitsanforderungen auf einer abstrakten, mathematischen Ebene formulieren. Diese sind dann wesentlich leichter zu validieren als implementationsnah formulierte Programmeigenschaften. Darüber hinaus modellieren wir die Implementierung innerhalb desselben formalen Rahmens. Dadurch erhalten wir einen nahtlosen Entwicklungsprozess mit einem klaren und beweisbar korrekten Übergang von den Sicherheitseigenschaften zu der Implementation. Wir glauben, dass diese Vorgehensweise für alle Sicherheitszertifikationen nützlich sein kann: die formale Modellierung erzwingt, dass alle Annahmen, die in den Sicherheitsanforderungen, der Implementation oder den Beweisen implizit enthalten sind, explizit gemacht werden, so dass sich der Zertifikationsprozess auf die Sicherheitsanforderungen konzentrieren kann, da die Korrektheitsbeweise automatisch geprüft werden können.

  @inproceedings{3857
  ,   author= {Udo Frese and Daniel Hausmann and Christoph L\"uth and Holger T\"aubig and Dennis Walter}
  ,   editor= {Walid Maalej and Bernd Br\"ugge}
  ,   title= {Zertifizierung einer Sicherungskomponente mittels durchg\"angig formaler Modellierung}
  ,   volume= {P-122}
  ,   pages= {335-338}
  ,   publisher= {Gesellschaft f\"ur Informatik}
  ,   year= {2008}
  ,   bookTitle= {Software Engineering 2008 - Workshopband: Fachtagung des GI-Fachbereichs Softwaretechnik}
  ,   conference= {GI-Fachtagungen}
  ,   series= {Lecture Notes in Informatics}
  ,   keywords= {sams}
  ,   isbn= {978-3-88579-216-1}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/3857_softzert08.pdf}
  }
  

• David Aspinall, Christoph Lüth, Daniel Winterstein. A Framework for Interactive Proof.
  6th International Conference on Mathematical Knowledge Management (MKM 2007), 2007. Lecture Notes in Artificial Intelligence 4573, p. 161-175. Springer.
  AbstractPDF BibTeX

  This paper introduces Proof General Kit, a framework for software components tailored to interactive proof development. The goal of the framework is to enable flexible environments for managing formal proofs across their life-cycle: creation, maintenance and exploitation. The framework connects together different kinds of component, exchanging messages using a common communication infrastructure and protocol called PGIP. The main channel connects provers to displays. Provers are the back-end interactive proof engines and displays are components for interacting with the user, allowing browsing or editing of proofs. At the core of the framework is a broker middleware component which manages proof-in-progress and mediates between components.

  @inproceedings{3893
  ,   author= {David Aspinall and Christoph L\"uth and Daniel Winterstein}
  ,   title= {A Framework for Interactive Proof}
  ,   volume= {4573}
  ,   pages= {161-175}
  ,   publisher= {Springer}
  ,   year= {2007}
  ,   bookTitle= {6th International Conference on Mathematical Knowledge Management (MKM 2007)}
  ,   conference= {International Conference on Mathematical Knowledge Management}
  ,   series= {Lecture Notes in Artificial Intelligence}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/3893_mkm07.pdf}
  }
  

• Bernd Krieg-Brückner, Antonio Krüger, M. Hoffmeister, Christoph Lüth. Kopplung von Zutrittskontrolle und Raumautomation - Eine Basis für die Interaktion mit einer intelligenten Umgebung.
  8. Fachtagung Gebäudesicherheit und Gebäudeautomation - Koexistenz oder Integration?, 2007. VDI Berichte 2005, p. 37-48. Springer.
  AbstractBibTeX

  Im BAALL sollen neu entwickelte AAL-Techniken erprobt und bis zur Alltagstauglichkeit hin evaluiert werden. Im Zent-rum steht die (natürlich-sprachliche) Interaktion der Nutzer des Rollstuhls ROLLAND oder der Gehhilfe INTELLIGENT-WALKER mit der intelligenten Umgebung (Steuerung von Raumautomation, intelligenten Möbeln, etc.); darauf auf-bauend sollen höhere Assistenzszenarien realisiert werden.

  @incollection{4454
  ,   author= {Bernd Krieg-Br\"uckner and Antonio Kr\"uger and M. Hoffmeister and Christoph L\"uth}
  ,   editor= {VDI-Gesellschaft}
  ,   title= {Kopplung von Zutrittskontrolle und Raumautomation - Eine Basis f\"ur die Interaktion mit einer intelligenten Umgebung}
  ,   volume= {2005}
  ,   pages= {37-48}
  ,   publisher= {Springer}
  ,   year= {2007}
  ,   bookTitle= {8. Fachtagung Geb\"audesicherheit und Geb\"audeautomation - Koexistenz oder Integration?}
  ,   series= {VDI Berichte}
  }
  

• David Aspinall, Christoph Lüth, Daniel Winterstein, Ahsan Fayyaz. Proof General in Eclipse.
  Eclipse Technology eXchange ETX'06, 2006. ACM Press.
  AbstractPDF BibTeX

  Interactive theorem proving is the art of constructing electronic proofs. Proof development, based around a proof script, has much in common with program development, based around a program text. Proof developers use rather primitive tools for developing and manipulating proof scripts at present. The Proof General project aims at to change this, by providing powerful generic tools and interfaces. The flagship tool is our Eclipse plugin, which brings the features of a industrial-strength IDE to theorem proving for the first time. In this paper we give an overview of the Eclipse plugin and its underlying architecture.

  @inproceedings{3892
  ,   author= {David Aspinall and Christoph L\"uth and Daniel Winterstein and Ahsan Fayyaz}
  ,   title= {Proof General in Eclipse}
  ,   publisher= {ACM Press}
  ,   year= {2006}
  ,   bookTitle= {Eclipse Technology eXchange ETX'06}
  ,   conference= {Eclipse Technology Exchange Workshop}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/3892_etx06.pdf}
  }
  

• Micheal Abbot, Neil Ghani, Christoph Lüth. Abstract Modularity.
  Rewriting Techniques and Applications (RTA'05), April 2005. Lecture Notes in Computer Science 3467, p. 46--60. Springer.
  AbstractPDF BibTeX

  Modular rewriting seeks criteria under which rewrite systems inherit properties from their smaller subsystems. This divide and conquer methodology is particularly useful for reasoning about large systems where other techniques fail to scale adequately. Research has typically focused on reasoning about the modularity of specific properties for specific ways of combining specific forms of rewriting. This paper is, we believe, the first to ask a much more general question. Namely, what can be said about modularity independently of the specific form of rewriting, combination and property at hand. A priori there is no reason to believe that anything can actually be said about modularity without reference to the specifics of the particular systems etc. However, this paper shows that, quite surprisingly, much can indeed be said.

  @inproceedings{Lueth:AbsMod
  ,   author= {Micheal Abbot and Neil Ghani and Christoph L\"uth}
  ,   title= {Abstract Modularity}
  ,   bookTitle= {Rewriting Techniques and Applications (RTA'05)}
  ,   editor= {J\"urgen Giesl}
  ,   publisher= {Springer}
  ,   series= {Lecture Notes in Computer Science}
  ,   volume= {3467}
  ,   year= {2005}
  ,   pages= {46--60}
  ,   month= {April}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/rta05.pdf}
  }
  

• Christoph Lüth, Markus Roggenbach, Lutz Schröder. CCC - The CASL Consistency Checker.
  17th International Workshop on Recent Trends in Algebraic Development Techniques (WADT 2004), 2005. Lecture Notes in Computer Science 3423, p. 94--105. Springer.
  AbstractPDF BibTeX

  We introduce the CASL Consistency Checker (CCC), a tool that supports consistency proofs in the algebraic specification language CASL. CCC is a faithful implementation of a previously described consistency calculus. Its system architecture combines flexibility with correctness ensured by encapsulation in a type system. CCC offers tactics, tactical combinators, forward and backward proof, and a number of specialised static checkers, as well as a connection to the CASL proof tool HOL-CASL to discharge proof obligations. We demonstrate the viability of CCC by an extended example taken from the CASL standard library of basic datatypes.

  @inproceedings{Lueth:WADT04a
  ,   author= {Christoph L\"uth and Markus Roggenbach and Lutz Schr\"oder}
  ,   title= {CCC - The CASL Consistency Checker}
  ,   year= {2005}
  ,   editor= {Jose Fiadeiro}
  ,   bookTitle= {17th International Workshop on Recent Trends in Algebraic Development Techniques (WADT 2004)}
  ,   publisher= {Springer}
  ,   series= {Lecture Notes in Computer Science}
  ,   volume= {3423}
  ,   pages= {94--105}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/wadt04a.pdf}
  }
  

• Lutz Schröder, Till Mossakowski, Christoph Lüth. Type class polymorphism in an institutional framework.
  17th International Workshop on Recent Trends in Algebraic Development Techniques (WADT 2004), 2005. Lecture Notes in Computer Science 3423, p. 234-- 248. Springer.
  AbstractPDF BibTeX

  Higher-order logic with ML-style type class polymorphism is widely used as a specification formalism. Its polymorphic entities (types, operators, axioms) can easily be equipped with a `naive' semantics defined in terms of collections of instances. However, this semantics has the unpleasant property that while model reduction preserves satisfaction of sentences, model expansion generally does not. In other words, unless further measures are taken, type class polymorphism fails to constitute a proper institution, being only a so-called rps preinstitution; this is unfortunate, as it means that one cannot use institution-independent or heterogeneous structuring languages, proof calculi, and tools with it. Here, we suggest to remedy this problem by modifying the notion of model to include information also about its potential future extensions. Our construction works at a high level of generality in the sense that it provides, for any preinstitution, an institution in which the original preinstitution can be represented. The semantics of polymorphism used in the specification language HasCASL makes use of this result. In fact, HasCASL's polymorphism is a special case of a general notion of polymorphism in institutions introduced here, and our construction leads to the right notion of semantic consequence when applied to this generic polymorphism. The appropriateness of the construction for other frameworks that share the same problem depends on methodological questions to be decided case by case. In particular, it turns out that our method is apparently unsuitable for observational logics, while it works well with abstract state machine formalisms such as state-based CASL.

  @inproceedings{Lueth:WADT04b
  ,   author= {Lutz Schr\"oder and Till Mossakowski and Christoph L\"uth}
  ,   title= {Type class polymorphism in an institutional framework}
  ,   year= {2005}
  ,   editor= {Jose Fiadeiro}
  ,   bookTitle= {17th International Workshop on Recent Trends in Algebraic Development Techniques (WADT 2004)}
  ,   publisher= {Springer}
  ,   series= {Lecture Notes in Computer Science}
  ,   volume= {3423}
  ,   pages= {234-- 248}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/wadt04b.pdf}
  }
  

• David Aspinall, Christoph Lüth, Burkhart Wolff. Assisted Proof Document Authoring.
  4th International Conference on Mathematical Knowledge Management (MKM 2005), 2005. Lecture Notes in Artificial Intelligence 3863, p. 65-80. Springer.
  AbstractPDF BibTeX

  Recently, significant advances have been made in formalised mathematical texts for large, demanding proofs. But although such large developments are possible, they still take an inordinate amount of effort and time, and there is a significant gap between the resulting formalised machine-checkable proof scripts and the corresponding human-readable mathematical texts. We present an authoring system for formal proof which addresses these concerns. It is based on a central document format which, in the tradition of literate programming, allows one to extract either a formal proof script or a human-readable document; the two may have differing structure and detail levels, but are developed together in a synchronised way. Additionally, we introduce ways to assist production of the central document, by allowing tools to contribute backflow to update and extend it. Our authoring system builds on the new PG Kit architecture for Proof General, bringing the extra advantage that it works in a uniform interface, generically across various interactive theorem provers.

  @inproceedings{4452
  ,   author= {David Aspinall and Christoph L\"uth and Burkhart Wolff}
  ,   editor= {Michael Kohlhase}
  ,   title= {Assisted Proof Document Authoring}
  ,   volume= {3863}
  ,   pages= {65-80}
  ,   publisher= {Springer}
  ,   year= {2005}
  ,   bookTitle= {4th International Conference on Mathematical Knowledge Management (MKM 2005)}
  ,   conference= {International Conference on Mathematical Knowledge Management}
  ,   series= {Lecture Notes in Artificial Intelligence}
  ,   isbn= {978-3-540-31430-1}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4452_mkm05.pdf}
  }
  

• Einar Broch Johnsen, Christoph Lüth. Theorem Reuse by Proof Term Transformation.
  International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2004), September 2004. Lecture Notes in Computer Science 3223, p. 152--167. Springer.
  AbstractPDF BibTeX

  Proof reuse addresses the issue of how proofs of theorems in a specific setting can be used to prove other theorems in different settings. This paper proposes an approach where theorems are generalised by abstracting their proofs from the original setting. The approach is based on a representation of proofs as logical framework proof terms, using the theorem prover Isabelle. The logical framework allows type-specific inference rules to be handled uniformly in the abstraction process and the prover's automated proof tactics may be used freely. This way, established results become more generally applicable; for example, theorems about a data type can be reapplied to other types. The paper also considers how to reapply such abstracted theorems, and suggests an approach based on mappings between operations and types, and on systematically exploiting the dependencies between theorems.

  @inproceedings{Lueth:TheoremReuse
  ,   author= {Einar Broch Johnsen and Christoph L\"uth}
  ,   title= {Theorem Reuse by Proof Term Transformation}
  ,   bookTitle= {International Conference on Theorem Proving in Higher-Order Logics (TPHOLs 2004)}
  ,   editor= {Konrad Slind and Annette Bunker and Ganesh Gopalakrishnan}
  ,   publisher= {Springer}
  ,   series= {Lecture Notes in Computer Science}
  ,   volume= {3223}
  ,   year= {2004}
  ,   pages= {152--167}
  ,   month= {September}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/tphols04.pdf}
  }
  

• David Aspinall, Christoph Lüth. Proof General meets IsaWin: Combining Text-Based and Graphical User Interfaces.
  5th International Workshop on User Interfaces for Theorem Provers (UITP'03), November 2004. Electronic Notes in Theoretical Computer Science 103, p. 3--26.
  AbstractPDF BibTeX

  We describe the design and prototype implementation of a combination of theorem prover interface technologies. On one side, we take from Proof General the idea of a prover-independent interaction language and its proposed implementation within the PG Kit middleware architecture. On the other side, we take from IsaWin a sophisticated graphical metaphor using direct manipulation for developing proofs. We believe that the resulting system will provide a powerful, robust and generic environment for developing proofs within interactive proof assistants that also opens the way for studying and implementing new mechanisms for managing interactive proof development.

  @inproceedings{AspinallLueth04
  ,   author= {David Aspinall and Christoph L\"uth}
  ,   title= {Proof General meets IsaWin: Combining Text-Based and Graphical User Interfaces}
  ,   bookTitle= {5th International Workshop on User Interfaces for Theorem Provers (UITP'03)}
  ,   series= {Electronic Notes in Theoretical Computer Science}
  ,   month= {November}
  ,   year= {2004}
  ,   volume= {103}
  ,   issue= {C}
  ,   pages= {3--26}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/uitp03.pdf}
  ,   linksMore= {http://www.sciencedirect.com/science/article/B75H1-4DN4HVV-2/2/39d1b3e85f828fde18ee7a35becf7958}
  }
  

• Bernd Krieg-Brückner, Arne Lindow, Christoph Lüth, Achim Mahnke, Georg Russell. Semantic Interrelation of Documents via an Ontology.
  DeLFI 2004, Tagungsband der 2. e-Learning Fachtagung Informatik, September 2004. Lecture Notes in Informatics P-52, p. 271--282. Gesellschaft für Informatik.
  AbstractPDF BibTeX

  This paper describes how to use an ontology for extensive semantic interrelation of documents in order to achieve sustainable development, i.e. continuous long-term usability of the contents. The ontology is structured via packages (corresponding to whole documents). Packages are related by import such that semantic interrelation becomes possible not only within a document but also between different documents. Coherence and consistency are enhanced by change management in a repository, including version control and configuration management. Semantic interrelation is realized by particular LATEX commands for the declaration and definition of classes, objects and relations, and references to them, such that they can be used in standard LATEX documents, in particular, with a new LATEX style for educational material (slides, handouts, annotated courses, assignments, and so on).

  @inproceedings{SemInter-DELFI04
  ,   author= {Bernd Krieg-Br\"uckner and Arne Lindow and Christoph L\"uth and Achim Mahnke and Georg Russell}
  ,   title= {Semantic Interrelation of Documents via an Ontology}
  ,   year= {2004}
  ,   month= {September}
  ,   editor= {Gregor Engels and Silke Seehusen}
  ,   bookTitle= {DeLFI 2004, Tagungsband der 2. e-Learning Fachtagung Informatik}
  ,   adress= {Paderborn, Germany}
  ,   publisher= {Gesellschaft f\"ur Informatik}
  ,   series= {Lecture Notes in Informatics}
  ,   volume= {P-52}
  ,   pages= {271--282}
  ,   isbn= {3-88579-381-4}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/delfi2004.pdf}
  }
  

• Bernd Krieg-Brückner, Dieter Hutter, Christoph Lüth, Erica Melis, Arnd Pötsch-Heffter, Markus Roggenbach, Jan-Georg Smaus, Martin Wirsing. Towards MultiMedia Instruction in Safe and Secure Systems.
  16th International Workshop on Recent Trends in Algebraic Development Techniques (WADT 2002), 2003. Lecture Notes in Computer Science 2755, p. 82-117. Springer.
  AbstractPDF BibTeX

  The aim of the MMiSS project is the construction of a multi-media Internet-based adaptive educational system. Its content will initially cover a curriculum in the area of Safe and Secure Systems. Traditional teaching materials (slides, handouts, annotated course material, assignments, and so on) are to be converted into a new hypermedia format, integrated with tool interactions for formally developing correct software; they will be suitable for learning on campus and distance learning, as well as interactive, supervised, or co-operative self-study. To ensure sustainable development, i.e. continuous long-term usability of the contents, coherence and consistency are especially emphasised, through extensive semantic linking of teaching elements and a particular version and configuration management, based on experience in formal software development and associated support tools.

  @inproceedings{1636
  ,   author= {Bernd Krieg-Br\"uckner and Dieter Hutter and Christoph L\"uth and Erica Melis and Arnd P\"otsch-Heffter and Markus Roggenbach and Jan-Georg Smaus and Martin Wirsing}
  ,   editor= {Martin Wirsing and Dirk Pattinson and Rolf Hennicker}
  ,   title= {Towards MultiMedia Instruction in Safe and Secure Systems}
  ,   volume= {2755}
  ,   pages= {82-117}
  ,   publisher= {Springer}
  ,   year= {2003}
  ,   bookTitle= {16th International Workshop on Recent Trends in Algebraic Development Techniques (WADT 2002)}
  ,   conference= {International Workshop on Algebraic Development Techniques}
  ,   series= {Lecture Notes in Computer Science}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/1636_wadt02.pdf}
  }
  

• Christoph Lüth, Neil Ghani. Composing Monads Using Coproducts.
  International Conference on Functional Programming (ICFP'02), September 2002. p. 133-- 144. ACM Press.
  AbstractPDF BibTeX

  Monads are a useful abstraction of computation, as they model diverse computational effects such as stateful computations, exceptions and I/O in a uniform manner. Their potential to provide both a modular semantics and a modular programming style was soon recognised. However, in general, monads proved difficult to compose and so research focused on special mechanisms for their composition such as distributive monads and monad transformers. We present a new approach to this problem which is general in that nearly all monads compose, mathematically elegant in using the standard categorical tools underpinning monads and computationally expressive in supporting a canonical recursion operator. In a nutshell, we propose that two monads should be composed by taking their coproduct. Although abstractly this is a simple idea, the actual construction of the coproduct of two monads is non-trivial. We outline this construction, show how to implement the coproduct within Haskell and demonstrate its usage with a few examples. We also discuss its relationship with other ways of combining monads, in particular distributive laws for monads and monad transformers.

  @inproceedings{Lueth:ICFP02
  ,   author= {Christoph L\"uth and Neil Ghani}
  ,   title= {Composing Monads Using Coproducts}
  ,   bookTitle= {International Conference on Functional Programming (ICFP'02)}
  ,   pages= {133-- 144}
  ,   year= {2002}
  ,   month= {September}
  ,   publisher= {ACM Press}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/icfp02.pdf}
  ,   linksMore= {http://www.informatik.uni-bremen.de/~cxl/papers/icfp02-src.tar.gz}
  }
  

• Christoph Lüth. Haskell in Space.
  Functional and Declarative Programming in Education (FDPE 2002), September 2002. p. 67-- 74. Technischer Bereicht 0210, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität Kiel.
  AbstractPDF BibTeX

  This short paper describes the final practical exercise in a functional programming course for second year computer science students at the University of Bremen. The exercise was to implement a small game involving a space ship in an asteroids belt, after the fashion of the classic Asteroids arcade game. We suggest that interactive graphics programs of this kind make good and entertaining programming exercises for functional programming courses.

  @inproceedings{Lueth:FDPE02
  ,   author= {Christoph L\"uth}
  ,   title= {Haskell in Space}
  ,   bookTitle= {Functional and Declarative Programming in Education (FDPE 2002)}
  ,   pages= {67-- 74}
  ,   year= {2002}
  ,   editor= {Micheal Hanus, Shriram Krishnamurthi, Simon Thompson}
  ,   month= {September}
  ,   publisher= {Technischer Bereicht 0210, Institut f\"ur Informatik und Praktische Mathematik, Christian-Albrechts-Universit\"at Kiel}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/fdpe02.pdf}
  }
  

• Ghani, Neil, Christoph Lüth, Federico de Marchi. Coalgebraic Approaches to Algebraic Terms.
  Fixed Points in Computer Science, June 2002. BRICS Notes Series NS-02-2, p. 6-- 8.
  AbstractPDF BibTeX

  Algebraic systems of equations define functions using recursion where parameter passing is permitted. This generalises the notion of a rational system of equations where parameter passing is prohibited. It has been known for some time that algebraic systems in Greibach Normal Form have unique solutions. This paper presents a categorical approach to algebraic systems of equations which generalises the traditional approach in two ways i) we define algebraic equations for locally finitely presentable categories rather than just Set; and ii) we define algebraic equations to allow right-hand sides which need not consist of finite terms. We show these generalised algebraic systems of equations have unique solutions by replacing the traditional metric-theoretic arguments with coalgebraic arguments.

  @inproceedings{Lueth:fics02
  ,   author= {Ghani, Neil and Christoph L\"uth and Federico de Marchi}
  ,   title= {Coalgebraic Approaches to Algebraic Terms}
  ,   bookTitle= {Fixed Points in Computer Science}
  ,   pages= {6-- 8}
  ,   year= {2002}
  ,   editor= {Zoltan 'Esik and Anna Ing'olfsd'ottir}
  ,   series= {BRICS Notes Series NS-02-2}
  ,   month= {June}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/fics02.pdf}
  }
  

• Christoph Lüth, Neil Ghani. Monads and Modularity.
  4th International Workshop on Frontiers of Combining Systems (FroCos 2002), Santa Margherita Ligure, Italy, April 2002. Lecture Notes in Artificial Intelligence, p. 18--32. Springer.
  AbstractPDF BibTeX

  This paper argues that the core of modularity problems is an understanding of how individual components of a large system interact with each other, and that this interaction can be described by a layer structure. We propose a uniform treatment of layers based upon the concept of a monad. The combination of different systems can be described by the coproduct of monads. Concretely, we give a construction of the coproduct of two monads and show how the layer structure in the coproduct monad can be used to analyse layer structures in three different application areas, namely term rewriting, denotational semantics and functional programming.

  @inproceedings{Lueth:FroCoS02
  ,   author= {Christoph L\"uth and Neil Ghani}
  ,   title= {Monads and Modularity}
  ,   pages= {18--32}
  ,   editor= {Alessandro Armando}
  ,   bookTitle= {4th International Workshop on Frontiers of Combining Systems (FroCos 2002)}
  ,   series= {Lecture Notes in Artificial Intelligence}
  ,   number= {2309}
  ,   month= {April}
  ,   year= {2002}
  ,   address= {Santa Margherita Ligure, Italy}
  ,   publisher= {Springer}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/frocos02.pdf}
  }
  

• Neil Ghani, Christoph Luth, Federico De Marchi. Coalgebraic Monads.
  5th International Workshop on Coalgebraic Methods in Computer Science (CMCS'02), Grenoble, France, April 2002. Electronic Notes in Theoretical Computer Science 65. Elsevier.
  AbstractPDF BibTeX

  This paper introduces coalgebraic monads as a unified model of term algebras covering fundamental examples such as initial algebras, final coalgebras, rational terms and term graphs. We develop a general method for obtaining finitary coalgebraic monads which allows us to generalise the notion of rational term and term graph to categories other than Set. As an application we sketch part of the correctness of the the term graph implementation of functional programming languages.

  @inproceedings{Lueth:CMCS02
  ,   author= {Neil Ghani and Christoph Luth and Federico De Marchi}
  ,   title= {Coalgebraic Monads}
  ,   bookTitle= {5th International Workshop on Coalgebraic Methods in Computer Science (CMCS'02)}
  ,   series= {Electronic Notes in Theoretical Computer Science}
  ,   volume= {65}
  ,   issue= {1}
  ,   publisher= {Elsevier}
  ,   editor= {Lawrence S. Moss}
  ,   year= {2002}
  ,   month= {April}
  ,   address= {Grenoble, France}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/cmcs02.pdf}
  }
  

• Neil Ghani, Christoph Lüth, Federico de Marchi, John Power. Algebras, Coalgebras, Monads and Comonads.
  4th International Workshop on Coalgebraic Methods in Computer Science (CMCS'01), Genoa, Italy, April 2001. Electronic Notes in Theoretical Computer Science 44.
  AbstractPDF BibTeX

  Whilst the relationship between initial algebras and monads is well-understood, the relationship between final coalgebras and comonads is less well explored. This paper shows that the problem is more subtle and that final coalgebras can just as easily form monads as comonads and dually, that initial algebras form both monads and comonads. In developing these theories we strive to provide them with an associated notion of syntax. In the case of initial algebras and monads this corresponds to the standard notion of algebraic theories consisting of signatures and equations: models of such algebraic theories are precisely the algebras of the representing monad. We attempt to emulate this result for the coalgebraic case by defining a notion cosignature and coequation and then proving the models of this syntax are precisely the coalgebras of the representing comonad.

  @inproceedings{Lueth:CMCS01
  ,   author= {Neil Ghani and Christoph L\"uth and Federico de Marchi and John Power}
  ,   title= {Algebras, Coalgebras, Monads and Comonads}
  ,   bookTitle= {4th International Workshop on Coalgebraic Methods in Computer Science (CMCS'01)}
  ,   series= {Electronic Notes in Theoretical Computer Science}
  ,   year= {2001}
  ,   month= {April}
  ,   address= {Genoa, Italy}
  ,   editor= {U. Montanari}
  ,   volume= {44}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/cmcs01.pdf}
  ,   moreLinks= {https://www.sciencedirect.com/science/article/pii/S1571066104809058}
  }
  

• Christoph Lüth, Burkhardt Wolff. TAS --- A Generic Window Inference System.
  Theorem Proving in Higher Order Logics: 13th International Conference (TPHOLs 2000), Portland, Oregon, August 2000. Lecture Notes in Computer Science 1869, p. 405--422. Springer Verlag.
  AbstractPDF BibTeX

  This paper presents work on technology for transformational proof and program development, as used by window inference calculi and transformation systems. The calculi are characterised by a certain class of theorems in the underlying logic. Our transformation system TAS compiles these rules to concrete deduction support, complete with a graphical user interface with command-language-free user interaction by gestures like drag&drop and proof-by-pointing, and a development management for transformational proofs. It is generic in the sense that it is completely independent of the particular window inference or transformational calculus, and can be instantiated to many different ones; three such instantiations are presented in the paper.

  @inproceedings{Lueth:TPHOLs00
  ,   author= {Christoph L\"uth and Burkhardt Wolff}
  ,   title= {TAS --- A Generic Window Inference System}
  ,   pages= {405--422}
  ,   editor= {J. Harrison and M. Aagaard}
  ,   bookTitle= {Theorem Proving in Higher Order Logics: 13th International Conference (TPHOLs 2000)}
  ,   series= {Lecture Notes in Computer Science}
  ,   publisher= {Springer Verlag}
  ,   volume= {1869}
  ,   year= {2000}
  ,   month= {August}
  ,   address= {Portland, Oregon}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/tphols00.pdf}
  }
  

• Christoph Lüth, Burkhardt Wolff. More about TAS and IsaWin: Tools for Formal Program Development.
  Fundamental Approaches to Software Engineering (FASE 2000). Joint European Conferences on Theory and Practice of Software (ETAPS 2000), Berlin, Germany, March 2000. Lecture Notes in Computer Science 1783, p. 367-- 370. Springer Verlag.
  AbstractPDF BibTeX

  We present a family of tools for program development and verification, comprising the transformation system TAS and the theorem proving interface IsaWin. Both are based on the theorem prover Isabelle , which is used as a generic logical framework here. A graphical user interface, based on the principle of direct manipulation, allows the user to interact with the tool without having to concern himself with the details of the representation within the theorem prover, leaving him to concentrate on the main design decisions of program development or theorem proving.

  @inproceedings{Lueth:ETAPS00
  ,   author= {Christoph L\"uth and Burkhardt Wolff}
  ,   title= {More about TAS and IsaWin: Tools for Formal Program Development}
  ,   pages= {367-- 370}
  ,   editor= {T. Maibaum}
  ,   bookTitle= {Fundamental Approaches to Software Engineering (FASE 2000). Joint European Conferences on Theory and Practice of Software (ETAPS 2000)}
  ,   series= {Lecture Notes in Computer Science}
  ,   publisher= {Springer Verlag}
  ,   volume= {1783}
  ,   year= {2000}
  ,   month= {March}
  ,   address= {Berlin, Germany}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/fase00.pdf}
  }
  

• Christoph Lüth, Haykal Tej, Kolyang, Bernd Krieg-Brückner. TAS and IsaWin: Tools for Transformational Program Developkment and Theorem Proving.
  Fundamental Approaches to Software Engineering (FASE'99). Joint European Conferences on Theory and Practice of Software (ETAPS'99), Amsterdam, The Netherlands, March 1999. Lecture Notes in Computer Science 1577, p. 239-- 243. Springer-Verlag.
  AbstractBibTeX

  We present two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle. Their distinguishing features are a graphical user interface based on the principle of direct manipulation, and a generic, open system design which allows the development of a family of tools for different formal methods on a sound logical basis with a uniform appearance. The aim of these tools is to provide a user-friendly framework for formal program development, supported by a powerful theorem prover, and generic over the actual formal method employed. By embedding a formal method into the theorem prover Isabelle, instantiating the generic graphical user interface, and adding customised proof support, we obtain a tool for that formal method which hides the details of the encoding; we call this an encapsulation of the formal method.

  @inproceedings{Lueth:ETAPS99
  ,   author= {Christoph L\"uth and Haykal Tej and Kolyang and Bernd Krieg-Br\"uckner}
  ,   title= {TAS and IsaWin: Tools for Transformational Program Developkment and Theorem Proving}
  ,   pages= {239-- 243}
  ,   editor= {J.-P. Finance}
  ,   bookTitle= {Fundamental Approaches to Software Engineering (FASE'99). Joint European Conferences on Theory and Practice of Software (ETAPS'99)}
  ,   series= {Lecture Notes in Computer Science}
  ,   publisher= {Springer-Verlag}
  ,   volume= {1577}
  ,   year= {1999}
  ,   month= {March}
  ,   address= {Amsterdam, The Netherlands}
  ,   link= {http://www.informatik.uni-bremen.de/~cxl/papers/fase99.pdf}
  }
  

• Christoph Lüth, Einar W. Karlsen, Kolyang, Stefan Westmeier, Burkhardt Wolff. Tool Integration in the UniForM Workbench.
  R. Berghammer, Y. Lakhnech (eds): International Workshop on Tool Support for System Specification, Development, and Verification, Malente, Germany, June 1999. Advances in Computing Science, p. 160--173. Springer-Verlag Wien New York.
  AbstractPDF BibTeX

  The UniForM-Workbench is an open tool integration environment providing type-safe communication, a toolkit for graphical user interfaces, version management and configuration management. It is specifically geared towards formal methods and based on the encoding of formal methods into the theorem prover Isabelle. The UniForM-Workbench thus tackles both the technical and the semantical problems arising when integrating tools for formal methods.

  @inproceedings{Lueth:Tools98
  ,   author= {Christoph L\"uth and Einar W. Karlsen and Kolyang and Stefan Westmeier and Burkhardt Wolff}
  ,   title= {Tool Integration in the UniForM Workbench}
  ,   bookTitle= {International Workshop on Tool Support for System Specification, Development, and Verification}
  ,   editors= {R. Berghammer and Y. Lakhnech}
  ,   pages= {160--173}
  ,   year= {1999}
  ,   month= {June}
  ,   address= {Malente, Germany}
  ,   publisher= {Springer-Verlag Wien New York}
  ,   series= {Advances in Computing Science}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/tools98.pdf}
  }
  

• Christoph Lüth, Einar W. Karlsen, Kolyang, Stefan Westmeier, Burkhardt Wolff. HOL-Z in the UniForM-Workbench -- A Case Study in Tool Integration for Z.
  11th International Conference of Z Users (ZUM'98), Berlin, September 1998. Lecture Notes in Computer Science 1493, p. 116--134. Springer Verlag.
  AbstractPDF BibTeX

  The UniForM-Workbench is an open tool-integration environment providing type-safe communication, a toolkit for graphical user-interfaces, version management and configuration management. We demonstrate how to integrate several tools for the Z specification language into the workbench, obtaining an instantiation of the workbench suited as a software development environment for Z. In the core of the setting, we use the encoding HOL-Z of Z into Isabelle as semantic foundation and for formal reasoning with Z specifications. In addition to this, external tools like editors and small utilities are integrated, showing the integration of both self-developed and externally developed tools. The resulting prototype demonstrates the viability of our approach to combine public domain tools into a generic software development environment using a strongly typed functional language.

  @inproceedings{Lueth:zum98
  ,   title= {HOL-Z in the UniForM-Workbench -- A Case Study in Tool Integration for Z}
  ,   author= {Christoph L\"uth and Einar W. Karlsen and Kolyang and Stefan Westmeier and Burkhardt Wolff}
  ,   pages= {116--134}
  ,   editor= {J. P. Bowen and A. Fett and M. G. Hinchey}
  ,   bookTitle= {11th International Conference of Z Users (ZUM'98)}
  ,   publisher= {Springer Verlag}
  ,   series= {Lecture Notes in Computer Science}
  ,   volume= {1493}
  ,   year= {1998}
  ,   month= {September}
  ,   address= {Berlin}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/zum98.pdf}
  }
  

• Kolyang, Christoph Lüth, Thomas Meier, Burkhardt Wolff. Generic Interfaces for Transformation Systems and Interactive Theorem Provers.
  International Workshop on Tool Support for Validation and Verfication, Bremen, Germany, 1998. BISS Monographs 1. Shaker Verlag.
  AbstractPDF BibTeX

  We present a new approach to implement graphical user interfaces (GUIs) for theorem provers and formal development support tools. A typed interface between Standard ML and Tcl/Tk provides the foundations, upon which a generic GUI is built. Besides the advantage of type safeness, this technique yields access to the full power of the modularisation concepts of Standard ML: the generic GUI is a functor (a parametric module), which instantiated with a particular application yields a GUI for this application. We present a prototypical implementation with two instantiations: an interface to Isabelle itself and a system for transformational program development based on Isabelle.

  @inproceedings{Lueth:Tools96
  ,   author= {Kolyang and Christoph L\"uth and Thomas Meier and Burkhardt Wolff}
  ,   title= {Generic Interfaces for Transformation Systems and Interactive Theorem Provers}
  ,   editor= {B. Berghammer and B. Buth and J. Peleska}
  ,   series= {BISS Monographs}
  ,   volume= {1}
  ,   bookTitle= {International Workshop on Tool Support for Validation and Verfication}
  ,   year= {1998}
  ,   address= {Bremen, Germany}
  ,   publisher= {Shaker Verlag}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/tools96.pdf}
  }
  

• Kolyang, Christoph Lüth, Thomas Meier, Burkhardt Wolff. TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving.
  TAPSOFT 97: Theory and Practice of Software Development, Lille, France, April 1997. Lecture Notes in Computer Science, p. 855-- 859. Springer Verlag.
  AbstractPDF BibTeX

  We present a new approach to the implementation of graphical user interfaces (GUIs) for formal program development systems like transformation systems or interactive theorem provers. Its distinguishing feature is a generic, open system design which allows the development of a family of tools for different formal methods on a sound logical basis with a uniform appearance.

  @inproceedings{Lueth:Tapsoft97
  ,   author= {Kolyang and Christoph L\"uth and Thomas Meier and Burkhardt Wolff}
  ,   title= {TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving}
  ,   editor= {M. Bidoit and M. Dauchet}
  ,   volme= {1214}
  ,   series= {Lecture Notes in Computer Science}
  ,   pages= {855-- 859}
  ,   bookTitle= {TAPSOFT 97: Theory and Practice of Software Development}
  ,   year= {1997}
  ,   publisher= {Springer Verlag}
  ,   address= {Lille, France}
  ,   month= {April}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/tapsoft97.pdf}
  }
  

• Christoph Lüth, Neil Ghani. Monads and Modular Term Rewriting.
  Category Theory and Computer Science, Santa Margherita Ligure, Italy, September 1997. Lecture Notes in Computer Science 1290, p. 69-- 86. Springer Verlag.
  AbstractPDF BibTeX

  Monads can be used to model term rewriting systems by generalising the well-known equivalence between universal algebra and monads on the category Set. In earlier work, the usefulness of this semantics was demonstrated by giving a purely categorical proof of the modularity of confluence for the disjoint union of term rewriting systems (Toyama's theorem). This paper provides further support for the use of monads in term rewriting by giving a categorical proof of the most general theorem concerning the modularity of strong normalisation. In the process, we improve upon some technical aspects of the earlier work.

  @inproceedings{Lueth:CTCS97
  ,   author= {Christoph L\"uth and Neil Ghani}
  ,   title= {Monads and Modular Term Rewriting}
  ,   editor= {E. Moggi and G. Rosolini}
  ,   volume= {1290}
  ,   series= {Lecture Notes in Computer Science}
  ,   pages= {69-- 86}
  ,   bookTitle= {Category Theory and Computer Science}
  ,   address= {Santa Margherita Ligure, Italy}
  ,   year= {1997}
  ,   publisher= {Springer Verlag}
  ,   month= {September}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/ctcs97.pdf}
  }
  

• Christoph Lüth. Transformational Program Development in the UniForM Workbench..
  Selected papers from the 8th Nordic Workshop on Programming Theory, December 1996. Oslo University.
  AbstractPDF BibTeX

  In this paper, the modelling of transformational program development inside a tactical theorem prover is described, together with a systematic way of building graphical user interfaces for applications based on a tactical prover. Combined with logical embeddings of formal methods into the prover, this yields a unifying framework for tool-supported formal program development. The work described here uses the theorem prover Isabelle, but is applicable to other tactical theorem provers as well.

  @inproceedings{Lueth:nwpt8
  ,   author= {Christoph L\"uth}
  ,   title= {Transformational Program Development in the UniForM Workbench.}
  ,   editor= {M. Haveraan and O. Owe}
  ,   bookTitle= {Selected papers from the 8th Nordic Workshop on Programming Theory}
  ,   year= {1996}
  ,   publisher= {Oslo University}
  ,   month= {December}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/nwpt96.pdf}
  }
  

• Kolyang, Christoph Lüth, Thomas Meier, Burkhardt Wolff. Generating Graphical User-Interfaces in a Functional Setting.
  User Interfaces for Theorem Provers (UITP '96), 1996. Technical Report, p. 59-- 66. University of York.
  AbstractPDF BibTeX

  We present a new approach to implementing graphical user interfaces (GUIs) for theorem provers and applications using theorem provers. A typed interface to Standard ML from Tcl/Tk provides the foundations upon which a generic user interface is built. Besides the advantage of type safeness, this technique yields access to the full power of the modularization concepts of Standard ML. It leads to a generic GUI, which instantiated with a particular application yields a GUI for this application. We present a prototypical implementation with two instantiations: an interface to Isabelle itself and a system for transformational program development based on Isabelle.

  @inproceedings{Lueth:UITP96
  ,   author= {Kolyang and Christoph L\"uth and Thomas Meier and Burkhardt Wolff}
  ,   bookTitle= {User Interfaces for Theorem Provers (UITP '96)}
  ,   editor= {N. Merriam}
  ,   pages= {59-- 66}
  ,   publisher= {University of York}
  ,   series= {Technical Report}
  ,   title= {Generating Graphical User-Interfaces in a Functional Setting}
  ,   year= {1996}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/uitp96.pdf}
  ,   moreLinks= {http://dcpu1.cs.york.ac.uk:6666/~nam/uitp/proceedings.html}
  }
  

• Christoph Lüth. Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem.
  7th International Conference on Rewriting Techniques and Applications (RTA-96), New Brunswick, USA, July 1996. Lecture Notes in Computer Science 1103, p. 261-- 275. Springer Verlag.
  AbstractPDF BibTeX

  This article proposes a compositional semantics for term rewriting systems, i.e. a semantics preserving structuring operations such as the disjoint union. The semantics is based on the categorical construct of a monad, adapting the treatment of universal algebra in category theory to term rewriting systems. As an example, the preservation of confluence under the disjoint union of two term rewriting systems is shown, obtaining an algebraic proof of Toyama's theorem, generalised slightly to term rewriting systems introducing variables on the right-hand side of the rules.

  @inproceedings{Lueth:RTA96
  ,   author= {Christoph L\"uth}
  ,   title= {Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem}
  ,   editor= {H. Ganzinger}
  ,   volume= {1103}
  ,   series= {Lecture Notes in Computer Science}
  ,   pages= {261-- 275}
  ,   bookTitle= {7th International Conference on Rewriting Techniques and Applications (RTA-96)}
  ,   address= {New Brunswick, USA}
  ,   year= {1996}
  ,   publisher= {Springer Verlag}
  ,   month= {July}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/rta96.pdf}
  }
  

Workshops, Technical Reports and Theses

• Iris Pigeot, Frank Oliver Glöckner, Antje Boetius, Andreas Breiter, Nicolas Dittert, Rainer Fechte-Heinen, Jutta Günther, Horst Hahn, Jan-Ocko Heuer, Betina Hollstein, Elisabeth Huber, Lutz Mädler, Rolf Drechsler, Guido Prause, Norbert Riefler, Norman Sieroka, Tanja Hörner, Derk Hergen Schönfeld, Lena Steinmann, Björn Oliver Schmidt, Florian Cordes, Frank Kirchner, Christoph Lüth. Etablierung eines kooperativen Forschungsdatenmanagements in der U Bremen Research Alliance.
  2021.
  AbstractPDF BibTeX

  Die U Bremen Research Alliance ist Kernbereich der Bremer Wissenschaft. Sie steht für Kooperation auf den Ebenen Forschung, wissenschaftlicher Nachwuchs, Rekrutierung und Infrastruktur. Um kooperative zukunftsorientierte Wissenschaft zu stärken, verfolgt sie gemeinschaftlich die Schaffung eines abgestimmten Raumes für Innovation, Infrastruktur und Forschung. Die Bereiche Forschungsdatenmanagement, Data Science und Digitalisierung bilden einen Schwerpunkt der Arbeit der Mitglieder der U Bremen Research Alliance. Beispiele dieser Entwicklung sind der Bremer Leibniz-WissenschaftsCampus „Digital Public Health“, die Gründung des Data Science Centers (DSC) an der Universität Bremen, der Aufbau der interdisziplinär und interorganisational getragenen Doktorand*innenausbildung „Data Train – Training in Research Data Management and Data Science“ und die aktive Beteiligung der Mitglieder an vier der neun im Juni 2020 ausgewählten Vorhaben zum Aufbau einer Nationalen Forschungsdateninfrastruktur (NFDI). Bremen ist damit im bundesweiten Vergleich einer der erfolgreichsten NFDI-Standorte. Dieses Whitepaper skizziert den aktuellen Status sowie Handlungsfelder für die disziplinübergreifende Etablierung eines kooperativen Forschungsdatenmanagements in der U Bremen Research Alliance.

  @misc{11722
  ,   author= {Iris Pigeot and Frank Oliver Gl\"ockner and Antje Boetius and Andreas Breiter and Nicolas Dittert and Rainer Fechte-Heinen and Jutta G\"unther and Horst Hahn and Jan-Ocko Heuer and Betina Hollstein and Elisabeth Huber and Lutz M\"adler and Rolf Drechsler and Guido Prause and Norbert Riefler and Norman Sieroka and Tanja H\"orner and Derk Hergen Sch\"onfeld and Lena Steinmann and Bj\"orn Oliver Schmidt and Florian Cordes and Frank Kirchner and Christoph L\"uth}
  ,   title= {Etablierung eines kooperativen Forschungsdatenmanagements in der U Bremen Research Alliance}
  ,   publisher= {Zenodo}
  ,   year= {2021}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/11722_20210719_Whitepaper Etablierung eines kooperativen Forschungsdatenmanagements in der U Bremen Research Alliance 2021.pdf and https://doi.org/10.5281/zenodo.4775371}
  }
  

• Christoph Lüth, Rolf Drechsler. Assistenzsysteme der Zukunft – Nutzen und Potenzial künstlicher Intelligenz.
  2019.
  BibTeX

  @inbook{10672
  ,   author= {Christoph L\"uth and Rolf Drechsler}
  ,   title= {Assistenzsysteme der Zukunft – Nutzen und Potenzial k\"unstlicher Intelligenz}
  ,   pages= {42-47}
  ,   publisher= {Kellner}
  ,   year= {2019}
  ,   bookTitle= {Brauchen wir eine neue Staatskunst?}
  ,   bookAuthor= {Henning L\"uhr}
  }
  

• Christoph Lüth, Cezary Kaliszyk (eds). Proceedings 10th International Workshop On User Interfaces for Theorem Provers.
  Electronic Proceedings in Theoretical Computer Science 118, 2013, www.eptcs.org.
  AbstractBibTeX

  This EPTCS volume collects the post-proceedings of the 10th International Workshop On User Interfaces for Theorem Provers (UITP 2012), held as part of the Conferences on Intelligent Computer Mathematics (CICM 2012) in Bremen on July 11th 2012. The UITP workshop series aims at bringing together reasearchers interested in designing, developing and evaluating interfaces for interactive proof systems, such as theorem provers, formal method tools, and other tools manipulating and presenting mathematical formulae. Started in 1995, it can look back on seventeen years of history by now. The papers in the present volume give a good indication of the range of questions currently addressed in the UITP community; this ranges from interface design (Windsteiger; Dunchev et al) to using technologies such as machine learning to assist the user (Komendantskaya et al). The web features prominently (Tankink), and new technology necessitates changes right down to the very basic modes of interaction (Wenzel) - the old REPL (read, evaluate, print, loop) mode of interaction can not take advantage of modern technology, such as the web and multi-core machines.

  @proceedings{6945
  ,   editor= {Christoph L\"uth and Cezary Kaliszyk}
  ,   title= {Proceedings 10th International Workshop On User Interfaces for Theorem Provers}
  ,   volume= {118}
  ,   publisher= {www.eptcs.org}
  ,   year= {2013}
  ,   conference= {Workshop on User Interfaces for Theorem Provers}
  ,   series= {Electronic Proceedings in Theoretical Computer Science}
  ,   linksMore= {http:// and http://dx.doi.org/10.4204/EPTCS.118}
  }
  

• Christoph Lüth. Schlussbericht des Projektes SAMS.
  DFKI Research Reports 10-01, Deutsches Forschungszentrum für Künstliche Intelligenz, 2010.
  AbstractPDF BibTeX

  Im Projekt SAMS (Sicherungskomponente für Autonome Mobile Serviceroboter) ist eine Komponente zur Berechnung von Schutzfeldern in Abhängigkeit von der Geschwindigkeit und dem Lenkwinkel eines sich bewegenden autonomen Fahrzeugs oder Serviceroboters entwickelt, implementiert, und für den Einsatz bis zu einem Sicherheitslevel (SIL) 3 geeignet zertifiziert worden. Das Schutzfeld überdeckt die beim Bremsen mit der momentanen Geschwindigkeit bis zum Stillstand überstrichene Fläche zuzüglich normativer Sicherheitszuschläge. Durch die Überwachung dieser Fläche mit einem Laserscanner kann die Sicherheit gegen Kollisionen mit statischen Hindernissen garantiert werden. Die Ergebnisse des Projektes sind zusammengefasst (i) die Entwicklung eines einfach konfigurierbaren, konservativen Bremsmodells für autonome Fahrzeuge und mobile Serviceroboter, (ii) ein als Sicherheitsfunktion nach der Norm IEC 61508:3 bis zu SIL 3 zertifizierter Algorithmus zur Berechnung von Schutzfeldern, und (iii) eine Verifikationsumgebung, welche zur Spezifikation und Verifikation von MISRA-C-Software gemäß IEC 61508:3 bis zu SIL 3 verwendet werden kann. Die Normenkonformität wurde durch den TÜV Süd schriftlich in letters of conformance bestätigt. Kern der Zertifizierung ist die formale mathematische Modellierung und der Korrektheitsbeweis der Implementierung mit dem computergestützten Theorembweiser Isabelle. Die entwickelten Techniken zur Verifikation algorithmisch orientierter Programme sind nicht auf die konkrete Anwendungsdomäne beschränkt, und für weitere Anwendungen einsetzbar.

  @techreport{4975
  ,   author= {Christoph L\"uth}
  ,   title= {Schlussbericht des Projektes SAMS}
  ,   volume= {10-01}
  ,   pages= {183}
  ,   year= {2010}
  ,   institution= {Deutsches Forschungszentrum f\"ur K\"unstliche Intelligenz}
  ,   series= {DFKI Research Reports}
  ,   linksMore= {https://www.dfki.de/fileadmin/user_upload/import/4975_dfki-rr-10-01.pdf}
  }
  

• Christoph Lüth. Formal Software Development: From Foundations to Tools.
  Habilitation thesis, Universität Bremen, 2005.
  AbstractPDF BibTeX

  This expose gives an overview of the author's contributions to the area of formal software development. These range from foundational issues dealing with abstract models of computation to practical engineering issues concerned with tool integration and user interface design. We can distinguish three lines of work: Firstly, there is foundational work, centred around categorical models of rewriting. A new semantics for rewriting has been developed, which abstracts over the concrete term structure while still being able to express key concepts such as variable, layer and substitution. It is based on the concept of a monad, which is well-known in category theory to model algebraic theories. We have generalised this treatment to term rewriting systems, infinitary terms, term graphs, and other forms of rewriting. The semantics finds applications in functional programming, where monads are used to model computational features such as state, exceptions and I/O, and modularity proofs, where the layer structure becomes central. Secondly, we are concerned with formal proof and development, where we understand `formal' as in formal logic (i.e. modelled inside a theorem prover.) The main contributions here are techniques for systematic generalisation of developments and proofs, called abstraction for reuse. We have developed abstraction procedures for any logical framework, and implemented them in Isabelle, combining proof term transformation known from type theory with tactical theorem proving. We have further shown how to model transformational development in-the-small in the TAS system by modelling window inferencing in Isabelle, and model development in-the-large by theory morphisms implemented via proof term transformation. Thirdly, we turn to tool development. We discuss suitable system architectures to implement formal methods tools, or integrate existing tools into a common framework. We consider user interfaces, introducing the design of a graphical user interface for the transformational development system TAS based on principles of direct manipulation, and showing how to combine the graphical user interface with a textual one based on the popular Emacs editor.

  @booklet{Lueth:Habilitation
  ,   author= {Christoph L\"uth}
  ,   title= {Formal Software Development: From Foundations to Tools}
  ,   howpublished= {Habilitation thesis, Universit\"at Bremen}
  ,   year= {2005}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/habil/thesis.pdf}
  ,   moreLinks= {http://www.informatik.uni-bremen.de/~cxl/habil/}
  }
  

• Dieter Hutter, David Basin, Christoph Lüth, Peter Lindsay. Workshop on Evolutionary Formal Software Development.
  2002.
  BibTeX

  @booklet{1630
  ,   author= {Dieter Hutter and David Basin and Christoph L\"uth and Peter Lindsay}
  ,   title= {Workshop on Evolutionary Formal Software Development}
  ,   year= {2002}
  }
  

• Neil Ghani, Christoph Lüth, Stefan Kahrs. Rewriting the Conditions in Conditional Rewriting.
  Technical report 2000/20, Dept. Mathematics and Computer Science, University of Leicester, 2000.
  AbstractPDF BibTeX

  Category theory has been used to provide a semantics for term rewriting systems at an intermediate level of abstraction between the actual syntax and the relational model. Recently we have developed a semantics for TRSs using monads which generalises the equivalence between algebraic theories and finitary monads on the category Sets. This semantics underpins the recent categorical proofs of state-of-the-art results in modular rewriting. We believe that our methods can be applied to modularity for conditional rewriting where several open problems exist. Any results we achieve here would be highly significant as, for the first time, substantial open problems in rewriting would have been solved using categorical techniques. This paper reports on the first step in this project, namely the construction of a semantics for CTRS using monads.

  @techreport{GhaniLuethKahrs
  ,   author= {Neil Ghani and Christoph L\"uth and Stefan Kahrs}
  ,   title= {Rewriting the Conditions in Conditional Rewriting}
  ,   institution= {Dept. Mathematics and Computer Science, University of Leicester}
  ,   number= {2000/20}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/ctrs2000.pdf}
  ,   year= {2000}
  }
  

• Christoph Lüth. Categorical Term Rewriting: Monads and Modularity.
  PhD Thesis, University of Edinburgh, 1997.
  AbstractPDF BibTeX

  Term rewriting systems are widely used throughout computer science as they provide an abstract model of computation while retaining a comparatively simple syntax and semantics. In order to reason within large term rewriting systems, structuring operations are used to build large term rewriting systems from smaller ones. Of particular interest is whether key properties are modular, that is, if the components of a structured term rewriting system satisfy a property, then does the term rewriting system as a whole? A body of literature addresses this problem, but most of the results and proofs depend on strong syntactic conditions and do not easily generalize. Although many specific modularity results are known, a coherent framework which explains the underlying principles behind these results is lacking. This thesis posits that part of the problem is the usual, concrete and syntax-oriented semantics of term rewriting systems, and that a semantics is needed which on the one hand elides unnecessary syntactic details but on the other hand still possesses enough expressive power to model the key concepts arising from the term structure, such as substitutions, layers, redexes etc.Drawing on the concepts of category theory, such a semantics is proposed, based on the concept of a monad, generalising the very elegant treatment of equational presentations in category theory. The theoretical basis of this work is the theory of enriched monads. It is shown how structuring operations are modelled on the level of monads, and that the semantics is compositional (it preserves the structuring operations). Modularity results can now be obtained directly at the level of combining monads without recourse to the syntax at all. As an application and demonstration of the usefulness of this approach, two modularity results for the disjoint union of two term rewriting systems are proven, the modularity of confluence (Toyama's theorem) and the modularity of strong normalization for a particular class of term rewriting systems (non-collapsing term rewriting systems). The proofs in the categorical setting provide a mild generalisation of these results.

  @PhdThesis{Lueth:Thesis
  ,   author= {Christoph L\"uth}
  ,   title= {Categorical Term Rewriting: Monads and Modularity}
  ,   school= {University of Edinburgh}
  ,   year= {1997}
  ,   links= {http://www.informatik.uni-bremen.de/~cxl/papers/thesis.pdf}
  }
  

• Christoph Lüth, Stefan Westmeier, Burkhardt Wolff. sml_tk: Functional Programming for Graphical User Interfaces.
  Technical report 8/96, FB 3, Universität Bremen, 1996.
  AbstractBibTeX

  sml_tk is a Standard ML package that provides a portable, typed and abstract interfce to the user interface and description language Tcl/Tk. This allows reusable programming of Graphical User Interfaces in a structured way, supported by the powerful module system of SML. Part of the sml_tk package is a library of standard components; in particular, the highly generic graphical user interface GenGUI, that has been instantiated for several theorem prover applications. This report presents an introduction, design description and a reference manual for sml_tk.

  @techreport{Lueth:smltk-Report
  ,   author= {Christoph L\"uth and Stefan Westmeier and Burkhardt Wolff}
  ,   title= {sml_tk: Functional Programming for Graphical User Interfaces}
  ,   institution= {FB 3, Universit\"at Bremen}
  ,   number= {8/96}
  ,   year= {1996}
  ,   moreLinks= {http://www.informatik.uni-bremen.de/~cxl/sml_tk/}
  }
  

Last Update: 2011-12-19 (Rev. 1534)