Techniche Universität, München

1. Developing, documenting and applying the Isabelle system
   • Isabelle/Isar, a generic environment for producing human-readable proof documents.
   • Implementation of the Owicki-Gries method for the verification of parallel programs.
   • A new definitional datatype package supporting mutual, indirect and strictly positive recursion.
   • Case studies: Formalization of programming language concepts and verification of a type inference algorithm.
   
   Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL. In: Theorem Proving in Higher Order Logics, Y. Bertot et al. eds, Springer LNCS 1690, pp. 19-36, 1999.
   

   Florian Kammüller and Markus Wenzel and Lawrence C. Paulson. Locales - A Sectioning Concept for Isabelle. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Springer LNCS 1690, 1999.
   

   Wolfgang Naraschewski and Tobias Nipkow. Type Inference Verified: Algorithm W in Isabelle/HOL. Journal of Automated Reasoning 23, pp. 299-318, 1999.
   

   Tobias Nipkow. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. Formal Aspects of Computing 10, pp. 171-186, 1998.
   

   Tobias Nipkow and Leonor Prensa Nieto. Owicki/Gries in Isabelle/HOL. In: Fundamental Approaches to Software Engineering (FASE'99), J.-P. Finance ed, Springer LNCS 1577, pp. 188-203, 1999.
   

   Markus Wenzel. Isar - a Generic Interpretative Approach to Readable Formal Proof Documents. In: Theorem Proving in Higher Order Logics, Y. Bertot et al. eds, Springer LNCS 1690, pp. 167-183, 1999.
   

2. Formalizing Java and the Java Virtual Machine in Isabelle/HOL
   We have significantly extended our formalization of both Java and the Java Virtual Machine. It now includes a type safety proof for the bytecode verifier, a correctness proof for a simple compiler, and a Hoare logic.
   
   David von Oheimb. Hoare Logic for Mutual Recursion and Local Variables. In: Foundations of Software Technology and Theoretical Computer Science (FST and TCS), Springer LNCS, 1999.
   

   David von Oheimb and Tobias Nipkow. Machine-Checking the Java Specification: Proving Type-Safety. In: Formal Syntax and Semantics of Java, J. Alves-Foss ed, Springer LNCS 1523, pp. 119-156, 1999.
   

   Cornelia Pusch. Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL. In: Tools and Algorithms for the Construction and Analysis of Systems (TACAS'99), W.R. Cleaveland ed, Springer LNCS 1579, pp. 89-103, 1999.
   

3. Embedding LCF in HOL: HOLCF
   We have completed our embedding of the logical system LCF (for reasoning about partial functions) in Isabelle/HOL. A significant part of the meta-theory of Input/Output Automata, a model of distributed systems, has been verified in HOLCF.
   
   Olaf Müller. A Verification Environment for I/O-Automata Based on Formalized Meta-Theory. PhD thesis, Institut für Informatik, Techn. Univ. München, 1998.
   

   Olaf Müller and Tobias Nipkow and David von Oheimb and Oskar Slotosch. HOLCF = HOL + LCF. Journal of Functional Programming 9, pp. 191-223, 1999.
   

Ludwig-Maximilians-Universität München

1. Developing the theory of MuTTI (Munich Type Theory Implementation)

   The goal of MuTTI is an integration of Type Theory and functional programming. We investigated the implementation and theory of a termination checker of a simply typed sublanguage with general recursion and simple pattern matching (foetus).

   Thorsten Altenkirch Design criteria for dependently typed programming and verification languages Talk given at the Workshop on Dependent Types in Programming of the ESPRIT working groups APPSEM and TYPES in Göteborg, Sweden, 27.3. -28.3. 99.

   Andreas Abel A Semantic Analysis of Structural Recursion . Diploma Thesis (1999)

   Andreas Abel foetus - Termination Checker for Simple Functional Programs . Technical report (1998)

2. Formalizing semantics in non-standard type theories

   We formalized Synthetic Domain Theory (SDT) in the Extended Calculus of Constructions (ECC) with additional axioms (extensionality, proof irrelevance and additional SDT axioms )

   Bernhard Reus Formalizing Synthetic Domain Theory - The Basic Definitions. Journal of Automated Reasoning, 1999.

   Bernhard Reus, Thomas Streicher General Synthetic Domain Theory - A Logical Approach. MSCS 9:177-223. Cambridge University Press, 1999.

3. Foundational studies of lambda calculus and types
   • Extensionality in a decidable and adequate intensional type theory
   • A representation of lambda terms using heterogeneous inductive types
   • Logical relations for inductive and coinductive types

   Thorsten Altenkirch. Extensional equality in intensional type theory. In LICS 99, 1999.

   Thorsten Altenkirch and Bernhard Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic, 1999.

   Thorsten Altenkirch. Logical relations and inductive/coinductive types. In Computer Science Logic, LNCS 1584, pages 343-354, 1998.

4. Workshop organisation

   Thorsten Altenkirch (LMU), Wolfgang Naraschewski (TU) and Bernhard Reus (LMU) organized the annual meeting of the Types Working Group at Kloster Irsee in March 98.

   Thorsten Altenkirch, Wolfgang Naraschewski, Bernhard Reus (Eds): Types for Proofs and Programs. Proceedings of the Types Working Group Meeting, 1998. LNCS 1657, Springer, Berlin, 1999.