Techniche Universität, München

Our research focused mainly on two topics:

a) Verification of the type-inference algorithm W in Isabelle/HOL

We developed the first machine-checked verification of Milner's type inference algorithm W for computing the most general type of an untyped lambda-term enriched with let-expressions. This term language is the core of most typed functional programming languages and is also known as Mini-ML. The theories and proofs are developed in Isabelle/HOL, the HOL instantiation of the generic theorem prover Isabelle.

b) Proving a subset of Java (Java-light) type-safe in Isabelle/HOL

Java-light - a large sequential sublanguage of Java - has been formalized (abstract syntax, type system, well-formedness conditions, and an operational (evaluation) semantics). Based on this formalization, type soundness has been proven. All definitions and proofs have been done formally in the theorem prover Isabelle/HOL.

Wolfgang Naraschewski and Tobias Nipkow, Type Inference Verified: Algorithm W in Isabelle/HOL, Workshop TYPES'96, C. Paulin-Mohring (Ed.), Springer, LNCS. To appear.

Tobias Nipkow and David von Oheimb, Java light is Type-Safe -- Definitely, 25th ACM Symp. Principles of Programming Languages, ACM Press. To appear.

Tobias Nipkow, Winskel is (almost) Right: Towards a Mechanized Semantics Textbook, Foundations of Software Technology and Theoretical Computer Science, V. Chandru and V. Vinay (Eds.), LNCS, volume=1180,1996, pages180-192.

Martin Hofmann, Wolfgang Naraschewski, Martin Steffen and Terry Stroup, Inheritance of Proofs, Theory and Practice of Object-Oriented Systems (Special Issue), 1998. To appear.

Wolfgang Naraschewski, Towards an Object-Oriented Progification Language, Theorem Proving in Higher Order Logics, Elsa L. Gunter and Amy Felty (Eds.), Springer,LNCS,volume 1275, 1997, pages 215-230

Markus Wenzel, Type Classes and Overloading in Higher-Order Logic, Theorem Proving in Higher Order Logics, Elsa L. Gunter and Amy Felty (Eds.), LNCS,volume 1275, 1997, pages 307-322