@InProceedings{AspinallDenneyLueth:LPAR2013, author = {David Aspinall and Ewen Denney and Christoph L\"uth}, title = {A Semantic Basis for Proof Queries and Transformations}, booktitle = {19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-19)}, editor = { McMillan, K. and Middeldrop, A. and Voronkov, A.} year = 2013, pages = {53-- 70}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 8312 } @Proceedings{Lueth:UITP2012, title = {Proceedings 10th International Workshop On User Interfaces for Theorem Provers}, year = 2013, month = {July}, editor = {Cezary Kaliszyk and Christoph L\"uth}, volume = 118, series = {Electronic Proceedings in Theoretical Computer Science}, doi = {10.4204/EPTCS.118} } @inproceedings{Lueth:CICM13, author={L\"uth, Christoph and Ring, Martin}, title={A Web Interface for Isabelle: The Next Generation}, booktitle={Conferences on Intelligent Computer Mathematics {CICM} 2013}, editor={Carette, Jacques}, volume={7961}, series={Lecture Notes in Artificial Intelligence}, publisher={Springer}, pages={326-- 329} year={2013}, } @inproceedings{Lueth:IsoLa2012, author={Autexier, Serge and Dietrich, Dominik and Hutter, Dieter and L\"uth, Christoph and Maeder, Christian}, title={SmartTies --- Management of Safety-Critical Developments}, booktitle={Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change}, editor={Margaria, Tiziana and Steffen, Bernhard}, volume={7609}, series={Lecture Notes in Computer Science}, doi={10.1007/978-3-642-34026-0_18}, publisher={Springer}, pages={238-- 252}, year={2012} } @InProceedings{AspinallDenneyLueth:LPAR2012, author = {David Aspinall and Ewen Denney and Christoph L\"uth}, title = {Querying Proofs}, booktitle = {18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-18)}, year = 2012, pages = {92-- 106}, ee = {http://dx.doi.org/10.1007/978-3-642-28717-6_10}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {7180} } @article{TaubigFreseLuethEtAl:SAMS-AR, 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}, volume = {32}, number = {3}, month = {4}, year = {2012}, pages = {303-- 331}, journal = {Autonomous Robots}, publisher = {Springer} } @Article{AspinallDenneyLueth:MCS2010, author = {Aspinall, David and Denney, Ewen and L\"uth, Christoph}, title = {Tactics for Hierarchical Proofs}, journal = {Mathematics in Computer Science}, year = 2010, volume = 3, pages = {309-- 330}, month = {March} } @InProceedings{AutexierLueth:iFM2010, author = {Autexier, Serge and and L\"uth, Christoph}, title = {Adding Change Impact Analysis to the Formal Verification of {C} Programs}, booktitle = {iFM 2010: {I}ntegrated {F}ormal {M}ethods - $8^{th}$ International Conference}, publisher = {Springer}, volume = 6396, series = {Lecture Notes in Computer Science}, pages = {59-- 73} } @InProceedings{BortinLueth:AISC2010, author = {Bortin, Maksym and L\"uth, Christoph}, title = {Structural Formal Development with Quotient Types in {Isabelle/HOL}}, booktitle = {AISC 2010 --- $10^{th}$ International Conference on Artificial Intelligence and Symbolic Computation}, publisher = {Springer}, volume = 6167, series = {Lecture Notes in Computer Science}, pages = {34-- 48}, year = {2010} } @InProceedings{WalterTaeubigLueth:SafeComp2010, author = {Walter, Dennis and T\"aubig, Holger and L\"uth, Christoph}, title = {Experiences in Applying Formal Verification in Robotics}, booktitle = {SafeComp 2010 --- $29^{th}$ International Conference on Computer Safety, Reliability and Security}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, note = 6351, pages = {347-- 360}. year = {2010} } @TechReport{Lueth:RR-10-01, author = {L\"uth, Christoph}, title = {Schlussbericht des Projektes {SAMS}}, institution = {Deutsches Forschungszentrum f\"ur K\"unstliche Intelligenz}, year = 2010, type = {Research Report}, number = {DFKI-RR-10-01} } @InProceedings{LuethWalter:FM2009, author = {L\"uth, Christoph and Walter, Dennis}, title = {Certifiable specification and verification of {C} programs}, editor = {Ana Cavalcanti and Dennis Dams}, booktitle = {Formal Methods (FM 2009)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {5350}, pages = {419-- 434}, year = {2009} } @InProceedings{Lueth:AVOCS09, author = {L\"uth, Christoph}, title = {User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?}, booktitle = {Ninth International Workshop on Automated Verification of Critical Systems {AVOCS'09}}, year = {2009}, volume = 23 series = {Electronic Communications of the {EASST}}, note = {To appear.} } @InProceedings{cxl:UITP08, author = {Aspinall, David and Autexier, Serge and L\"uth, Christoph and Wagner, Marc}, title = {Towards Merging {Plat$\Omega$} and {PGIP}}, booktitle = {Proc. 8th International Workshop on User Interfaces for Theorem Provers (UITP 2008)}, publisher = {Elsevier Science}, series = {Electronic Notes in Theoretical Computer Science}, volume = 226, year = {2009}, pages = {3-- 21} } @InProceedings{cxl:MKM08, author = {Aspinall, David and Denney, Ewen and L\"uth, Christoph}, title = {A Tactic Language for Hiproofs}, booktitle = {Mathematical Knowledge Management {MKM 2008}, Intelligent Computer Mathematics}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, volume = 5144, year = {2008}, pages = {339-- 354} } @InCollection{cxl:robotik2008, author = {Christoph L{\"u}th and Udo Frese and Holger T{\"a}ubig and Dennis Walter and Daniel Hausmann}, title = {SAMS Sicherheitskomponente f{\"u}r Autonome Mobile Serviceroboter}, year = {2008}, booktitle = {VDI-Bericht}, publisher = {VDI-Verlag}, volume = {2012}, status = {Reviewed} } @InProceedings{cxl:softzert08, author = {Udo Frese and Daniel Hausmann and Christoph L{\"u}th and Holger T{\"a}ubig and Dennis Walter}, title = {Zertifizierung einer Sicherungskomponente mittels durchg{\"a}ngig formaler Modellierung}, year = {2008}, booktitle = {Software Engineering 2008}, publisher = {Gesellschaft f\"ur Informatik}, series = {Lecture Notes in Informatics}, volume = {P-122}, pages = {335-- 338} } @InProceedings{cxl:SafeCert08, author = {Udo Frese and Daniel Hausmann and Christoph L{\"u}th and Holger T{\"a}ubig and Dennis Walter}, title = {The Importance of Being Formal}, year = {2009}, editor = {Hardi Hungar}, booktitle = {International Workshop on the Certification of Safety-Critical Software Controlled Systems SafeCert'08}, publisher = {Elsevier Science}, series = {Electronic Notes in Theoretical Computer Science}, volume = 238, pages = {57-- 70}, doi = {http://dx.doi.org/10.1016/j.entcs.2009.09.006} } @InProceedings{Lueth:PGIPImp, author = {Aspinall, David and L\"uth, Christoph and Winterstein, Daniel}, title = {A Framework for Interactive Proof}, booktitle = {Mathematical Knowledge Management {MKM 2007}}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, volume = 4573, year = {2007}, pages = {161-- 175} } @Article{Lueth:SicherheitKI author = {L\"{u}th, Christoph and Krieg-Br\"{u}ckner, Bernd}, title = {Sicherheit in der K\"unstlichen Intelligenz}, journal = {K\"unstliche Intelligenz}, year = {2007}, volume = {1}, pages = {51-- 52} } @Article{Lueth:StructuredDev, author = {Bortin, Maksym and Broch~Johnsen, Einar and L\"{u}th, Christoph}, title = {Structured Formal Development in Isabelle}, journal = {Nordic Journal of Computing}, year = {2006}, volume = {13}, pages = {1-- 20} } @InProceedings{Lueth:PGEclipse, author = {Aspinall, David and L\"uth, Christoph and Winterstein, Daniel and Fayyaz, Ahsan}, title = {Proof General in Eclipse}, booktitle = {Eclipse Technology eXchange ETX'06}, publisher = {{ACM} Press}, year = {2006}, } @InProceedings{Lueth:ProofDocAuthoring, author = {Aspinall, David and L\"uth, Christoph and Wolff, Burkhart}, title = {Assisted Proof Document Authoring}, booktitle = {Mathematical Knowledge Management {MKM 2005}}, editor = {Michael Kohlhase}, publisher = {Springer}, series = {Lecture Notes in Artificial Intelligence}, volume = 3863, year = {2006}, pages = {65-- 80} } @InProceedings{Lueth:AbsMod, author = {Micheal Abbot, 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 = apr } @InProceedings{Lueth:TheoremReuse, author = {Broch~Johnsen, Einar and L\"uth, Christoph}, 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 = sep } @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 } @Article{Lueth:AbstractingTransformations, author = {Broch~Johnsen, Einar and L\"uth, Christoph}, title = "Abstracting Transformations for Refinement", journal = "Nordic Journal of Computing", volume = 10, pages = {316-- 336}, year = 2004 } @Article{Lueth:MSCS04, author = {N.~Ghani and C.~L\"uth and F.~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 = Jun, year = 2005, note = "doi: 10.1017/S0960129505004743" } @Article{Lueth:SolvingAlgebraicEquations, author = {de~Marchi, Federico and Ghani, Neil and L\"uth, Christoph }, title = "Coalgebraic Approaches to Algebraic Terms", journal = "Theoretical Informatics and Applications", volume = 37, pages = {301-- 314}, year = 2003 } @Article{AspinallLueth04, author = {David Aspinall and Christoph L{\"u}th}, title = {{Proof General} meets {IsaWin}: Combining Text-Based and Graphical User Interfaces}, journal = {Electronic Notes in Theoretical Computer Science}, month = {November}, year = 2004, volume = 103, issue = {C}, pages = {3--26}, url = {http://www.sciencedirect.com/science/article/B75H1-4DN4HVV-2/2/39d1b3e85f828fde18ee7a35becf7958} } @Article{Lueth:HaskellInSpace, author = {Christoph~L\"uth}, title = "Haskell in Space", journal = "Journal of Functional Programming", volume = 13, number = 6, pages = {1077-- 1085}, month = Nov, year = 2003 } @InProceedings{Lueth:WADT04a, author = {Christoph L{\"u}th and Markus Roggenbach and Lutz Schr{\"o}der}, title = {{CCC} - The {CASL} Consistency Checker}, year = 2005, editor = {Jos{\'e} Fiadeiro}, booktitle = {Recent Trends in Algebraic Development Techniques, 17th International Workshop (WADT 2004)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = 3423, pages = {94--105} } @InProceedings{Lueth:WADT04b, author = {Lutz Schr{\"o}der and Till Mossakowski and Christoph L{\"u}th}, title = {Type class polymorphism in an institutional framework}, year = 2005, editor = {Jos{\'e} Fiadeiro}, booktitle = {Recent Trends in Algebraic Development Techniques, 17th International Workshop (WADT 2004)}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume= 3423, pages = {234-- 248} } @InProceedings{SemInter-DELFI04, author = {Bernd Krieg-Br{\"u}ckner and Arne Lindow and Christoph L{\"u}th and Achim Mahnke and Georg Russell}, title = {Semantic Interrelation of Documents via an Ontology}, year = {2004}, editor = {Gregor Engels and Silke Seehusen}, booktitle = {DeLFI 2004, Tagungsband der 2. e-Learning Fachtagung Informatik, 6.-8. September 2004, Paderborn, Germany}, publisher = {Gesellschaft f\"ur Informatik}, series = {Lecture Notes in Informatics}, volume = {P-52}, pages = {271--282}, isbn = {3-88579-381-4} } @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 = Sep, publisher = {{ACM} Press} } @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 = Sep, publisher = {Technischer Bereicht~0210, Institut f\"ur Informatik und Praktische Mathematik, Christian-Albrechts-Universit\"at Kiel} } @InProceedings{Lueth:MMiSS2002, editor = {Martin Wirsing and Dirk Pattinson and Rolf Hennicker}, booktitle = {Recent Trends in Algebraic Development Techniques, 16th International Workshop, WADT 2002}, author = {Bernd Krieg-Br\" uckner and Dieter Hutter and Arne Lindow and Christoph L\"uth and Achim Mahnke and Erica Melis and Philipp Meier and Arnd Poetzsch-Heffter and Markus Roggenbach and George Russell and Jan-Georg Smaus and Martin Wirsing}, title = {MultiMedia Instruction in Safe and Secure Systems}, pages = {82-- 117}, publisher = {Springer}, series = {Lecture Notes in Computer Science}, volume = {2755}, year = {2003} } @InProceedings{Lueth:fics02, author = {Ghani, Neil and L\"uth, Christoph and de~Marchi, Federico}, title = {Coalgebraic Approaches to Algebraic Terms}, booktitle = {Fixed Points in Computer Science}, pages = {6-- 8}, year = 2002, editor = {\'{E}sik, Zoltan and Ing\'olfsd\'ottir, Anna}, series = {{BRICS} Notes Series NS-02-2}, month = {June} } @InProceedings{Lueth:FroCoS02, author = {Christoph~L\"uth and Neil~Ghani}, title = "Monads and Modularity", pages = {18--32}, editor = {Alessandro~Armando}, booktitle = "Frontiers of Combining Systems {FroCos} 2002, 4th International Workshop", series = "Lecture Notes in Artificial Intelligence", publisher = "Springer Verlag", number = 2309, year = 2002 } @InProceedings{Lueth:CMCS02, author = {Neil Ghani, Christoph Luth and Federico De Marchi}, title = {Coalgebraic Monads}, booktitle = {Electronic Notes in Theoretical Computer Science}, volume = {65}, issue = {1}, publisher = {Elsevier Science Publishers}, editor = {Lawrence S. Moss}, year = {2002} } @Article{Lueth:MSCS, author = {N.~Ghani and C.~L\"uth and F.~de~Marchi and J.~Power}, title = "Dualising Initial Algebras", journal = "Mathematical Structures in Computer Science", year = 2003, volume = "13", number = "2", pages = "349-- 370" } @InProceedings{Lueth:CMCS01, author = {N.~Ghani and C.~L\"uth and F.~de~Marchi and J.~Power}, title = {Algebras, Coalgebras, Monads and Comonads}, booktitle = {Proceedings {CMCS'01}}, journal = {Electronic Notes in Theoretical Computer Science}, year = 2001, editor = {U.~Montanari}, volume = 44 } @InProceedings{Lueth:TPHOLs00, author = {C.~L\"uth and B.~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", number = 1869, year = 2000 } @InProceedings{Lueth:ETAPS00, author = {C.~L\"uth and B.~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", number = 1783, year = 2000 } @Article{LuethWolff, author = {C.~L\"uth and B.~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 = Mar, year = 1999 } @InProceedings{Lueth:ETAPS99, author = {C.~L\"uth and H,~Tej and Kolyang and B.~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", number = 1577, year = 1999 } @InProceedings{Lueth:zum98, title = {HOL-{Z} in the {UniForM}-Workbench -- A Case Study in Tool Integration for {Z}}, author = {C. L\"uth and E. W. Karlsen and Kolyang and S. Westmeier and B. Wolff}, pages = {116--134}, editor = {J. P. Bowen and A. Fett and M. G. Hinchey}, booktitle = {{ZUM'98}: The {Z} Formal Specification Notation, 11th International Conference of {Z} Users}, publisher = "Springer Verlag", series = "Lecture Notes in Computer Science", number = 1493, year = 1998 } @InProceedings{Lueth:Tools98, author = {C.~L\"{u}th and E.~W.~Karlsen and Kolyang and S.~Westmeier and B.~Wolff}, title = "Tool Integration in the {UniForM} Workbench", booktitle = "Tool Support for System Specification, Development, and Verification", editors = "R.~Berghammer and Y.~Lakhnech", pages = {160--173}, year = 1999, publisher = "Springer-Verlag Wien New York", series = "Advances in Computing Science", } @InProceedings{Lueth:Tapsoft97, author = {Kolyang and C.~L\"uth and T.~Meier and B.~Wolff}, title = "{TAS} and {I}sa{W}in: Generic Interfaces for Transformational Program Development and Theorem Proving", editor = "M.~Bidoit and M.~Dauchet", number = 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" } @TechReport{Lueth:smltk-Report, author = {C.~L\"uth and S.~Westmeier and B.~Wolff}, title = {sml\_{}tk: Functional Programming for Graphical User Interfaces}, institution = {FB~3, Universit\"at Bremen}, number = {8/96}, year = 1996 } @InProceedings{Lueth:nwpt8, author = {C.~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 = "Dec" } @inproceedings{Lueth:UITP96, author = {Kolyang and C.~L\"uth and T.~Meier and B.~Wolff}, booktitle = {User Interfaces for Theorem Provers (UITP '96), Proceedings}, editor = {N.~Merriam}, pages = "59-- 66", publisher = {University of York}, series = {Technical Report}, title = "Generating Graphical User-Interfaces in a Functional Setting", year = 1996, annote= "Electronic proceedings at {\tt http://dcpu1.cs.york.ac.uk:6666/~nam/uitp/proceedings.html}" } @InProceedings{Lueth:Tools96, author = {Kolyang and C.~L\"uth and T.~Meier and B.~Wolff}, title = "Generic Interfaces for Transformation Systems and Interactive Theorem Provers", editor = "B.~Berghammer and B.~Buth and J.~Peleska", series = "BISS Monographs", number = 1, booktitle = "International Workshop on Tool Support for Validation and Verfication", year = 1998, publisher = "Shaker Verlag" } @InProceedings{Lueth:RTA96, author = {C.~L\"uth}, title = "Compositional Term Rewriting: An Algebraic Proof of Toyama's Theorem", editor = "H.~Ganzinger", number = 1103, series = "Lecture Notes in Computer Science", pages = "261-- 275", booktitle = "Rewriting Techniques and Applications", address = "New Brunswick, USA", year = 1996, publisher = "Springer Verlag", month = "July" } @InProceedings{Lueth:CTCS97, author = {C.~L\"uth and N.~Ghani}, title = "Monads and Modular Term Rewriting", editor = "E.~Moggi and G.~Rosolini", number = 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" } @TechReport{GhaniLuethKahrs, author = {N.~Ghani and C.~L\"uth and S.~Kahrs}, title = {Rewriting the Conditions in Conditional Rewriting}, institution = {Dept. Mathematics and Computer Science, University of Leicester}, number = {2000/20}, year = 2000 } @PhdThesis{Lueth:Thesis, author = {C.~L\"uth}, title = "Categorical Term Rewriting: Monads and Modularity", school = "University of Edinburgh", year = "1997" }