Types for proofs and programs

the long version

Types for Proofs and Programs: International Workshop, TYPES’ 98 Kloster Irsee, Germany, March 27–31, 1998 Selected Papers<br />Author: Thorsten Altenkirch, Bernhard Reus, Wolfgang Naraschewski<br /> Published by Springer Berlin Heidelberg<br /> ISBN: 978-3-540-66537-3<br /> DOI: 10.1007/3-540-48167-2<br /><br />Table of Contents:<p></p><ul><li>On Relating Type Theories and Set Theories </li><li>Communication Modelling and Context-Dependent Interpretation: An Integrated Approach </li><li>Gröbner Bases in Type Theory </li><li>A Modal Lambda Calculus with Iteration and Case Constructs </li><li>Proof Normalization Modulo </li><li>Proof of Imperative Programs in Type Theory </li><li>An Interpretation of the Fan Theorem in Type Theory </li><li>Conjunctive Types and SKInT </li><li>Modular Structures as Dependent Types in Isabelle </li><li>Metatheory of Verification Calculi in LEGO </li><li>Bounded Polymorphism for Extensible Objects </li><li>About Effective Quotients in Constructive Type Theory </li><li>Algorithms for Equality and Unification in the Presence of Notational Definitions </li><li>A Preview of the Basic Picture: A New Perspective on Formal Topology</li></ul>