A Tactic Language for Hiproofs (2009)
David Aspinall, Ewen Denney, Christoph Lüth, Deutsches Forschungszentrum, Künstliche Intelligenz
Abstract. 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...
The Importance of Being Formal (2008)
Udo Frese, Daniel Hausmann, Christoph Lüth, Holger Täubig, Dennis Walter
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...
Nordic Journal of Computing 10(2003), 313–336. ABSTRACTING REFINEMENTS FOR TRANSFORMATION (2008)
Abstract. Formal program development by stepwise refinement involves a lot of work discharging proof obligations. Transformational techniques can reduce this work: applying correct transformation...
Nordic Journal of Computing 13(2006), 2–21 Structured Formal Development in Isabelle (2008)
Abstract. 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...
David Aspinall, Christoph Lüth
We give a brief overview of the Proof General Kit software framework for proof development. The goal of the framework is to enable flexible environments for managing formal proofs across their...
Formal Software Development: From Foundations to Tools (2008)
This exposé 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...
Proof General in Eclipse System and Architecture Overview (2008)
Daniel Winterstein, Christoph Lüth, Ahsan Fayyaz
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....
Nordic Journal of Computing Structured Formal Development in Isabelle (2008)
Abstract. 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...
Abstract Composing Monads Using Coproducts (2008)
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...
A Framework for Interactive Proof (2008)
David Aspinall, Christoph Lüth, Daniel Winterstein
Abstract. 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...
1 Introduction Proof General / Eclipse: A Generic Interface for Interactive Proof (2008)
Daniel Winterstein, David Aspinall, Christoph Lüth
Inspite of the considerable achievements of the formal proof
David Aspinall, Christoph Lüth, Daniel Winterstein
This paper describes how proof texts are constructed and edited in the Proof General Kit framework. Proof texts are the central object of development within our framework and we want to allow...
Nordic Journal of Computing 10(2003), 313–336. ABSTRACTING REFINEMENTS FOR TRANSFORMATION (2008)
Abstract. Formal program development by stepwise refinement involves a lot of work discharging proof obligations. Transformational techniques can reduce this work: applying correct transformation...
Nordic Journal of Computing 10(2003), 290–312. REWRITING VIA COINSERTERS (2008)
Abstract. 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...
CCC —the Casl Consistency Checker (2008)
Christoph Lüth, Markus Roggenbach, Lutz Schröder
Abstract. 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...
Nordic Journal of Computing 10(2003), 290–312. REWRITING VIA COINSERTERS (2008)
Abstract. 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...
A Framework for Interactive Proof (2008)
David Aspinall, Christoph Lüth, Daniel Winterstein
Abstract. This paper introduces a software framework for conducting interactive proof, dubbed the Proof General Kit. It defines a component infrastructure, the syntax of messages exchanged between...
DOI: 10.1051/ita:2003021 SOLVING ALGEBRAIC EQUATIONS USING COALGEBRA (2008)
Federico De Marchi, Neil Ghani, Christoph Lüth
Abstract. Algebraic systems of equations define functions using recursion where parameter passing is permitted. This generalizes the notion of a rational system of equations where parameter passing...
A Framework for Interactive Proof (2008)
David Aspinall, Christoph Lüth, Daniel Winterstein
Abstract. 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...
Nordic Journal of Computing 13(2006), 1–20. STRUCTURED FORMAL DEVELOPMENT IN ISABELLE (2008)
Abstract. 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...
Nordic Journal of Computing 10(2003), 313–336. ABSTRACTING REFINEMENTS FOR TRANSFORMATION (2008)
Abstract. Formal program development by stepwise refinement involves a lot of work discharging proof obligations. Transformational techniques can reduce this work: applying correct transformation...
TAS - A Generic Window Inference System (2007)
Christoph Lüth, Burkhart Wolff
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...
Generic Transformation Systems for Formal Methods (2007)
Christoph Lüth, Thomas Meyer, Burkhart Wolff
Introduction We will present two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle. Their distinguishing feature...
Haskell in Space - An Interactive Game as a Functional Programming Exercise (2007)
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...
Composing Monads Using Coproducts (2007)
Christoph Lüth, Christoph L Uth, Neil Ghani
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...
Haskell Communities and Activities Report (2006)
Andres Löh (ed, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, Dmitry Astapov, ...
This is the tenth edition of the Haskell Communities and Activities Report (HCAR) – a collection of entries about everything that is going on and related to Haskell in some way that appears twice a...
Assisted proof document authoring (2006)
David Aspinall, Christoph Lüth, Burkhart Wolff
Abstract. 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...
Assisted proof document authoring (2006)
David Aspinall, Christoph Lüth, Burkhart Wolff
Abstract. 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...
Dagstuhl-Manifest zur Strategischen Bedeutung des Software Engineering in Deutschland (2006)
Broy, Manfred, Jarke, Matthias, Nagl, Manfred, Rombach, Hans Dieter, Cremers, Armin B., Ebert, Jürgen, ...
Im Rahmen des Dagstuhl Perspektiven Workshop 05402 "Challenges for Software Engineering Research" haben führende Software Engineering Professoren den derzeitigen Stand der Softwaretechnik in...
Modular Modelling with Monads (2005)
monads, which are used to model diverse computational effects (such as stateful computations, exceptional behaviour or non-determinism). This goes back to Moggi [6], and is for example used to great...
Haskell Communities and Activities Report (2005)
Andres Löh (ed, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, Alistair Bayley, ...
Finally, here is the 9th edition of the Haskell Communities and Activities Report (HCAR), almost three weeks after the submission deadline. This delay is entirely my own fault. In fact, I have to...
Haskell Communities and Activities Report (2005)
Andres Löh (ed, Perry Alexander, Lloyd Allison, Tiago Miguel, Laureano Alves, Krasimir Angelov, ...
You are reading the 8th edition of the Haskell Communities and Activities Report (HCAR). These are interesting times to be a Haskell enthusiast. Everyone seems to be talking about darcs ( → 6.3)...
Haskell Communities and Activities Report (2004)
Andres Löh (ed, Perry Alexander, Lloyd Allison, Krasimir Angelov, Alistair Bayley, Jérémy Bobbio, ...
Welcome to the Seventh edition of the Haskell Communities and Activities report. I can proudly announce that the report has survived yet another change of editor, and chances are good that this...
Proof General meets IsaWin — combining textbased and graphical user interfaces (2004)
David Aspinall, Christoph Lüth
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...
Proof General meets IsaWin — combining textbased and graphical user interfaces (2004)
David Aspinall, Christoph Lüth
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...
Proof General meets IsaWin — combining textbased and graphical user interfaces (2004)
David Aspinall, Christoph Lüth
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...
Type class polymorphism in an institutional framework (2004)
Lutz Schröder, Till Mossakowski, Christoph Lüth
Abstract. Higher-order logic with shallow type class polymorphism is widely used as a specification formalism. Its polymorphic entities (types, operators, axioms) can easily be equipped with a...
Theorem reuse by proof term transformation (2004)
Einar Broch Johnsen, Christoph Lüth
Abstract. 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...
Type class polymorphism in an institutional framework (2004)
Lutz Schröder, Till Mossakowski, Christoph Lüth
Abstract. Higher-order logic with shallow type class polymorphism is widely used as a specification formalism. Its polymorphic entities (types, operators, axioms) can easily be equipped with a...
Semantic interrelation of documents via an ontology (2004)
Bernd Krieg-brückner, Arne Lindow, Christoph Lüth, Achim Mahnke, George Russell
Abstract: 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...
Theorem reuse by proof term transformation (2004)
Einar Broch Johnsen, Christoph Lüth
Abstract 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...
Bernd Krieg-brückner, Arne Lindow, Christoph Lüth, Achim Mahnke, George Russell, ...
MMiSS Multi-Media Instruction in Safe and Secure Systems 4
MultiMedia Instruction in (2003)
Safe And Secure, Bernd Krieg-brückner, Dieter Hutter, Arne Lindow, Christoph Lüth, Achim Mahnke, ...
The aim of the MMiSS project is the construction of a multimedia Internet-based adaptive educational system. Its content will initially cover a curriculum in the area of Safe and Secure Systems....
M.: Multimedia instruction in safe and secure systems (2003)
Bernd Krieg-brückner, Dieter Hutter, Arne Lindow, Christoph Lüth, Achim Mahnke, Erica Melis, ...
Abstract. The aim of the MMiSS project is the construction of a multimedia Internet-based adaptive educational system. Its content will initially cover a curriculum in the area of Safe and Secure...
Dualising initial algebras. Coalgebraic methods in computer science (Genova, 2001) (2003)
Ghani, Neil, Lüth, Christoph, De Marchi, Federico, Power, John
Abstract. 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...
More About TAS and IsaWin - Tools for Formal Program Development (2000)
Christoph Lüth, Burkhart Wolff
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...
TAS — a generic window inference system (2000)
Christoph Lüth, Burkhart Wolff
Abstract. 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...
More about TAS and IsaWin: Tools for formal program development (2000)
Christoph Lüth, Burkhart Wolff
Abstract. 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...
TAS and IsaWin: Tools for Transformational Program Development and Theorem Proving (1999)
Christoph Lüth, Haykal Tej, Bernd Krieg-Brückner
Introduction We will present two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle [9]. Their distinguishing...
Rewriting the Conditions in Conditional Rewriting (1999)
Neil Ghani, Christoph Lüth, Stefan Kahrs
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...
Rewriting the Conditions in Conditional Rewriting (1999)
Neil Ghani, Christoph Lüth, Stefan Kahrs
Category theory provides 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...
TAS and IsaWin: Tools for transformational program developkment and theorem proving (1999)
Christoph Lüth, Haykal Tej, Bernd Krieg-brückner
We will present two tools, TAS and IsaWin, for transformational program development and theorem proving respectively, based on the theorem prover Isabelle [9]. Their distinguishing features are a...
Categorical Term Rewriting: Monads and Modularity (1998)
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...
Categorical Term Rewriting: Monads and Modularity (1998)
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...
Monads and Modular Term Rewriting (1997)
. 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 [Lu96], the usefulness of this semantics...
Monads and modular term rewriting (1997)
Abstract. 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 [Lü96], this semantics was used...
Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem (1996)
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...
El bachillerato en Francia : las reformas de Fouchet y de Faure : 1965-1969
En: Historia de la educación : revista interuniversitaria Salamanca 1987, v. 6 ; p. 325-341