Next: Univiversity of Birmingham Up: Progress Report Previous: Katholieke Univ. Nijmegen

Techniche Universität, München

  1. Developing, documenting and applying the Isabelle system
    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

    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.

Next: Katholieke Univ. Nijmegen Up: Progress Report Previous: University of Manchester