Marko Luther

Dr. Marko Luther  Abtl. Künstliche Intelligenz  Universität Ulm  D-89069 Ulm  (+49) 731 / 50 - 24116  (+49) 731 / 50 - 24119  O27 / 421  luther@ki.informatik.uni-ulm.de GPG Public Key Fingerprint (D-H/DSS): A676 ABAC 5BEA A0AE 8EDA C6A5 C09A 7933 4DAE D781

WS 2003/2004

• Computergestützte Modellierung und Verifikation

• Einführung in die LISP-Programmierung

• The Typelab Project (Deduction and Software Verification)

• Marko Luther
  Elaboration and Erasure in Type Theory
  Ph.D. thesis, University of Ulm, 2003


• Marko Luther
  More On Implicit Syntax
  Proceedings of IJCAR'01, LNAI 2083, pp. 386-400, 2001, © Springer-Verlag


• Thorsten Liebig, Dieter Finkenzeller, Marko Luther
  KB-VISION: A Tool for Graphical Manipulation and Visualization of Domain Models
  10th European - Japanese Conference on Information Modelling and Knowledge Bases EJC 2000, Saariselkä, Finland, May 2000.


• Martin Strecker, Marko Luther, F.W. von Henke
  Book Chapter: Interactive and automated proof construction in type theory
  Foundations, Chapter 3: Interactive Theorem Proving.
  In : Automated Deduction - A Basis for Applications, W. Bibel and P. Schmitt, Kluwer Academic Publishers, 1998


• Marko Luther, Martin Strecker
  A guided tour through Typelab
  Technical Report UIB-98-03, Universität Ulm, Fakultät für Informatik, Jan. 1998


• Martin Strecker, Marko Luther, F.W. von Henke
  Typelab: An Environment for Modular Program Development
  Proc. of TAPSOFT'97, LNCS 1214, pp. 851-854, 1997, © Springer-Verlag


• Martin Strecker, Marko Luther, Matthias Wagner
  Structuring and Using a Knowledge Base of Mathematical Concepts: A Type-Theoretic Approach
  Proc. of ECAI'96, pp. 23-26, 1996


• F.W. von Henke, Marko Luther, Holger Pfeifer, Harald Rueß, Detlef Schwier, Martin Strecker, Matthias Wagner
  The Typelab Specification and Verification Environment
  Proc. of AMAST'96, LNCS 1101, pp. 604-607, Munich, 1996, © Springer-Verlag


• Marko Luther; Master's Thesis (in German):
  Wissensbasierte Methoden zur Beweisunterstüzung in Typentheorie
  Fakultät für Informatik, Universität Ulm (1995)

• I was a participant of the International Summer School Marktoberdorf (Germany) on Calculational System Design from July 28 to August 9, 1998.
• In my spare time I play the saxophone in the famous band The Soul Plumbers. Sometimes I also play gigs with a free jazz combo.
• http://www.luther.de
• http://www.hausband.de
• http://www.typelab.com
• http://www.thetypes.com/fonts/script/typelab.html